Re: Silly and stupid post-condition or not ?

[Robert A Duff <bobduff@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.

>...(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.

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.

- Bob