Version 1.7 of ais/ai-00286.txt

Unformatted version of ais/ai-00286.txt version 1.7
Other versions for file ais/ai-00286.txt

!standard 11.5 (00)          03-03-05 AI95-00286/04
!standard 11.4.1 (10)
!class amendment 02-02-05
!status work item 02-02-05
!status received 02-02-05
!priority Medium
!difficulty Medium
!subject Assert pragma
!summary
A standard "assert" pragma is proposed which takes a boolean expression and an optional string and raises Ada.Assertions.Assertion_Error if the expression evaluates to false. To control how the pragma is handled in the generated code, a configuration pragma "Assertion_Policy" is defined.
!problem
Several Ada compilers support an "assert" pragma, in largely the same form. This AI proposes to standardize the pragma, an associated package, and an associated configuration pragma for controlling the effect of the pragma on the generated code.
It anticipates proposals for additional assertion-like pragmas for subprogram call pre and post conditions, and type and package oriented invariants. These will be discussed in separate AIs.
!proposal
The form of the pragma Assert is as follows:
pragma Assert(boolean_expression[, [Message =>] string_expression]);
A pragma Assert is allowed at the place where a basic_declaration or a statement is allowed.
The package Ada.Assertions is as follows:
package Ada.Assertions is pragma Pure(Ada.Assertions);
Assertion_Error : exception; -- This exception is raised by an assertion check that fails
procedure Assert(Check : in Boolean; Message : in String := ""); -- Calling this procedure has no effect if Check is true. -- It raises Assertion_Error if false, with the associated -- exception message if non-null. end Ada.Assertions;
[Should we add the following (though how could you tell)?
A compilation unit with an Assert pragma has a semantic dependence on the Ada.Assertions library unit.]
The following configuration pragma is defined:
pragma Assertion_Policy(assertion_policy_identifier);
assertion_policy_identifier ::=
Check
| Ignore | implementation-defined-assertion_policy
An Assertion_Policy pragma is a configuration pragma that specifies the assertion policy in effect for the compilation units to which it applies. Different policies may pertain to different compilation units within the same partition.
An assertion policy specifies how an Assert pragma is interpreted by the implementation. If the assertion policy is "Ignore" at the point of an Assert pragma, the pragma is ignored. If the assertion policy is "Check" at the point of an Assert pragma, the elaboration of the pragma consists of evaluating the boolean expression, and if it evaluates to False, evaluating the Message string, if any, and raising the exception Ada.Assertions.Assertion_Error, with a message if the Message argument is provided.
Other implementation-defined assertion policies might be introduced to specify that the compiler should perform static analysis presuming the assertions are true, even if code for the assertions is suppressed (i.e. it would be erroneous if they are false). These have not been standardized because specifying their semantics portably is problematic (and a bit controversial, to be honest).
Calling the procedure Ada.Assertions.Assert is equivalent to:
if Check = False then
Ada.Exceptions.Raise_Exception(
Ada.Assertions.Assertion_Error'Identity, Message);
end if;
except that it can be called from Pure code. The procedure Assert has these effects independent of the assertion policy in effect.
The form of the representation pragma Assertions_Only is as follows:
pragma Assertions_Only(local_name);
If an Assertions_Only pragma applies to a declaration, then it also applies to the completion of the declaration, and any declarations declared within the declarative region, if any, associated with the declaration.
A declaration to which Assertions_Only applies may only be referenced within an assertion pragma, or within another construct to which the Assertions_Only pragma applies. Pragma Assert is an assertion pragma. Other language- and implementation-defined pragmas may be identified as being assertion pragmas.
NOTE: The boolean expression in an Assert pragma should normally not
call functions that have side-effects (or at least, not when the result of the expression is True) so that the particular assertion policy in effect will not affect normal operation of the program.
Implementation Permission
Assertion_Error may be declared by renaming an implementation-defined exception from another package.
Implementation Advice
When an assertion policy of Ignore applies to all compilation units with visibility on a construct to which Assertions_Only applies, storage space occupied by the construct should be minimized in the executable program.
!wording
!discussion
This AI attempts to standardize the Assert pragma already supported by various implementations. The package and exception name are probably not the same as any existing implementation, but presumably exception and subprogram renaming can be used to provide backward compatibility.
There was some concern expressed about the word "Assert" as implying an orientation toward static analysis, as opposed to run-time checking. However, there is a significant history of using "assert" for run-time checking in programming languages (cf. C, C++, Java, Eiffel), and a number of existing Ada compilers have adopted the term as well, so it seems that that "cat" is already well out of the "bag."
We considered using pragma Suppress to control the affect of the Assert pragma, but it was felt that this could lead to confusion, as pragma Suppress can always be ignored by the implementation, whereas one possible desired interpretation for pragma suppress of assertions is that they are certain to be completely ignored.
The configuration pragma approach gives more flexibility, and allows the user to be explicit as to how the pragmas are to be interpreted. For those wanting run-time checking, Check makes the most sense. Ignore ensures that adding an Assert pragma can never make the program less safe. Other implementation-defined policies can be defined which might be more oriented toward static analysis.
We originally proposed two other language-defined assertion policies, Assume_True and Evaluate_And_Assume_True. However, these both could result in erroneous execution, and might not match what would be most useful for static analysis in any case, hence we leave it to implementations to provide other policies as they see fit. Because configuration pragmas can be separated off into a single file, having implementation-defined policies should not endanger the portability of the bulk of an application that uses Assert pragmas.
We have provided a procedure Assert as well, as it is something that could be used on compilers that don't yet support the pragma, and it eliminates any possibility of the assertion policy affecting the operation of the program.
We have provided a pragma Assertions_Only to address the concern that to make assertion pragmas most valuable, additional operations or objects may need to be defined. This pragma ensures that these additional constructs are only referenced from within assertion pragmas or other Assertions_Only constructs. Implementations are encouraged to minimize storage occupied by such constructs if assertion policy Ignore applies to all compilation units with visibility on the construct. Note that there is no permission to eliminate elaboration of such constructs or the side-effects associated with this elaboration. However, an implementation-defined assertion policy might be used to control aspects of Assertion_Only constructs further.
Here are comments on other issues identified by the HRG:
1) Limitations on expressiveness
We believe that Ada is fully capable of expressing almost anything of interest. The System_Of_Units AI provides some examples of using pragma Assert with relatively sophisticated expressions. However, we realize it may be necessary to introduce additional variables or functions. We believe that the Assertions_Only pragma can be used to identify clearly these additional variables or functions, and to enable the implementation to minimize storage devoted to them when assertions are being ignored.
Specific mention is made of implication and quantifiers. Both of these can be readily defined in Ada: Implication can be defined using a rename:
function Implies(A, B : Boolean) return Boolean renames "<=";
Quantification would require defining appropriate functions, perhaps with the help of appropriate generics. Again, the Assertions_Only pragma could be used if storage space were a concern.
2) The possibility of side-effects.
This seems entirely within the programmers control. By judicious use of pragma Pure, this problem can be minimized. An additional policy could be defined which required all expressions in a pragma Assert to be pure.
3) The use of exceptions.
Exceptions are the way in which errors are signaled in Ada. Yes it is possible to catch them by mistake by using "when others," but that is as true for Constraint_Error as it is for Assertion_Error. Clearly in an high-integrity system, there is often a desire to eliminate all exceptions. This is generally done by certifying either statically or through heavy testing that the exceptions will not be raised. An advantage of pragma Assert is it allows the programmer to specify explicit checks that are treated essentially like the language-defined checks, and would require the same level of proof.
4) The use of the word "assert."
That was discussed above.
One main underlying objection seems to be that the pragma Assert might not be terribly useful for high-integrity systems. Although we believe that they can be just as useful as the language-defined run-time checks, namely they provide a set of additional explicit "checks" which must be "proved" safe by testing or analysis, we don't believe that pragma Assert should go in annex H. We believe it is a generally useful capability, that is already in wide use, and should be standardized, and probably defined somewhere in chapter 11 (exceptions).
!example
!ACATS test
!appendix

