Re: Assertions

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

Robert Dewar wrote in message <7i7ei9$93v$1@nnrp1.deja.com>...
|In article <ur9o9f95c.fsf@infomatch.com>,
|  Ray Blaak <blaak@infomatch.com> wrote:
|>
|> I would suggest the name "Verify" for assertions intended to
|> be runtime checks, and "Assume" for assertions intended to
|> give info to the compiler.
|
|In any case, this thread should have adequately demonstrated
|that
|
|(a) this is quite a tricky subject
|(b) it is not easy to propose a solution that gets any kind of
|    consensus agreement.
|
|This has always been the case when this issue has been
|discussed, so it is hardly surprising to see it happening again
|:-)


Robert is absolutely right on both points, of course.  However, I don't
actually recall anybody actually suggesting anything to the contrary.  I,
for one, never expected otherwise.

Of course it's a tricky subject!  Of course consensus is not going to be
handed to us on a plate!  However, I would suggest that we can,
nevertheless, attempt to negotiate this tricky subject, and to persue a
sufficient consensus.  If people hadn't taken this attitude towards almost
all aspects of the development of the Ada standard, there would never have
been an Ada language at all.

At this point, I think I can suggest five possible pragmas as candidates for
a future revision of the Ada standard (and perhaps for prior de facto
adoption):

============================================================

   pragma Assume (Condition);
   pragma Verify (Condition);

The Assume and Verify pragmas are allowed anywhere a declaration or a
statement is allowed.  When the pragma would be elaborated, if it were a
declaration, or executed, if it were a statement, the pragma is said to be
executed.

For execution of the  Assume pragma, the compiler is allowed, but not
required, to test the Condition, but in either case is allowed to assume
that the Condition is true for the purposes of optimisation.

For execution of the  Verify pragma, the compiler is required, unless
suppression of Verify_Check applies, to test the Condition is true. If the
suppression of Verify_Check applies, the compiler is allowed, but not
required, to omit this test.  In any case, the compiler is allowed to assume
that the Condition is true for the purposes of optimisation.

   pragma Verify_Before_Call (Subprogram,Condition);
   pragma Verify_Before_Return (Subprogram,Condition);

These two pragmas are allowed anywhere a declaration is allowed in the
public part of a package specification.  The Subprogram must be the name of
a subprogram declared before the pragma in the same specification.  The
condition may contain the names of any of the parameters of the subprogram,
as well as any entity that would normally be visible at the point of the
pragma (but not any entity in the body of the subprogram).  The
Verify_Before_Call pragma causes the execution, with the same Condition, of
an implicit Verify pragma just before the first declaration, or, if the
subprogram has no declarations, as the only declaration, of the subprogram.
The Verify_Before_Return pragma causes the execution, with the same
Condition, of an implicit Verify pragma just after the evaluation of the
return expression of a return statement in the subprogram, or just before
the execution of a return statement in the subprogram which has no return
expression.  For both these pragmas, the meanings of the names in the
Condition shall be interpreted at the place of the pragmas (not at the
places of their implicit execution).

For all four of these pragmas, if the test of the Condition is actually
done, and it fails (evaluates to False), the predefined exception
Program_Error is raised.  (If this exception is raised by a pragma which
takes the place of a declaration, the exception is immediately propagated
out the innermost enclosing block, and is never handled by an exception
handler inside this block.)

[There is a new check for the Suppress pragma, Verify_Check.]

   pragma Parallel_Loop [(Loop_Name)];

This pragma is allowed anywhere a statement is allowed, but must apply to
loop.  With no parameter, this pragma applies to the innermost enclosing
loop statement; otherwise this pragma applies to loop whose name is
Loop_Name.  The loop must have an iteration scheme of the 'for' variety, and
this iteration scheme must not include the reserved word 'reverse'.

The pragma Parallel_Loop allows the compiler to assume, for the purposes of
optimisation, that the loop it applies to has the following property:
execution of the iterations of the loop may be arbitrarily overlapping, and
in any order, without changing the effect of the loop.  The compiler is
allowed, but not required, to test that the loop actually has this property;
if such a test is done, and fails, the predefined exception Program_Error is
raised.

============================================================

It may well be better to use 'Assert' throughout rather than 'Verify'.
Comments please.

Does this count as a stoneman? :-)  I hope no-one objects to my throwing in
the last pragma, but it seemed reasonably appropriate.  Sorry, I must go
now, my mum is expecting her cup of tea ;-)

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