Re: Assertions in the Next Ada Standard

[FGD <presbeis@look.ca>]

Ah! I see now that your proposal is deeper than what I originally 
thought it was. I see also that it does addresses some very real issues 
of Ada.

As you point out yourself, when it comes to incorporating them in the 
current Ada framework, invariants and pre-/post-conditions are quite 
different. Invariants are connected to types whereas conditions pertain 
to subprograms and their parameters. Consider dividing it in two related 
proposals to avoid opposition to one reject the other.

  Invariants constitute a "type improvement" as I would have said in my 
first reply. As such they are desirable, they provide a nice way of 
defining disconnected ranges and imposing constraints on type 
discriminants for example. Safety is an issue, but we know enough to 
work around it. The sublanguage of assertions should be constrained so 
that it cannot describe conditions which are not polytime---we know how 
to do that. More severe restrictions will probably be imposed, and very 
severe restrictions should apply if some kind of non-static assertions 
are to be allowed. Since the sublanguage of assertions should contain 
boolean variables and all propositional connectives, the problem of 
deciding whether or not a particular assertion is ever true is 
NP-complete. Thus one cannot reasonably expect compile time warnings for 
all such conditions. Some may object to that, but I consider this to be 
the programmer's problem.

 From my perspective, invariants have many merits. The most important is 
that it provides a uniform way of implementing all the type improvements 
I ever thought of in a uniform way. I'm still not sure about 
pre-/post-conditions. Right now, it seems to me that the associated 
complexities outnumber the benefits and I'm still curious about 
practical applications...

-- Frank