Re: AdaYY; Assertions?

["Robert I. Eachus" <rieachus@earthlink.net>]

Robert A Duff wrote:
 
> The "obvious" thing to do with a precondition failure in the Ada context
> is to raise an exception.  I have thought a lot about how to move this
> checking to compile time -- it's not easy.  The same comments apply to
> the run-time checks that already exist in Ada.

And for the same reason.  Requiring an assertion to be checked and raise
an exception is not problematical, and compilers can and should check as
many as possible at compile time, with warnings.

But in the general case, it is not only not possible to check all
interesting post conditions at compile time, it should be trivially
obvious that you can't always statically determine even that the post
condition will be reached.  (And not just in the case of the halting
problem. ;-)

So I certainly favor allowing more general conditions in assertions,
rather than trying to define a compile time checkable set.  And I think
that current compilers do a pretty good job.  For example, if you need
to assert that a number is even, "pramga Assert(N mod 2 = 0);"