From: Robert Dewar
Sent: Wednesday, February 6, 2002, 2:40 PM

I doubt we would implement this in its suggested form, because it is very
close to what we have but arbitrarily different, and I would see no reason
to disconcert our existing customers who use this feature with such small
changes. The package in GNAT is:

package System.Assertions is

   Assert_Failure : exception;
   --  Exception raised when assertion fails

   procedure Raise_Assert_Failure (Msg : String);
   pragma No_Return (Raise_Assert_Failure);
   --  Called to raise Assert_Failure with given message

end System.Assertions;

This package has been in use by many of our customers since 1993, and I see
no benefit to them in making arbitrary small changes to this spec.

****************************************************************

From: Tucker Taft
Sent: Wednesday, February 6, 2002,  3:20 PM

I mentioned this issue in the AI, and suggested that with renaming of
exceptions and subprograms, backward compatibility could be achieved.  Is there
a reason why the renaming wouldn't work adequately?

****************************************************************

From: Robert Dewar
Sent: Wednesday, February 6, 2002,  4:03 PM

Yes that might work fine

****************************************************************

From: Alan Burns
Sent: Tuesday, January 7, 2003,  5:01 AM

he HRG was asked (by ARG) to look at these AIs on
assert and pre/post conditions etc.

Please find attached our considerations (which
was on the whole are not supportive). To prevent these
thoughts getting lost, perhaps they should be
incorporated into the AIs

