Re: AdaYY; Assertions?

[Lao Xiao Hai <laoxhai@ix.netcom.com>]

Stephen Leake wrote:

> Lao Xiao Hai <laoxhai@ix.netcom.com> writes:
>
> So what is your proposal?

At this point, my proposal is the addition of a pre-, post-, and invariant
capability to the Ada language, similar to that found in Eiffel.   I fully
realize that it is easier to propose something than to figure out how to
make it work.   The general mechanism, as I see it.

Pre-conditions

These could be applied to a subprogram or a data type.   Since data types
already
have the benefit of range constraints and other features of the type model,
this might
be superfluous.  However,  some properties are not as simple as range
constraints.

What happens when a pre-condition fails.  Eiffel has two basic options:
        1) handle and leave scope (as well as potentially propogating)
        2) handle the exception and retry

I personally have a problem with the retry semantics, but it seems to be
effective
with Eiffel.  Not sure about all the implications for Ada.

I do believe that run-time is the wrong place to find a pre-condition
error.   It is too
late in the process.  However,  if the pre-condition error can be detected
at run-time
and corrective action other than an exception handler be taken, perhaps it
has some
virtue.

Post-conditions

Many of the same issues apply as for pre-conditions.   However, what to do
if a post-condition
fails could be quite different, even problematic.

Invariants

These should apply to the type/class.   Invariants should be inherited.
Eiffel allows overriding of the
invariant (they call it something else, but same general effect).

Ada poses another problem.  Should be have an invariant to applies to an
entire package rather than just
a type?   This problem originates in the Ada model of enclosing a type
declaration within a package.

Other problems

It is easy to craft a self-contradictory assertion.   It would be too much
overhead, and probably impossible,
to include some kind of theorem prover in the compiler to detect such
assertions.

Can assertions contribute to safer code?  That is debatable.  Probably some
assertions are inherently more
safe.   But to rely on assertions, for safety-critical software, might pose
some serious considerations.  I realize
that Bertrand Meyer and others who espouse the Design By Contract philosophy
have made a strong case
for the value of assertions in constructing safer software, but I believe
the jury is still out.

Given my doubts, why do I still support the idea.   It seems to me that a
conservative approach to this issue,
for Ada, can have some real benefits.  If we adhere to some of the existing
syntactic rules and some of the
existing semantics of the language, pre-, post-, and invariant conditions
can be subjected to some rigor
during the compile process.   Trivial example, complex boolean expressions
in Ada require parentheses.

I don't want to seem as if I believe this is a simple change to the
language.  Tucker seems to agree with the
general proposition, and he is much smarter about this kind of thing than
I.  There is a need for more
technical input, more ideas, more criticism, before deciding on this
course.   However, it is a serious enough
issue that it deserves our attention.

As I stated earlier, more and more textbooks are publishing algorithms,
examples of classes, and other
pseudocode fragments in which assertions are part of the code.   Ada can
benefit from being more
compatible with those examples, I believe.

Richard Riehle
Lao Xiao Hai