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.1 required=5.0 tests=BAYES_00,
	PP_MIME_FAKE_ASCII_TEXT autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,595c75298fbdce96
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news1.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!newsfeed.straub-nv.de!nuzba.szn.dk!news.jacob-sparre.dk!pnx.dk!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Is Aunit helpful?
Date: Mon, 16 Aug 2010 21:46:23 -0500
Organization: Jacob Sparre Andersen
Message-ID: <i4ct62$ahf$1@munin.nbi.dk>
References: 
 <8a1e58c0-2330-4475-8013-97df103dd85e@o19g2000yqb.googlegroups.com>
 <82r5ids1o9.fsf@stephe-leake.org>
 <daea94be-eb3a-4984-a6de-0b68225e3139@o19g2000yqb.googlegroups.com>
 <20100805211820.52c18cb5.tero.koskinen@iki.fi>
 <8d166cfb-4850-42b6-ac25-d9ac00df7565@q35g2000yqn.googlegroups.com>
 <op.vhdx2hsoule2fv@garhos> <82ocd5wukf.fsf@stephe-leake.org>
 <3957496a-af4b-45f5-87c9-327b22d19f08@x21g2000yqa.googlegroups.com>
 <82eie0vzyd.fsf@stephe-leake.org>
 <32dc1191-0a83-40ef-8bbc-a13a06f2167e@u26g2000yqu.googlegroups.com>
 <op.vhh4slqeule2fv@garhos>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: munin.nbi.dk 1282013187 10799 69.95.181.76 (17 Aug 2010 02:46:27 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Tue, 17 Aug 2010 02:46:27 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.5931
X-RFC2646: Format=Flowed; Response
Xref: g2news1.google.com comp.lang.ada:13444
Date: 2010-08-16T21:46:23-05:00
List-Id: <comp.lang.ada>

"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message 
news:op.vhh4slqeule2fv@garhos...
Le Sun, 15 Aug 2010 23:47:21 +0200, Midoan <midoan.ses@gmail.com> a �crit:
...
> 3) About point #1, just wanted to say I don't want here to discourage 
> people interested in pre-post introduced in Ada 2012, to use it. No-no-no, 
> if they enjoy this, this is very good, and this will lead them to a good 
> way. Just wanted to say what should not be hidden: this is weak, as this 
> is more a step above comments. I was to say "this is just like  comments"... 
> but honestly, comment are not checked at all, so these  pre-post may be 
> viewed as "Better Comments".

Not so much "Better Comments", but "automatic pragma Asserts". I don't 
disagree with your point, but Pre/Post are better than pragma Assert in two 
ways:

(1) Pre and Post are automatically added to every call site; it's not 
possible to forget to put in a needed Assert;

(2) Pre and Post are in the specification, and thus are visible to the 
callers. That allows both the Ada compiler and other tools to do static 
analysis. The Ada compiler may be able to prove that the precondition cannot 
fail (and thus eliminate the overhead); other tools may be able to do even a 
better job. That is, well-written preconditions and postconditions can be 
statically proved. (The Ada 2012 language won't require that, because its 
beyond the state-of-the-art today to be able to decide which ones can be 
proved and which ones cannot. But I hope that we can do better in the 
future.)

Pre and Post hopefully will provide a foundation where compilers will make 
at least some of these checks statically.

                           Randy.