Assert pragma

Assert pragma

[Robert C. Leif]

The following is from 03-06-23  AI95-00286/04.  Evidently the status is a
work item for Ada 0Y

The following configuration pragma is defined:

    pragma Assertion_Policy(assertion_policy_identifier);

    assertion_policy_identifier ::=
        Check
      | Ignore
      | implementation-defined-assertion_policy

Since at SIGAda 2003 SPARK was demonstrated to be a useful and potentially
the killer technology for Ada, it would be prudent to include the
possibility of enhancing Ada to do the equivalent of SPARK.  Since SPARK is
a compile time tool that heavily uses assertions, Ada 0Y should include a
standardized means to call compile time assertions.  However as far as I
know, compile time assertions have never been implemented in a standard Ada
compiler.  Therefore, the syntax for this option should be specified and the
implementation should NOT be required.  The possibilities should be expanded
in Assertion_Policy: Run_Check, Compile_Check, and Run_And_Compile_Check.
The new definition would be:

pragma Assertion_Policy(assertion_policy_identifier);

    assertion_policy_identifier ::=
        Run_Check
      | Compile_Check
      | Run_And_Compile_Check 
      | Ignore
      | implementation-defined-assertion_policy