Re: Assertions in Ada

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

AdaWorks (adaworks@netcom.com) wrote:

: ...
: These could be pragmas in the general form,

:     pragma Require(Entity, Data-type, Boolean-Expression)

I'm not sure what the "Entity" and "Data-type" arguments signify,
but the basic ability to introduce an assertion is supported
in the Ada 95 compilers from GNAT, Aonix, Green Hills, and
Intermetrics (and perhaps others) via:

    pragma Assert(<boolean_expression> [, <string>]);

I would hope that most other Ada 95 vendors now or would
soon support this as well.

This can accomplish many of the same goals as the Eiffel mechanisms,
though it is not associated with a type/class, but rather with a 
particular point in the execution (which is undeniably less powerful).  
A pragma Assert does not support the ability to specify a loop "variant," 
at least not without the programmer adding some extra variables.

Note that during the 9X design we did consider adding more complete
assertion/invariant constructs, but dropped them in the desire to
reduce the overall scope of the revision.

The Eiffel mechanisms are certainly interesting, though I 
believe the class-oriented assertions are in fact a bit 
limiting, in that one must write only assertions that all
subclasses can satisfy.  There is less support for writing assertions
that apply only to a class, but not to its subclasses.  Such 
class-specific assertions make good sense and can help in debugging 
and proving correctness of a particular class, even though they do 
not apply to subclasses.

My biggest complaint about Eiffel (and Java, for that matter), however, 
is that they don't physically separate interface from implementation (except 
via the notion of "deferred" classes).  The normal response is that
you can use a tool to "extract" the interface any time you want,
but that seems to break the whole notion of "design by contract."
I would never go to an implementor and ask them "what is today's
contract?"  The contract should be a separate entity (e.g. the
package spec) which does not "belong" to (and is not extracted from)
either the client or the implementation of the abstraction.
The compiler can then check conformance of an implementation against
its contract.  If you bundle the interface with the implementation,
then there is nothing against which the compiler can check conformance.

It is sort of like answering the question "what does it do?" with the
answer "it does what it does."

I realize that assertions can represent a contract, but the
parameter/result profile is also an important kind of contract
(especially when it includes parameter modes, as it does in Ada).
And if assertions are the only form of separate contract, they
are less useful if they cannot be class-specific, but must
always be constructed in a way that they can apply to any
subclass as well.

: ...
: Richard Riehle
: richard@adaworks.com
: AdaWorks Software Engineering

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