----

Comment from the HRG on AI286 - pragma Assert.

The proposal contains a number of problems that clearly suggest that the
AI does not in fact significantly aid the construction and verification
of high-integrity software. At best, the proposed mechanism
would provide a convenient debugging aid for use during program
development.

There are 4 particular difficulties, 3 of which are significant to
the behaviour of Ada programs and the last which is more conceptual and
stylistic:

1.  Serious limitations to what can be expressed in the predicate
associated with the pragma (i.e. what can be "asserted").

2.  The likelihood of program semantics being affected by the presence
of assert pragmas and by the assertion policy in force.

3.  The use of the exception mechanism to indicate assertion failure.

4.  The use of the word "assert", which has strong connotations of proof
for what is actually a "run time check".


Limits on what can be Expressed
-------------------------------

The proposed pragma allows for a standard Boolean expression or
predicate. This limits assertions to what can expressed in the standard
expression language of Ada. Furthermore, it means that assertions can
only be made about program entities that are visible at the point where
the assertion is to be planted. Unfortunately, many (perhaps most) of
the interesting properties that it is worth asserting cannot be
expressed in simple Ada expressions and/or involve program properties
not visible according to the rules of Ada.

Specific limitations in the expressions include:

1.  a way of distinguishing current from initial variable values;
2.  a notation for handling updates of structured variables;
3.  the absence of implication operators; and
4.  the absence of quantifiers.

Examples:

1.  We call an "Exchange" procedure and wish to assert that the parameter
values have been exchanged:

procedure Swap (X, Y : in out Integer); -- exchanges X and Y
...
Swap (P, Q);
pragma Assert (P = 'old value of Q', "Swap failure");


2.  We update the 3rd element of an array and wish to assert that the array
is unchanged except for the new value:

