Re: Assertions in Ada

[stt@houdini.camb.inmet.com (Tucker Taft)]

Robert Dewar (dewar@merv.cs.nyu.edu) wrote:

: Jon Anthony says

: <<b) If a) is the expectation, then why was this pragma left out of the
:    standard??  Just hadn't thought of it at the time? (oops that makes
:    3)>>


: It is one thing to stick this into an implementation, quite another to
: formally define what you mean. In particular the whole issue of whether
: the compiler can use the assertion involves some tricky business. We
: found that different people had very different ideas in mind.

: ...

: We could not resolve this issue, so the feature got omitted. It's always
: surprising (especially to those who do not have experience in language
: design) how the simplest appearing things can turn out to be very complex.

Other stumbling blocks to including it in the Standard:

   The safety-critical community seemed generally to prefer methods
   based on separate tools that look from the "outside" to
   verify conditions in the code, without adding anything to
   the generated code in the target machine.  Since we had presumed
   the safety-critical community would have been one of the big
   supporters of the pragma, this lack of interest was a big blow.

   One reviewer felt very strongly that a pragma assert in the
   declarative part should be interpreted as a block-wide invariant,
   rather than as a one-time assertion about the state at the
   point of the pragma.  This further broke the consensus on the meaning
   of the pragma, and when you can't get consensus, it is difficult
   to standardize.

Be that as it may, most "every day" programmers very much like
the notion of a pragma Assert, and I expect to see it widely used,
and presumably therefore widely (universally?) supported.

"Assert" is perfect for a pragma in Ada, because if an implementation 
doesn't support it, it simply ignores it, so the program is still fully
portable.

--
-Tucker Taft   stt@inmet.com   http://www.inmet.com/~stt/
Intermetrics, Inc.  Burlington, MA  USA