Re: Assertions in the Next Ada Standard

[Darren New <dnew@san.rr.com>]

Richard Riehle wrote:
> 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.

Actually, if you wanted to follow the Eiffel model for this, the
invariant would be that the values of the type have to obey the
invariants unless you're running the body of a primitive operation of
that type. That is, if you had something like

type x is new integer;
invariant x /= 0; -- Or whatever syntax
procedure increment(value : in out x) is
begin
  value := value + 1;
  if value = 0 then value = 1; end if;
end increment;

then it would be legal to call increment with a value of -1, and the
first line of increment would not cause an exception.

> 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.

It's really, really difficult to rule out side-effects with
post-conditions. Indeed, some of the hardest post-conditions are those
of side-effects. For example, you do a Put on a file, and the
postcondition is very unlikely to be able to express what that actually
does in terms of future Gets.
 
> 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.

That's generally what they're good for, yes. Like, don't pop empty
stacks, don't real closed files, and stuff like that. Most any
subprogram that raises an exception specific to the package would be
using preconditions instead.
 
> Now to the problems.   First, there is the danger that one might be able to
> construct a self-cancelling boolean expresssion as an assertion. 

Not sure what a "self-cancelling" boolean expression is. You mean a
tautology? Or a negation of a tautology?

> We
> are not very sophisticated in the automated theorem proving in the
> world of computer science, even though there is some progress.

Actually, "we" are. It's just a very difficult problem, with lots of NP
stuff involved.

>   The
> person who constructs an assertion might be tempted to rely on it
> to the exclusion of more careful inspection. 

Indeed. That's part of the point of doing it, at least for
preconditions. If your precondition is "don't pop an empty stack", then
you don't have to implement pop to handle the case of an empty stack.
This is actually a good thing.

Well, not that the person won't "inspect", but that the implementation
will be more straightforward.

>    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".
 
-- 
Darren New 
San Diego, CA, USA (PST). Cryptokeys on demand.
  The opposite of always is sometimes.
   The opposite of never is sometimes.