Re: Assertions

[Tucker Taft <stt@averstar.com>]

Ehud Lamm wrote:
> 
> On Fri, 21 May 1999, Robert Dewar wrote:
> 
> > But to think that Ada dismissed DBC just because it did not
> > adopt the particular partial assertion language facilities
> > of Eiffel misses the point I think.
> >
> >
> Sure.
> 
> But still two points.
> 1) I was responding to a claim that the issue of DBC was dicussed in the
> Ada95 design process. I just wondered whether any documents from this
> dicussion may be available.

We discussed associating assertions with types.  We didn't "dismiss"
them, but rather decided at the time they were too complex for the
perceived benefit.  We came quite close to standardizing on a
pragma Assert, and in fact most Ada 95 compilers have implemented
such a pragma.  Whether we can get it officially standardized over
the next few years, or just "de facto" standardized remains to be seen.

> 2) I think having language support for DBC is a good thing. (I am not
> advoacting Eiffel, just the general claim.) It is much cleaner, more
> readable and most reliable to declare some set of assertions as being the
> invariant of an ADt, than to explicitly code a check for them at the end
> (etc.) of each routine that updates the ADT. Don't you agree?
> Sure, language support is not essential for DBC. But I think it has many
> advantages.

Bertrand Meyer has a very specific definition of design by contract
which he associates closely with the Eiffel assertions/invariants.

Ada certainly has linguistic support for design by contract in 
general, though not in the same way as Eiffel.  In particular, every
subtype constraint in Ada is a contract that is enforced at run-time.
In addition, the fact that Ada physically separates spec from body,
and visible part from private part, creates a number of very well-defined
and configuration-manageable "contracts" that are compiler enforced.
Personally, I find one of the greatest weaknesses of Eiffel (and Java) is
that classes do not provide this physical separation into spec and body.
The notion that you "extract" the spec from a class is counter to the
idea that you have a well-defined contract.  The contract is much stronger
if it is physically separate from the implementation.  In a business
contract, I would never allow the supplier to be the "keeper" of the
contract, where I would have to ask the supplier to "extract" the
contract from the current implementation.

None of the above is meant to say I don't see the value in assertions
and invariants.  However, I think in practice, the support that Ada
already has for contracts is in many ways more valuable on a "day-to-day"
basis, because the range constraints (and other constraints) are ubiquitous
in a typical Ada program, providing contract enforcement on a line-by-line
basis and at every subprogram call, and the physical separation of
spec and body is valuable in every package. I would certainly 
not want to trade Ada's existing support for "contracts" for just 
having the explicit assertions provided by Eiffel.  
I would want both.  The pragma Assert generally available
in Ada compilers already provides a good portion of the power of
explicit assertions and invariants. 

> Ehud Lamm     mslamm@pluto.mscc.huji.ac.il

-- 
-Tucker Taft   stt@averstar.com   http://www.averstar.com/~stt/
Technical Director, Distributed IT Solutions  (www.averstar.com/tools)
AverStar (formerly Intermetrics, Inc.)   Burlington, MA  USA