Re: Assertions in the Next Ada Standard

[Robert A Duff <bobduff@shell01.TheWorld.com>]

Darren New <dnew@san.rr.com> writes:

> >    Second,  in an inheritance
> > scheme, what do we do about either inheriting or overriding a assertion.
> > This problem is non-trivial.   I am not sure I have the answer,  and that
> > is why there is a need for more people thinking about this than we have
> > so far.
> 
> This is pretty well considered in Eiffel, actually. Indeed, the strength
> of Eiffel's "DbC" assertions over those of just inlining boolean checks
> is that they *do* get inherited in the "right way".

The right way for Eiffel, perhaps.  But Ada makes has a distinction
between class-wide and specific types, which is not present in Eiffel,
so the Eiffel rules don't quite translate over to Ada.  I think you
really want *two* preconditions on a dispatching procedure: one that
applies to non-dispatching calls, and one that applies to dispatching
calls.  This is so the specific type can provide a stronger contract
than is provided by the whole class.  Same for post-cond.

The Eiffel rules are certainly a good starting point.  But it would
require some thought to translate them into the Ada world.

- Bob