Re: Assertions in Ada

[dewar@merv.cs.nyu.edu (Robert Dewar)]

Brian says

<<This decision seems exactly right to me, though for a different reason. It
isn't clear to me that there is enough consensus on formal (in the sense of
"mathematically formal") programming methodologies to consider choosing a
set of constructs to put in the language proper. It makes more sense to
let people experiment with tools/notations/methods like Anna, Larch, Z, B,
and others. So IMO, Ada got this right, and Eiffel got it wrong, just like
Eiffel got modules wrong.>>

I basically agree. I think it useful to have the simple minded Assert
that is provided in GNAT (and several other compilers have copied this,
as Tuck notes). This assert is not some kind of wonderful silver bullet
that will make all Ariane-like problems disappear, but it is a useful
tool, as has been well known by programmers for longer than I can
remember. The GNAT compiler itself for instance is full of assertions,
and they have been invaluable in 

   (a) avoiding silent generation of wrong code, the most heinous
       crime a compiler can commit.

   (b) speeding up the tracking of errors

GNAT is now at the point where it is stable enough that it makes sense
to turn off these assertions for the production version, and we intend
to do this in version 3.11 of GNAT -- our experiments show that (a) is
no longer a significant concern, and we will still keep the assertions
around to help with (b) -- one of the handy things about the pragma
Assert is that it can be externally activated (the -gnata switch in GNAT).

But I agree that putting in anything formal or elaborate would have been
premature. What would be nice to see is people experimenting with possible
interesting annotations, etc with GNAT. 

(by the way, if you want to experiment with the fast version of GNAT, with
assertions off, you can do it yourself, by rebuilding the compiler with
the -gnatn switch on and the -gnata switch omitted :-)