A (3) := X;
pragma Assert (A = 'the old A with the 3rd element overridden by X', ...


3.  We obtain the maximum of X or Y:
Z := Max (X, Y);
pragma Assert ('X > Y -> Z = X and X <= Y -> Z = Y', ...

(admittedly this could be restructured to avoid the use of implication
but many common forms of predicate are substantially clearer when
expressed in the form shown).


4.  We wish to assert that an array contains at least on element greater
than 10.

pragma Assert ('there exists in A some index value I such
                that (A(I) > 10, ...


5.  We wish to assert that a stack is not full before calling a push
operation; however, the stack package does not export an "IsFull"
function and we don't want make the internals of the stack visible at
the point of call.


Effect of assertions on program semantics
-----------------------------------------

The expression language used in the assertions allows the use of
calls to functions which have side effects.  This clearly allows the
semantics of a program to be affected by the assertion policy in force.
The AI admits this and even provides an option to evaluate the predicate
("for its side-effects") whilst ignoring the result.  The paragraph
stating that "...expression in an Assert pragma should normally not call
functions that have side-effects...." is far too weak for a proposal
that purports to raise the integrity of Ada programs.


Use of exceptions
-----------------

The raising of Assertion_Error as a mechanism for signalling assertion
failures is highly problematic.

1. The exception may be inadvertently caught by an existing "when
others" clause which would negate the purpose of the assertion
mechanism.

2.  The HRG report is cautious about the use of exceptions in high-
integrity systems and the deliberate introduction of a new exception
runs counter to the advice given in TR 15942.

3.  Many high-integrity systems are built on reduced run-time systems
that provide limited or no support for exception handling.  Therefore,
assertion checks would most likely have to be removed from production
code; this reinforces the view that the proposal is more a debugging aid
than a serious production tool.

Use of term "Assert"
--------------------

The term "assertion" has great significance to the program verification
community.  For most practitioners it implies the use of some form of
proof process; however, the AI is proposing a run-time executable check
which is semantically no different from "if C then raise X; end if".
There is a serious risk of muddying the distinction between static proof
work and testing/debugging.  The HRG report itself takes great care to
separate these different forms of verification.

For these reasons, if the AI is accepted it is the HRG's view that this
be on the basis that the pragma is renamed "Run_Time_Assert" or better
"Run_Time_Check".


Conclusions
-----------

The weaknesses identified above reduce the AI to a simple debugging aid
that offers no significant gain over what can currently be achieved
using standard Ada language constructs.  If the only purpose of the AI
is to support high integrity systems (ie. if the pragma would be
defined in Annex H) then the HRG does not support its acceptance.

****************************************************************

From: Dale Stanbrough
Sent: Friday, May 23, 2003,  8:40 AM

Hello,

I hope i have the format for the following AI proposal correct.
If you have any questions, please feel free to contact me.

The format (and some of the wording) has been taken from AI-286.

Dale Stanbrough
Director Adasoft (Australia).

---------------------------------------------------------------------
!summary

Two pragmas similar to "assert" are proposed which have
slightly different semantics.

!problem

The exact semantics of pragma Assert are hard to define.
It may result in a run time check, but compilers could also assume
that the condition is true, and take advantage of it to make
optimisations (and potentially remove other checks or code).
This AI proposes that two pragmas, pragma Verify and pragma Assume,
be created to separate the two possible uses of pragma Assert.


!proposal

The form of the pragma Verify is as follows:

     pragma Verify(boolean_expression[, [Message =>] string_expression]);

   A pragma Verify is allowed at the place where a basic_declaration or
   a statement is allowed.


The form of the pragma Assume is as follows:

     pragma Assume(boolean_expression);

   A pragma Assume is allowed at the place where a basic_declaration or
   a statement is allowed.


As per AI-286 the package Ada.Assertions is as follows:

     package Ada.Assertions is
         pragma Pure(Ada.Assertions);

         Assertion_Error : exception;
           -- This exception is raised by an assertion check that fails
     end Ada.Assertions;



Pragma Assume specifies a boolean expression which the developer has
proven
to be true by analysis of the code. The purpose of the pragma is to
provide
extra information to the compiler to allow it to make optimisations
in the generated code, as well as helping to document the code.
There would be no evaluation of the boolean expression at run time,
and therefore no possible raising of an exception.

Pragma Verify would specify a boolean condition that is to be converted
into a run time check that would raise Assertion_Error when it evaluates
to false. It provides identical functionality to the pragma Assert
provided
by several compilers, but it would not be used to provide any
optimisations
of the code, and could therefore always be relied on to be checked at
run
time.


Implementation Permission

Assertion_Error may be declared by renaming an implementation-defined
exception from another package.

!wording


!discussion


!example


!ACATS test


!appendix

From: John Barnes
Sent: Tuesday, June 10, 2003  2:11 AM

There is some disquiet in the UK concerning the possible
interaction between the assert pragma proposed by AI-286 and
the assert statement in Spark.

After discussion among members of the UK BSI Ada panel, I
have been asked to submit the following comment/suggestion.

===

The current AI286 suggests a new pragma "Assert" and a
procedure
Ada.Assertions.Assert for run-time assertion checking.
However, there will be occasions where SPARK users will want
to use both SPARK "static asserts" and
pragma/procedure-based dynamic asserts in the same program.

Unfortunately, this won't work given then current AI, since "assert"
is a reserved word in SPARK.  Any attempt to use this pragma simply
generates a syntax error from the Exainer, which is most unfortunate.
It is also impossible to write a legal SPARK shadow of the proposed
Ada.Assertions package as is currently written.

We suggest renaming the pragma and procedure to
"Dynamic_Assert" or "Runtime_Assert" to avoid name-space
conflict.  These names also help to distinguish between
dynamic asserts, and static asserts - an orignal
concern of the HRG.

===


I believe that the HRG hopes to look at this again before
the ARG meeting in Toulouse.

The feeling about this AI is strong and I think I should add
that unless it is amended to overcome this concern then it
is probable that the UK will vote against it.

****************************************************************

From: Robert Dewar
Sent: Tuesday, June 10, 2003  2:27 AM

I object to this renaming.

First, there is nothing to stop a pragma from having the same name
as a keyword if you are in the language extension business.

Second I don't think we should choose a less convenient name (and for
many many users of Ada 95 the name they have used extensively
for ten years) just because some non-Ada compiler has an incompatible
extension.

My recommendation is fix the examiner so that it allows both the
current use of the assert keyword, and also allows pragma assert.
This is convenient in any case for using the examiner with existing
compilers that recognize pragma Assert.

****************************************************************

From: Alan Burns
Sent: Tuesday, June 10, 2003  2:55 AM

The HRG's concern with the use of `assert' was not
a concern about name clash with SPARK examiner but
with the widely held view in the verification world
that `assert' implies a static provable property
of a program not a wish that at run-time this
property is true.

Hence the HRG's view is that another name be used for
the dynamic case.

Please see HRG's earlier review of this AI

****************************************************************

From: Pascal Leroy
Sent: Tuesday, June 10, 2003  4:02 AM

> I object to this renaming.

I strongly agree with Robert here.

1 - Two major implementations have been supporting this pragma for
years, and in fact the ARG careful designed AI 286 is such a way that
incompatibilities would be minimized.  Although we don't know for sure,
chances are that there is a substantial amount of code out there that
depends on these pragmas.  Changing the name would defeat the purpose of
the AI, which was to increase portability by making it possible to port
code that includes assertions from one compiler to another.  Not to
mention that we would now have two assertion pragmas around, with just
more confusion for the user.

2 - Anyone designing extensions to syntax of the language is in a state
of sin, and should not be surprised that some of these extensions would
conflict with future evolutions of the language, especially if they use
perfectly good words like "assert".  If I were designing an extension, I
would choose a syntax that cannot possibly conflict with the rules of
Ada, e.g. "_assert" (sounds like C, doesn't it).

3 - I understand the HRG concern, but it carries little weight in my
opinion.  The fact that a name conveys a meaning that may not be exactly
right for some subcommunity of Ada users is no justification for
introducing the compatibility mess described in #1.  I would be happy to
study proposals regarding pragmas for static checks (although that seems
like a can of worms IMHO) but this is no justification for renaming
Assert.

****************************************************************

From: Tucker Taft
Sent: Tuesday, June 10, 2003  8:58 AM

Let me add my voice to the other implementors.
This pragma has been supported for years by
several vendors (Aonix, Green Hills, ACT,
Intermetrics/AverStar/AverCom/SofCheck (do we count
as 4? ;-), and probably others).

It is silly to change the name at this point.
Programmers certainly understand what it means,
and "assert" is used in C, C++, Java, etc.

Fixing the SPARK examiner to allow Assert
in a pragma could not be more than an afternoon's
work, given their impressive track record.
The same "trick" that is used for attributes
could be used here, namely if ASSERT is a reserved
word, then change the pragma grammar rule to be:

    pragma ::= PRAGMA identifier [pragma_args];
             | PRAGMA ASSERT pragma_args;"

I really hope the UK delegation can understand
the sense in standardizing this wide-spread existing
practice, rather than inventing some new name.
Certainly in the kind of code we develop in Ada,
pragma Assert appears thousands of times.

****************************************************************


Questions? Ask the ACAA Technical Agent