From bobduff  Wed Dec 16 16:07:40 1992
From: bobduff (Bob Duff)
To: ada9x-mrt
To: iso@ajpo.sei.cmu.edu
Subject: LSN-1062 on Assert

Here is another copy of LSN-1062 on Assert with the correct number.
(The previous version was incorrectly labeled 1058.)
Sorry for the confusion.

- Bob

!topic LSN on Assert
!key LSN-1062 on Assert
!reference MS-K;4.9
!from Brian Wichmann $Date: 92/12/16 16:06:06 $ $Revision: 1.5 $
!discussion

This Language Study Note discusses pragma ASSERT.  It is in response to
resolution number 10-3 of the Salem ISO/WG9 meeting.  It is written in
LaTeX format.  Remove the ",a4wide" if you are printing on 8.5x11 inch
paper.

-------------------------------- cut here --------------------------------
\documentstyle[times,a4wide]{article}
% times and a4wide can be deleted from the above if your system does not
% support these sytles.

\title{LSN on the pragma Assert}
\author{B A Wichmann,\\
 National Physical Laboratory,\\
 Teddington, Middlesex, TW11 OLW, UK \\
 E-mail: baw@seg.npl.co.uk}

\begin{document}

\maketitle
\section{Introduction}

This LSN has been produced at the request of WG9, following the meeting
in Salem in November 1992. See the summary for a direct response to the
WG9 resolution.


\section{Issues}

The main issues with the proposal are as follows:

\begin{description}

\item[Exception:]

Robert Dewar has suggested that the pragma, if the check fails, should raise
an unhandleable exception and hence that the program would halt if the
assertion failed. This corresponds to the notion that the pragma is
concerned with a property of the program, rather than a dynamic effect.
However, this idea seems too irregular.

The proposal in the 11th September version of the Annex raised
{\tt Constraint\_Error}. This corresponds to the notion of breaking a constraint,
which in this case, is specified in a general form by the user.

Another possibility would be to define a specific exception {\tt Assert\_Error}.
However, since handling the exception is not the main intent, this seems
like over-kill. Indeed, it might encourage handling the exception rather
than ensuring that the conditions checked in the exceptions are true.
We want to encourage a programming style that doesn't depend on handled
assertions.

A suggestion made during the review of the 11th September version, was that
{\tt Program\_Error} seemed a more appropriate exception than {\tt Constraint\_Error}.
I agree with this view, since it seems more in the spirit of Ada.

\item[Proof tools:]

One reason for proposing the Assert pragma is that the condition can be
used as input to a proof tool. Rudolf Landwehr points out that proof tools
require much more extensive input than that which can be expressed by the
Assert pragma. This is certainly true, indeed, the formulation of a complete
assertion language was ruled out-of-scope initially. However, for many
software components, the specification is not in doubt, but formal
verification is useful. Hence for something like a sort routine, the pragma
could be used to specify loop invariants, allowing little additional input
for verification.

My own view is that the facility will be widely implemented, even though
many vendors will not support the Annex, and that users will also write
assertions regularly instead of comments. This could aid the re-use of
code in cases in which formal verification is required.

\item[Activation:]

Conventional practice in small safety-critical systems is to show the code
is exception free and even compile it with exception detection suppressed.
Hence the use of the Assert pragma could be expected to follow the same
practice. During early development, the Assert checks could be performed,
although one strategy would be to use them entirely for input to a tool.

The ability to switch the checks on or off without source text modification
is useful, and hence the use of something like {\tt pragma Suppress(Assert\_Error)}
is not appropriate (unless it were a configuration pragma, in which case,
the effect is similar to a compiler option.) Also, the pragma Suppress
does not remove any side-effect of the expression in the pragma -- in
time-critical systems, it is essential such code is not executed.

For those systems in which it is essential the checks are not performed in
the final system, the use of a configuration pragma is appropriate. However,
it does not seem necessary to define such a pragma, as a compiler option is
equally convenient.

Note that a user-written assertion procedure cannot be switched on and off
except globally.

The proposal here is to specify that both checking and no checking be
provided, and leave the mechanism to the vendor. This allows the system
to support various development strategies.


\item[Optimization:]

Although optimization is a difficult issue in general, it this case, the
position is very straightforward. The pragma if either equivalent to an if
statement, or a null statement, with obvious effects. When the assertion is
not being checked, the code produced by the compiler should be the same as
that without the pragma (this can easily be checked).

% Most correct optimization is not observable other than an increase in
% speed or a reduction in space. Clearly, this is benign. However, the
% widely held view is that for critical software, an optimizer should be
% switched off, to reduce the risks of compiler errors. However, one vendor
% claims that his compiler is more reliable with the optimization turned on,
% since that is the usual way it is used.


It is possible to envisage some horrible incorrect optimizations, which is
really a problem quite separate from the pragma. For
instance, take the following:

\begin{verbatim}
    I, J: Integer range 1..10;
    A: array(Integer range 1..10) of Float;
    begin
    if F then
       J := 1;
    else
       I := 2;
       J := 2;
    end if;
    pragma Assert(I=J);
    A(I) := 1.0;
