From: "Randy Brukardt" <randy@rrsoftware.com>
Subject: Re: Tests in a software release
Date: Tue, 14 Nov 2017 18:01:28 -0600
Date: 2017-11-14T18:01:28-06:00 [thread overview]
Message-ID: <oug04o$h02$1@franka.jacob-sparre.dk> (raw)
In-Reply-To: ot981s$7m5$1@dont-email.me
"G.B." <bauhaus@notmyhomepage.invalid> wrote in message
news:ot981s$7m5$1@dont-email.me...
...
> Checking is behavior. However, let SPARK check conditions
> of a contract, and let the result be Truth. Then they
> have been checked before the program even runs, and
> turning *off* Ada checks is, therefore, justified.
Yes, but a compiler can do this better, since it knows the actual
representations chosen (which might ensure that a check cannot fail where
SPARK may not be able to prove this, at least not without lots of additional
information). Moreover, a compiler surely knows if it generated code to
raise Constraint_Error.
Ergo, I would much prefer to trust the compiler (and if you can't trust your
compiler, you have a serious problem that no other tool is going to be able
to help with) rather than having to trust an entire chain of tools that
necessarily has to include the compiler.
There are lots of things that SPARK can prove that a compiler can't, but
there aren't many (if any) check eliminations that require the power of
SPARK (and I believe that the vast majority of those can be fixed with the
addition of additional tests or subtypes).
Randy.
next prev parent reply other threads:[~2017-11-15 0:01 UTC|newest]
Thread overview: 39+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-10-25 19:30 Tests in a software release Victor Porton
2017-10-26 7:20 ` Dmitry A. Kazakov
2017-10-27 18:06 ` G. B.
2017-10-27 18:54 ` Dmitry A. Kazakov
2017-10-28 6:53 ` G.B.
2017-10-28 7:35 ` Dmitry A. Kazakov
2017-10-30 20:44 ` G. B.
2017-10-30 20:56 ` Dmitry A. Kazakov
2017-10-31 7:17 ` G.B.
2017-10-31 8:32 ` Dmitry A. Kazakov
2017-11-03 7:24 ` G.B.
2017-11-03 8:16 ` Dmitry A. Kazakov
2017-11-03 12:49 ` Shark8
2017-11-04 10:15 ` G.B.
2017-11-15 0:11 ` Randy Brukardt
2017-11-15 17:57 ` G. B.
2017-11-15 20:46 ` Dmitry A. Kazakov
2017-11-17 15:36 ` Shark8
2017-11-15 22:17 ` Randy Brukardt
2017-11-16 21:44 ` G.B.
2017-11-17 0:15 ` Randy Brukardt
2017-11-17 15:45 ` Shark8
2017-11-18 1:07 ` Randy Brukardt
2017-11-15 0:06 ` Randy Brukardt
2017-11-15 8:47 ` Dmitry A. Kazakov
2017-11-15 21:53 ` Randy Brukardt
2017-11-15 16:47 ` Jeffrey R. Carter
2017-11-15 16:59 ` J-P. Rosen
2017-11-15 20:45 ` Dmitry A. Kazakov
2017-11-15 21:58 ` Randy Brukardt
2017-11-16 5:50 ` J-P. Rosen
2017-11-16 23:53 ` Randy Brukardt
2017-11-15 0:01 ` Randy Brukardt [this message]
2017-11-16 17:02 ` Robert Eachus
2017-11-17 0:20 ` Randy Brukardt
2017-11-22 20:40 ` Robert Eachus
2017-11-14 23:55 ` Randy Brukardt
2017-10-26 8:09 ` Stefan.Lucks
2017-10-26 17:30 ` Simon Clubley
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox