Re: Assertions in the Next Ada Standard

[Richard Riehle <richard@adaworks.com>]

FGD wrote:

> Richard Riehle wrote:
>
> > I am hoping to see something like pre-conditions, post-conditions,
> > and invariants in the next revision of Ada.  I would be pleased if
> > we simply adopted the wording already used in Eiffel:  require,
> > ensure, and invariant, but I am not intractable about the terminology.

> For suprograms, this doesn't seem essential because of Ada's strong
> typing. It may however be very useful for loops and related constructs.
> But I can find *weak* replacements within Ada. For invariants, enclose
> loops in a block statement, e.g.

I have snipped the corresponding code for sake of economy.

For greatest benefit, the pre-conditions, post-conditions and invariants
would be declared in the package specification.   The does not preclude
declaring some in subprograms, but that is not my focus, at present.

Taking the invariant, first.    At present, there is no construct in Ada
that
is package-wide or type-wide except the type declaration itself.   All that
one can do with a type declaration is declare a range or a set of
operations.
OK, one can do a little more, but that is beside the point.

For a type, an invariant declaration simply adds some additional rules
for that type.    For example, one cannot declare a discontinous range
for a numeric type, but an invariant might state that a value of that
numeric type cannot ever be zero.   This would be stated (asserted)
in the package specfication.   For other types, boolean expressions
could be declared that would further constrain a type with a more
rigorous invariant.

I will address the problem with this a little later in this posting.

Pre-conditions and post-conditions would be part of the declaration of
each subprogram.   Post-conditions are particularly worthwhile because
there is, for access to composite type parameters,  potential for
side-effects
that might be unknown to the client of a specification.   A post-condition
can guarantee there are no unchecked side-effects.

Pre-conditions might be less useful given many of the controls already
in place for parameter lists in subprograms.    However, one might declare
a pre-condition that prevents a subprogram from executing if some
combination of parameters is invalid.

Now to the problems.   First, there is the danger that one might be able to
construct a self-cancelling boolean expresssion as an assertion.  We
are not very sophisticated in the automated theorem proving in the
world of computer science, even though there is some progress.   The
person who constructs an assertion might be tempted to rely on it
to the exclusion of more careful inspection.     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.

In a later post, one beyond this one in chronology, Dr. Dewar makes a
good point.   He announces that within in his customer base, there has
been very little interest in this feature.   Given some of the other
postings
I have seen so far, I am not surprised since it does not seem to be a
well-understood concept within the larger Ada community.  Certainly,
many who frequent this forum do understand it and I would expect
people such as Robert Duff to weigh in with well-reasoned criticisms.
The fact that there is very little demand for assertions might be said
of other seldom used and little understood features already in the language.

I would like to see us engage in dialogue about this idea in terms of
its intrinsic merits and and potential for harm rather than depend on the
immediate demand of the day-to-day current Ada practitioner.

Richard Riehle