From: "Randy Brukardt" <randy@rrsoftware.com>
Subject: Re: {Pre,Post}conditions and side effects
Date: Fri, 8 May 2015 17:52:15 -0500
Date: 2015-05-08T17:52:15-05:00 [thread overview]
Message-ID: <mijen0$1hj$1@loke.gir.dk> (raw)
In-Reply-To: alpine.DEB.2.11.1505072052570.16448@debian
<Stefan.Lucks@uni-weimar.de> wrote in message
news:alpine.DEB.2.11.1505072052570.16448@debian...
> On Thu, 7 May 2015, Randy Brukardt wrote:
...
>> You ought to fix your
>> program (probably by adding an appropriate predicate) so that the check
>> *can* be eliminated (or pushed to somewhere where the cost is
>> irrelevant).
>
>Why do I need to fix the program, if I know it is correct? Just because
>the compiler isn't good enough at theorem proving?
Because there is no such thing. There is no real way for you to know that it
is correct. I have plenty of examples of supposedly correct programs that
turned out to have serious bugs.
The only way for a program to be "correct" is for it to be proven that way
by the compiler. (And even then, the compiler algorithm might have
problems.) Because if any other tool does it, the compiler might disagree
(because either tool has bugs), and thus the actual code might still in fact
be incorrect.
>>> Turning off the checks just hides the problem.
>
>*IF* there is a problem at all.
See above. There is *always* a problem; the only question is whether you are
willing to defend against it or not.
For example, in this "Is_Sorted" example, if you are assuming that some
object is sorted, then it should have a predicate to that effect. In such a
case, the compiler would be able to eliminate all of the precondition checks
on calls, the only time the predicate would be checked is when the object is
initially created (which certainly should not be on any critical path), or
if it is modified by a routine that doesn't include Is_Sorted in its
postcondition (which is clearly the source of potential bugs as well).
In the absence of those sorts of things, you are just hiding potential
flaws.
Randy.
next prev parent reply other threads:[~2015-05-08 22:52 UTC|newest]
Thread overview: 107+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-12-22 16:22 {Pre,Post}conditions and side effects Jean François Martinez
2014-12-22 17:18 ` Brad Moore
2014-12-23 8:22 ` Jean François Martinez
2014-12-23 17:05 ` Robert A Duff
2014-12-23 21:09 ` Jean François Martinez
2014-12-23 21:35 ` Robert A Duff
2014-12-23 23:02 ` Peter Chapin
2014-12-24 1:03 ` Robert A Duff
2015-04-24 8:59 ` Jacob Sparre Andersen
2015-04-24 9:18 ` J-P. Rosen
2015-04-24 23:39 ` Randy Brukardt
2015-04-24 12:10 ` G.B.
2015-04-24 14:40 ` Jacob Sparre Andersen
2015-04-24 16:29 ` G.B.
2015-04-24 23:46 ` Randy Brukardt
2015-04-24 22:26 ` Peter Chapin
2015-04-25 0:13 ` Randy Brukardt
2015-04-25 1:01 ` Peter Chapin
2015-04-25 5:51 ` Dmitry A. Kazakov
2015-04-25 0:31 ` Bob Duff
2015-04-25 12:08 ` vincent.diemunsch
2015-04-25 16:37 ` Georg Bauhaus
2015-05-06 21:07 ` Randy Brukardt
2015-05-06 22:10 ` Paul Rubin
2015-05-07 9:01 ` Georg Bauhaus
2015-05-07 9:12 ` Dmitry A. Kazakov
2015-05-07 9:29 ` Georg Bauhaus
2015-05-07 9:31 ` Georg Bauhaus
2015-05-07 18:32 ` Randy Brukardt
2015-05-08 7:50 ` Dmitry A. Kazakov
2015-05-08 23:31 ` Randy Brukardt
2015-05-09 6:16 ` Dmitry A. Kazakov
2015-05-12 0:28 ` Randy Brukardt
2015-05-12 8:04 ` Dmitry A. Kazakov
2015-05-07 10:06 ` Stefan.Lucks
2015-05-07 12:16 ` Dmitry A. Kazakov
2015-05-07 18:00 ` Stefan.Lucks
2015-05-07 19:01 ` Randy Brukardt
2015-05-07 19:29 ` Niklas Holsti
2015-05-08 23:16 ` Randy Brukardt
2015-05-09 5:18 ` Niklas Holsti
2015-05-12 0:15 ` Randy Brukardt
2015-05-07 19:55 ` Dmitry A. Kazakov
2015-05-08 23:24 ` Randy Brukardt
2015-05-09 5:47 ` Dmitry A. Kazakov
2015-05-07 18:52 ` Randy Brukardt
2015-05-07 19:40 ` Stefan.Lucks
2015-05-08 7:28 ` Dmitry A. Kazakov
2015-05-08 22:58 ` Randy Brukardt
2015-05-08 22:52 ` Randy Brukardt [this message]
2015-05-09 0:14 ` Paul Rubin
2015-05-12 0:30 ` Randy Brukardt
2015-05-12 18:10 ` Paul Rubin
2015-05-12 22:01 ` Randy Brukardt
2015-05-13 9:35 ` Dmitry A. Kazakov
2015-05-13 11:53 ` G.B.
2015-05-13 12:47 ` Dmitry A. Kazakov
2015-05-13 14:06 ` G.B.
2015-05-13 14:21 ` Dmitry A. Kazakov
2015-05-13 16:33 ` G.B.
2015-05-13 19:15 ` Dmitry A. Kazakov
2015-05-14 1:36 ` Randy Brukardt
2015-05-14 7:10 ` Dmitry A. Kazakov
2015-05-14 1:32 ` Randy Brukardt
2015-05-14 7:19 ` Dmitry A. Kazakov
2015-05-12 0:36 ` Randy Brukardt
2015-05-11 10:35 ` Stefan.Lucks
2015-05-11 21:49 ` vincent.diemunsch
2015-05-11 22:49 ` Peter Chapin
2015-05-12 4:49 ` vincent.diemunsch
2015-05-12 23:25 ` Peter Chapin
2015-05-13 9:00 ` vincent.diemunsch
2015-05-12 4:42 ` vincent.diemunsch
2015-05-12 14:53 ` johnscpg
2015-05-13 9:14 ` vincent.diemunsch
2015-05-12 1:03 ` Randy Brukardt
2015-05-12 7:21 ` Georg Bauhaus
2015-05-12 22:08 ` Randy Brukardt
2015-05-12 8:02 ` Georg Bauhaus
2015-05-12 22:14 ` Randy Brukardt
2015-05-12 8:37 ` Stefan.Lucks
2015-05-12 11:25 ` Stefan.Lucks
2015-05-12 18:44 ` Paul Rubin
2015-05-12 20:52 ` Stefan.Lucks
2015-05-18 9:49 ` Jacob Sparre Andersen
2015-05-18 12:10 ` Stefan.Lucks
2015-05-19 7:46 ` Jacob Sparre Andersen
2015-06-09 7:55 ` Stefan.Lucks
2015-06-09 12:02 ` G.B.
2015-06-09 17:16 ` Stefan.Lucks
2015-05-12 18:39 ` Paul Rubin
2015-05-12 20:51 ` Stefan.Lucks
2015-05-12 14:21 ` Bob Duff
2015-05-12 22:37 ` Randy Brukardt
2015-05-13 6:58 ` Georg Bauhaus
2015-05-14 1:21 ` Randy Brukardt
2015-05-07 21:29 ` Georg Bauhaus
2015-05-08 23:11 ` Randy Brukardt
2015-05-08 23:19 ` tmoran
2014-12-23 21:53 ` Florian Weimer
2014-12-24 11:41 ` Brad Moore
2014-12-22 19:38 ` sbelmont700
2014-12-22 19:59 ` Brad Moore
2014-12-22 23:46 ` Randy Brukardt
2014-12-23 10:41 ` Georg Bauhaus
2014-12-22 23:32 ` Randy Brukardt
2015-04-24 17:59 ` Shark8
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox