comp.lang.ada
 help / color / mirror / Atom feed
From: "Randy Brukardt" <randy@rrsoftware.com>
Subject: Re: Silly and stupid post-condition or not ?
Date: Mon, 6 Feb 2012 19:46:55 -0600
Date: 2012-02-06T19:46:55-06:00	[thread overview]
Message-ID: <jgpvqi$71b$1@munin.nbi.dk> (raw)
In-Reply-To: wccobtdfgz9.fsf@shell01.TheWorld.com

"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message 
news:wccobtdfgz9.fsf@shell01.TheWorld.com...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>
>> The postcondition (and precondition) moves this "contract" information to
>> where it belongs (on the specification).
>
> Right.  That's what makes a precondition better than simply putting
> a pragma Assert at the start of the procedure body.
>
>>... That allows the compiler to take
>> advantage of that information, and in many cases completely eliminate the
>> associated checks (just like the compiler can eliminate a large 
>> proportion
>> of constraint checks). Like constraint checks, well-written contracts 
>> should
>> never need to be turned off...
>
> I don't agree.  There are definitely cases when constraint checks
> should be turned off.  Likewise preconditions.  If you say
> "Never turn off checks", you're really saying "Never write
> an assertion that is too expensive in production, even
> though it might be helpful in testing and debugging",
> which is clearly counter-productive.

I would indeed argue that. More accurately, what I would argue is that any 
assertion that is too expensive to "use in production" be kept completely 
separate from the rest, and I'd suggest that it generally be turned off 
(unless absolutely needed).

I've done this in my programs by simply commenting them out; they're only 
inserted when the problem that they are intended to detect shows up a second 
time. (That doesn't happen much.) I could see using some other mechanism to 
keep them separate; possibly going so far as to using a dynamic method to 
turn them on or off.

This has always been one of my biggest complaints with Assertions; all or 
nothing is insufficient control; it's bad enough that I've never seen any 
real value to pragma Assert. (I'd rather use if statements controlled from a 
global package than to use a single compiler switch for such detection.)

>>...(as always, it's like taking off the seatbelts
>> when you leave the garage...).
>
> I don't buy this analogy (nor the similar one about life jackets and
> sailboats).  Seatbelts often save lives and reduce injuries
> when something goes wrong.  Preconditions (etc) don't cause
> programs to give correct answers when something goes wrong
> -- they just detect the wrongness.

Turning off constraint checks make a program erroneous, and thus the program 
can return wrong answers without any notice. Back in the CP/M/MS-DOS-1 days, 
we used to have this problem a lot, especially by accessing non-existent 
variants. And a lot of those problems only showed up in production.

Today, this sort of thing is a security problem - constraint checks at least 
bound the problem to at worse a denial-of-service problem, much less of a 
problem than allowing a buffer overflow that allows anything to be executed.

I admit that is less of a problem for preconditions and the like, but I 
think the same holds true -- particular if the correctness checks were 
removed from the code in favor of the preconditions.

> By the way, I find that when I (at first) think I want a
> pre/post, it's usually better expressed as a subtype predicate.
> My favorite new feature of Ada 2012.

I agree. I originally thought that predicates were a better solution to the 
problem than pre/post/invariants. I still do for most uses, but of course 
whenever multiple parameters are involved you have to use a precondition 
instead.

                                                 Randy.





  parent reply	other threads:[~2012-02-07  1:46 UTC|newest]

