Re: Assertions

["Nick Roberts" <nickroberts@callnetuk.com>]

I would suggest that a pragma Assert expands to something like the
following:

   if not boolean_expression then
      Ada.Exceptions.Raise_Exception(
         Ada.Assertions.Assert_Failure'Identity,
         "Test expression evaluated to False in a pragma Assert." & NL &
         "Page: " & Page & "Line: " & Line & NL &
         "File: " & Source_File_Name & NL &
         [""|string_expression]);
    end if;

where NL is the implementation's code for a line break. Then there should be
a package:

package Ada.Assertions is

   Assert_Failure: exception [renames lower_level_exception];

end;

I think it's also got to be made explicit that if a pragma Assert in the
place of a declaration---in the declarative region of a certain
block---raises an exception, that exception must be immediately propagated
out of the block (and can never be handled inside the block). I would also
suggest the following points.

1. There's no reason why the compiler should not be able to assume that any
assertion's condition holds true, regardless of whether assertion checking
is turned on or off. This would obviously be highly desirable, since, in
many cases, it would allow optimising compilers to make optimisations they
otherwise could not. The situation is analogous to other checks: if a check
is turned off, and consequently an exception fails to be raised, the
program's behaviour is undefined, and possibly highly erratic; if
Assertion_Check is on (the default) the failure of an assertion's condition
will always raise an exception (so the condition will certainly always hold
as a post condition).

2. I don't see why assertions should not be allowed to have side-effects.
Whether it would be wise, in practice, for an assertion to have side effects
is another matter (to be left to the 'wisdom' of the programmer ;-).

3. If Assertion_Check is turned off, but the compiler can nevertheless
detect (at compile time) that an assertion's condition will always fail (be
False), it should still be entitled to raise an exception. Again, this is
analogous to the other checks. In theory, the compiler should be entitled to
continue checking any assertions it fancies.

4. A pragma Assert must not be evaluated by the elaboration of a
preelaborated library unit.

-------------------------------------
Nick Roberts
-------------------------------------