comp.lang.ada
 help / color / mirror / Atom feed
From: "Randy Brukardt" <randy@rrsoftware.com>
Subject: Re: Is Aunit helpful?
Date: Mon, 16 Aug 2010 21:46:23 -0500
Date: 2010-08-16T21:46:23-05:00	[thread overview]
Message-ID: <i4ct62$ahf$1@munin.nbi.dk> (raw)
In-Reply-To: op.vhh4slqeule2fv@garhos

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1716 bytes --]

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





  reply	other threads:[~2010-08-17  2:46 UTC|newest]

Thread overview: 45+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2010-08-04 14:19 Is Aunit helpful? Ada novice
2010-08-05 12:07 ` Stephen Leake
2010-08-05 17:29   ` Ada novice
2010-08-05 18:18     ` Tero Koskinen
2010-08-05 20:39       ` Ada novice
2010-08-05 20:57         ` Simon Wright
2010-08-13 16:43         ` Yannick Duchêne (Hibou57)
2010-08-13 19:34           ` Simon Wright
2010-08-13 20:59             ` Yannick Duchêne (Hibou57)
2010-08-14  6:57           ` Stephen Leake
2010-08-14 13:38             ` Yannick Duchêne (Hibou57)
2010-08-14 21:33             ` Midoan
2010-08-14 21:38               ` Yannick Duchêne (Hibou57)
2010-08-14 21:49                 ` Simon Wright
2010-08-14 22:04                   ` Yannick Duchêne (Hibou57)
2010-08-15  7:57                 ` Midoan
2010-08-15 11:46                   ` Simon Wright
2010-08-15 12:10               ` Stephen Leake
2010-08-15 21:47                 ` Midoan
2010-08-15 22:58                   ` Yannick Duchêne (Hibou57)
2010-08-17  2:46                     ` Randy Brukardt [this message]
2010-08-17 12:37                       ` Cyrille
2010-08-20  9:22                         ` Yannick Duchêne (Hibou57)
2010-08-20  9:20                       ` Yannick Duchêne (Hibou57)
2010-08-16  7:59                   ` Stephen Leake
2010-08-16  9:02                     ` Midoan
2010-08-26 17:45                       ` Colin Paul Gloster
2010-08-07 16:57       ` Marco
2010-08-13 14:09       ` Yannick Duchêne (Hibou57)
2010-08-05 20:48     ` Simon Wright
2010-08-06  9:06       ` Ada novice
2010-08-06 16:51         ` Simon Wright
2010-08-06 18:13           ` Ada novice
2010-08-08 13:39 ` John McCormick
2010-08-08 17:10   ` Ada novice
2010-08-09 17:05     ` John McCormick
2010-08-09 17:23       ` Michael R
2010-08-10  8:33         ` Ada novice
2010-08-10 13:48           ` John McCormick
2010-08-10  9:45       ` Mark Lorenzen
2010-08-10 14:07         ` John McCormick
2010-08-10 17:32       ` Ada novice
2010-08-12 15:04         ` John McCormick
2010-08-17 15:51           ` Ada novice
2010-08-13 15:31 ` Yannick Duchêne (Hibou57)
replies disabled

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