Thread overview: 84+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2012-01-30 23:11 Silly and stupid post‑condition or not ? Yannick Duchêne (Hibou57)
2012-01-31  6:47 ` J-P. Rosen
2012-01-31 18:48   ` Jeffrey Carter
2012-01-31 22:02     ` Yannick Duchêne (Hibou57)
2012-01-31  8:54 ` Dmitry A. Kazakov
2012-01-31  9:35   ` Georg Bauhaus
2012-01-31 10:22     ` Dmitry A. Kazakov
2012-01-31 12:33       ` Georg Bauhaus
2012-01-31 13:52         ` Dmitry A. Kazakov
2012-01-31 15:34           ` Georg Bauhaus
2012-01-31 16:24             ` Dmitry A. Kazakov
2012-01-31 19:44               ` Georg Bauhaus
2012-02-01  8:41                 ` Dmitry A. Kazakov
2012-02-01 10:37                   ` stefan-lucks
2012-02-01 10:51                     ` Yannick Duchêne (Hibou57)
2012-02-01 13:49                     ` Yannick Duchêne (Hibou57)
2012-02-01 13:49                     ` Dmitry A. Kazakov
2012-02-01 16:37                       ` stefan-lucks
2012-02-02  1:50                         ` Silly and stupid post�?'condition " Randy Brukardt
2012-02-02  1:56                           ` Silly and stupid postâ?'condition or not ? Yannick Duchêne (Hibou57)
2012-02-03  2:45                             ` Silly and stupid post�?'condition or not ? Randy Brukardt
2012-02-02  8:25                         ` Silly and stupid post‑condition " Dmitry A. Kazakov
2012-02-02  9:01                           ` stefan-lucks
2012-02-02  9:18                           ` stefan-lucks
2012-02-02 10:04                             ` Dmitry A. Kazakov
2012-01-31 22:08         ` Yannick Duchêne (Hibou57)
2012-01-31 17:28 ` Dmitry A. Kazakov
2012-01-31 22:12   ` Yannick Duchêne (Hibou57)
2012-02-01  8:49     ` Dmitry A. Kazakov
2012-02-01  8:36 ` Stephen Leake
2012-02-01 16:30   ` Silly and stupid post-condition " Adam Beneschan
2012-02-02  9:40     ` Stephen Leake
2012-02-02 13:20       ` Georg Bauhaus
2012-02-02 13:35         ` Yannick Duchêne (Hibou57)
2012-02-03  3:13       ` Randy Brukardt
2012-02-03  3:33         ` Yannick Duchêne (Hibou57)
2012-02-03  8:12         ` Simon Wright
2012-02-07  2:29           ` BrianG
2012-02-07 10:43             ` Simon Wright
2012-02-08  2:25               ` BrianG
2012-02-07 21:15             ` Robert A Duff
2012-02-03  9:11         ` Dmitry A. Kazakov
2012-02-04  3:27           ` Randy Brukardt
2012-02-04 10:15             ` Dmitry A. Kazakov
2012-02-03 12:25         ` Phil Thornley
2012-02-04  9:30         ` Phil Thornley
2012-02-04 12:02         ` Phil Thornley
2012-02-05  6:18           ` Randy Brukardt
2012-02-05 10:23             ` Phil Thornley
2012-02-05 10:55               ` Yannick Duchêne (Hibou57)
2012-02-05 15:03               ` Robert A Duff
2012-02-05 18:04                 ` Phil Thornley
2012-02-05 21:27                   ` Robert A Duff
2012-02-05 23:09                     ` Phil Thornley
2012-02-07  2:05               ` Randy Brukardt
2012-02-07  9:38                 ` Dmitry A. Kazakov
2012-02-05 11:31             ` Yannick Duchêne (Hibou57)
2012-02-05 14:50             ` Robert A Duff
2012-02-07  2:11               ` Randy Brukardt
2012-02-07  2:34             ` BrianG
2012-02-07  4:38               ` Yannick Duchêne (Hibou57)
2012-02-09  3:10               ` Randy Brukardt
2012-02-04 23:07         ` Stephen Leake
2012-02-05  2:49           ` Yannick Duchêne (Hibou57)
2012-02-05  6:29           ` Randy Brukardt
2012-02-05 11:40             ` Yannick Duchêne (Hibou57)
2012-02-07  1:36               ` Randy Brukardt
2012-02-05 15:16             ` Robert A Duff
2012-02-06  4:56               ` Yannick Duchêne (Hibou57)
2012-02-06 14:39                 ` Robert A Duff
2012-02-06 16:12                   ` Yannick Duchêne (Hibou57)
2012-02-07  1:46               ` Randy Brukardt [this message]
2012-02-07 17:24                 ` Robert A Duff
2012-02-03  6:26       ` J-P. Rosen
2012-02-03  9:12         ` Dmitry A. Kazakov
2012-02-03  9:48           ` Yannick Duchêne (Hibou57)
2012-02-03 11:09             ` Dmitry A. Kazakov
2012-02-03 11:40               ` Yannick Duchêne (Hibou57)
2012-02-03 13:18                 ` Dmitry A. Kazakov
2012-02-03 14:14                   ` Yannick Duchêne (Hibou57)
2012-02-03 14:45                     ` Dmitry A. Kazakov
2012-02-04  3:16           ` Randy Brukardt
2012-02-04  6:27             ` Yannick Duchêne (Hibou57)
2012-02-04 10:47             ` Dmitry A. Kazakov
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox