From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,ad06d2d7cb045687
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.74.201 with SMTP id w9mr4126476pbv.0.1328454987676;
        Sun, 05 Feb 2012 07:16:27 -0800 (PST)
Path: 
 lh20ni263551pbb.0!nntp.google.com!news2.google.com!newsfeed2.dallas1.level3.net!news.level3.com!bloom-beacon.mit.edu!newsswitch.lcs.mit.edu!nntp.TheWorld.com!not-for-mail
From: Robert A Duff <bobduff@shell01.TheWorld.com>
Newsgroups: comp.lang.ada
Subject: Re: Silly and stupid post-condition or not ?
Date: Sun, 05 Feb 2012 10:16:26 -0500
Organization: The World Public Access UNIX, Brookline, MA
Message-ID: <wccobtdfgz9.fsf@shell01.TheWorld.com>
References: <op.v8w6ptk5ule2fv@douda-yannick>
 <82wr86fzos.fsf@stephe-leake.org>
 <5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com>
 <82k445fu9n.fsf@stephe-leake.org> <jgfjc4$u4b$1@munin.nbi.dk>
 <82ty36urik.fsf@stephe-leake.org> <jgl7k6$lp1$1@munin.nbi.dk>
NNTP-Posting-Host: shell01.theworld.com
Mime-Version: 1.0
X-Trace: pcls6.std.com 1328454987 13339 192.74.137.71 (5 Feb 2012 15:16:27
 GMT)
X-Complaints-To: abuse@TheWorld.com
NNTP-Posting-Date: Sun, 5 Feb 2012 15:16:27 +0000 (UTC)
User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix)
Cancel-Lock: sha1:oDAWdGbS0xXY2DcxEUikrjtWNXg=
Content-Type: text/plain; charset=us-ascii
Date: 2012-02-05T10:16:26-05:00
List-Id: <comp.lang.ada>

"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