\end{verbatim}

A compiler could assume that {\tt I} must have a value in the last
statement, since it is referenced in the Assert expression, and therefore
omit the index check on the assignment to {\tt A(I)}. Implications of this
nature are avoided, since the semantics states that there are really two
programs, one in which the Assert is an if statement, the other a null
statement. In both cases, the above program is erroneous in Ada 83, but will
be a bounded error in Ada 9X.

A related issue is what information a proof tool will deduce from an
assertion. This is obviously beyond the scope of the Ada 9X standard,
and will depend upon the tool. Consider replacing the pragma above by:
\begin{verbatim}
   pragma Assert( I in 1..10);
\end{verbatim}
Surely this is stating that {\tt I} has been assigned a value, which a proof
tool (of no great strength) would show is false. An alternative view is that
a proof tool would regard the assertion as true (from the declaration) which
reflects a different strategy.

The conclusion from this is that it is important to state that the mode
in which the check is not performed must be equivalent to the absence
of the pragma. This is clear from the proposed wording.
    
\item[Side-effects:]

One reason why in the original design of Ada that assertions were dropped
was because the facility for defining functions without side-effects was
withdrawn. The fact that the condition in the pragma can have a side-effect
is undesirable, but cannot be ruled out. The view taken here is that it is
the user's responsibility to avoid any unintentional effects of the
evaluation of the pragma.

In fact, in some safety-critical code, even the evaluation of a pragma
which always succeeds and has no side-effect is problematic, due to the
time taken.

A consequence of this decision is that a program unit containing assertions
must be regarded as having two distinct semantics -- either with or without
the pragma evaluation. I would assume that proof tools would object to
discovering a side-effect.

\item[User-written procedure:]

It is important to note that the proposed pragma is quite different from
the effect the user could obtain by writing a similar procedure. The
procedure has the following properties:
\begin{itemize}
\item The source code must be changed to avoid the checking;
\item It is difficult to avoid the evaluation of the Boolean expression;
\item It is difficult to selectively change the checking;
\item The expressions cannot be easily identified by verification tools.
\end{itemize}

\item[Context:]

The pragma is not allowed in both the declarative context.
Some confusion could arise from the declarative context
since a range constraint in a declaration restricts a variable for the
entire scope of the declaration, while an Assert pragma would only apply
to the value at the point of the assert.

Also, an assert pragma could only refer to the initial values of declared
entities, which should be self-evident from the initialisation code.

>From many points of view, it is best to think of a sequence of declarations
as an atomic action, in which case, it is natural to place an Assert pragma
at the start of the statement sequence.

Given a package without a statement part, then it may be necessary to
introduce a statement part to place an Assert pragma.

I conclude that restricting the pragma to a statement context seems best.
In Ada 200X, it might be possible to introduce the Assert into declarative
contexts to indicate predicates which remain true throughout the program
execution. (The Gypsy system had such a facility which was not easy to
define.)

\end{description}

\section{Revised proposal}

To allow users to document properties of values which can be expressed
via a boolean expression, the pragma {\tt Assert} is provided. This
pragma has the form:

\begin{quote}
{\sf pragma} {\tt Assert} ( {\em boolean\_}expression );
\end{quote}

This pragma is only allowed where a null statement would be allowed.
Two modes of operation are provided. In one mode, the pragma is equivalent
to the null statement. In the other mode, the pragma is equivalent to:

\begin{verbatim}
     if not boolean_expression then
        raise Program_Error;
     end if;
\end{verbatim}

Note: The mode of operation could change the semantics of the program by
raising an exception, or by a side-effect in the evaluation of the
boolean expression.


\section{Summary}

I think this note answers all the issues that arises from the pragma.
Please note that it is not a key component of the Annex, but merely
something that on reflection, I think is advantageous. The only
change from the 11 September version is that {\tt Constraint\_Error}
has been replaced by {\tt Program\_Error}.

The WG9 resolution and a summary of the response is as follows:

\begin{quote} 
Pragma ASSERT should be the subject of a study covering at least
the following questions:
\begin{itemize} 
\item which exception should be raised {\em The exception should be
{\tt Program\_Error} since this seems closest to the spirit of Ada.}
 
\item should program halt {\em No, since this would make the feature
very irregular.}
 
\item can it be optimized away {\em No. Either the assertion is executed,
or it is not. If not, the pragma is equivalent to the null statement and
has not effect whatsoever.}
 
\item can it be used for other optimization {\em It can only effect
optimization if the pragma is evaluated. In which case, it acts like
any other executable statement. }
 
\item can same effect be programmed {\em No. The syntax is special which
allows proof tools to identify the pragma.}

\end{itemize}
\end{quote}
\end{document}

Revised to reflect comments by Bob Duff and John McHugh (27th Nov 92).
(Robert Dewar did not comment.)
------ Output from automsg.perl ------
Mail received from bobduff
*** Key LSN-1062 given to topic 'LSN on Assert'
----------- End of output ------------