Version 1.3 of ai05s/ai05-0145-1.txt

Unformatted version of ai05s/ai05-0145-1.txt version 1.3
Other versions for file ai05s/ai05-0145-1.txt

!standard 11.5 (00)          09-02-16 AI05-0145-1/02
!standard 11.4.1 (10)
!class amendment 09-02-15
!status work item 09-02-15
!status received 09-02-15
!priority Medium
!difficulty Medium
!subject Pre- and Postconditions
!summary
To augment the basic "assert" pragma capability in Ada 2005, we propose pragmas for specifying pre and post conditions for subprograms.
The semantics for these pragmas are defined in terms of the Assertion_Error exception used by the Assert pragma and the Assertion_Policy configuration pragma.
!problem
A number of programming paradigms include the heavy use of pre/post conditions on subprograms. Having a basic standardized "Assert" pragma supports this approach to some degree, but generally requires that the Assert pragmas actually be inserted inside the bodies of the associated code. It would be much more appropriate if these pre/post conditions appeared on the specification of the subprograms rather than buried in the body, as it really represents part of the contract. In particular, one wants any implementation of a given package spec to conform to all of the pre/post conditions specified, in the same way one wants any implementation of a package to conform to the constraints of the parameter and result subtypes of the visible subprograms of the package.
Effectively, pre/post conditions may be considered as generalized, user-definable constraints. They have the same power to define more accurately the "contract" between the user and implementor of a package, and to thereby catch errors in usage or implementation earlier in the development cycle. They also can provide valuable documentation of the intended semantics of an abstraction.
!proposal
The pragmas Precondition, Inherited_Precondition, Postcondition, and Inherited_Postcondition have the following form:
pragma Precondition(subprogram_local_name,
[Check =>] boolean_expression [, [Message =>] string_expression]);
pragma Inherited_Precondition(dispatching_subprogram_local_name,
[Check =>] boolean_expression [, [Message =>] string_expression]);
pragma Postcondition(subprogram_local_name,
[Check =>] boolean_expression [, [Message =>] string_expression]);
pragma Inherited_Postcondition(dispatching_subprogram_local_name,
[Check =>] boolean_expression [, [Message =>] string_expression]);
The (dispatching_)subprogram_name must name the immediately preceding subprogram. For Inherited_Precondition and Inherited_Postcondition, the subprogram must be a dispatching subprogram. The boolean expression is defined within the context of the subprogram specification so that the formal parameter names are directly visible.
The names in the boolean_expression of a precondition or postcondition pragma are resolved not at the point of the pragma, but rather at the freezing point of the named subprogram, or at the end of the immediately enclosing visible part, whichever comes first.
For a postcondition on a function, the attribute "Result" is defined on the subprogram name, yielding the value returned by the function. For a postcondition on a procedure, the attribute "Old" is defined on each of the IN OUT nonlimited formal parameters, yielding the value of the formal parameter at the beginning of the execution of the procedure.
If an Inherited_Precondition or Inherited_Postcondition pragma is specified for a primitive subprogram, then it also applies to all overridings of the primitive. By contrast, Precondition/Postcondition pragmas may be applied to non-primitive subprograms, and are not inherited.
For an Inherited_Precondition or Inherited_Postcondition, if a formal parameter name corresponding to a controlling operand of the subprogram appears in the boolean expression, it is view converted to the associated class-wide type, implying that dispatching is performed if calls on primitive functions occur in the expression. All other formal parameter names appearing within the boolean expression of a precondition or postcondition pragma have the type specified in the subprogram's parameter profile.
If the assertion policy in effect at the point of a precondition pragma is "Check," then upon a call on the specified subprogram, after evaluating the actual parameters and making the parameter associations, the check associated with the precondition pragma is performed. This consists of the evaluation of the boolean expression, and if False, a raise of the Ada.Assertions.Assertion_Error exception, with the specified Message if provided. It is not specified whether any check for elaboration of the subprogram body is performed before or after the precondition check.
If multiple precondition pragmas apply to the same subprogram (through inheritance of Inherited_Preconditions), then only if all of the boolean expressions evaluate to False, is Assertion_Error raised; an implementation-defined message is associated with the exception occurrence in this case. If any one of them evaluates to True, the subprogram call proceeds normally. The order in which multiple precondition pragmas are checked is not specified, and if one of them evaluates to True, it is not specified whether the others are checked.
If the assertion policy in effect at the point of a postcondition pragma is "Check," then upon successful return from a call on the specified subprogram (as opposed to a return due to the propagation of an exception), and prior to copying back any by-copy [IN] OUT parameters, the check associated with the postcondition pragma is performed. This consists of evaluating the boolean expression, and if false, raising Ada.Assertions.Assertion_Error, with the specified Message, if any. It is not specified whether the exception, if any, is raised at the point of the return statement or after leaving the subprogram. (I.e. it is not specified whether the exception can be handled within the subprogram.)
If multiple postcondition checks apply to the same subprogram, then Assertion_Error is raised if any of them evaluates to False; the message provided corresponds to one of the failing checks. The order of performing the checks is not specified, and if one of them evaluates to False, it is not specified whether the others are checked. If more than one evaluates to False, it is not specified which message is provided with the exception occurrence. It is not specified whether any constraint checks associated with copying back [IN] OUT parameters are performed before or after the postcondition checks.
For a dispatching call or a call via an access-to-subprogram, the precondition/postconditions that apply to the call are determined by the subprogram actually invoked. Note that for a dispatching call, if there is an Inherited_Precondition that applies to the subprogram named in the call, then the rules for checking preconditions ensure that so long as this Inherited_Precondition is satisfied, the overall precondition check will succeed (because if any precondition evaluates to True, the call proceeds normally).
Assertion Policy
If the assertion policy at the point of a precondition or postcondition pragma is "Check" then the semantics are as described above. If the assertion If the assertion policy at the point of the pragma is "Ignore" then the pragma has no effect.
!wording
!discussion
This is based on AI95-0288.
The precondition and postcondition pragmas provide a basic capability for defining the "contract" of a subprogram. Implementation of the corresponding checks is tied to the assertion policy in effect at the point of the pragma (rather than at the call or the body), to ensure that the checks may be inserted either at the point of the call or inside the subprogram body, and both the caller and the callee "know" whether the check will be performed (which might affect optimization).
We provide a separate "Inherited_" version of the pragmas to distinguish between conditions that apply to a particular version of a dispatching operation from those that apply to all overridings of the operation. This distinction is missing in Eiffel, and represents a weakness (in our view) of their model. The "Inherited_" version necessarily must be less specific to the particular body (Inherited_Precondition must be more restrictive, and Inherited_Postcondition must be more lax), and hence cannot catch as many bugs by itself as the combination of an inherited condition and a condition specific to a particular body.
We defer resolving the names in the boolean_expression because it is natural for preconditions or postconditions to refer to other subprograms declared in the same scope, and requiring that there be no forward references unduly restricts the expressions.
A possible implementation model for the pre/postcondition checks is as follows. Existing calls on Proc or Func are replaced with calls on "Proc_with_check" or "Func_with_check" if the assertion policy is "Check" at the point of the pragmas. The "_with_check" subprograms are defined as follows:
procedure Proc_with_check( ...; Nonlimited_Inout_Param1 : in out Inout_Type1; ...) is -- Procedure with pre/post conditions inserted
begin -- Check precondition(s) if not <precondition_bool_expr1> and then not <precondition_bool_expr2> and then not ... then raise Ada.Assertions.Assertion_Error [with <message>]; end if;
declare -- save Old values of nonlimited in/out params -- referenced in postconditions Nonlimited_Inout_Param1'Old : constant Inout_Type1 := Nonlimited_Inout_Param1; ... -- other nonlimited in/out params referenced in postconditions begin
-- Call the "real" procedure Proc(..., Nonlimited_Inout_Param1, ...);
-- check postcondition(s) if not <postcondition_bool_expr> then raise Ada.Assertions.Assertion_Error [with <message>]; end if; ... -- any other postconditions end; end Proc_with_check;
function Func_with_check(...) return Result_Type is -- Function with pre/post conditions inserted begin -- Check precondition(s) if not <precondition_bool_expr1> and then not <precondition_bool_expr2> and then not ... then raise Ada.Assertions.Assertion_Error; -- or Ada.Exceptions.Raise_Exception(..., <message>) end if;
declare -- Save result of calling the function (use "renames" -- so this works with limited-type return as well) Func'Result: Result_Type renames Func(...); begin -- Check postcondition(s) if not <postcondition_bool_expr> then raise Ada.Assertions.Assertion_Error; -- or Ada.Exceptions.Raise_Exception(..., <message>) end if; ... -- any other postconditions
-- Now return to the caller return Func'Result;
end;
end Func_with_check;
Note we don't specify exactly where the precondition checks occur relative to elaboration checks so these checks may be done "outside" or "inside" the subprogram as is most convenient. Similarly, we don't specify whether the postcondition checks are performed at the point of the return statement, or at the end of the call, to provide implementation flexibility. This means that in some implementations Assertion_Error could be caught inside the subprogram. This does not seem to be a serious concern, and the implementation flexibility seems valuable.
However, we do require that dynamically bound calls, i.e. calls via an access-to-subprogram dereference or a dispatching call, have the applicable pre/postconditions checked. This implies that in most situations, the pre/postcondition checks will need to be implemented by adding code "inside" the subprogram, or by having two separate subprograms (as above), one which is used by dynamically bound calls which includes the check, and one which is used when the checks are performed by the caller.
To do the best job of optimizing precondition checks, one would generally want to expand them at the point of the call. On the other hand, postcondition checks are probably most optimizable when done inside the subprogram. This would imply that under heavy optimization, it might be useful to have a separate version for dynamically bound calls that performs the precondition checks "inside," while statically bound calls would perform the check at the point of call, and then call the version that bypasses the precondition check if the checks succeed. This is similar to an approach that some compilers use for access-before-elaboration checking. Having postcondition checks inside seems preferable in any case.
We don't provide a pre/postcondition pragma for access-to-subprogram types. That might be useful in some cases. However, the pre/postcondition would (presumably) only apply on calls through a value of the type, which means additional implementation complexities, in that the checking code could not be inserted inside the designated subprograms, and would have to be at the call point, or in some kind of "indirection" stub. I suppose one approach would be to interpret a pre/postcondition pragma on an access-to-subprogram type as a requirement for statically matching (or provably "stronger"?) pre/postconditions on all subprograms to be designated by values of the type. That begins to get into theorem proving, etc., which might be appropriate for a separate tool, but is beyond what we want the "average" Ada compiler to have to do. ;-)
Assertion Policy
We have used the Assertion_Policy pragma of Ada 2005, with the same options and interpretation. It might make sense to define separate pragmas, such as Precondition_Policy, and Postcondition_Policy but with the same set of identifiers. This would give the programmer more control. On the other hand, typically either the programmer wants full debugging, or full speed. Intermediate points seem relatively rare.
Inherited vs. Inheritable vs. Classwide vs. ...
We considered other names for Inherited_Precondition and Inherited_Postcondition. The Ada 95 AI used "Classwide_Precondition." We also considered "Inheritable_Precondition", though that sounded a bit like a disease. In the end we went with what seemed the simplest name that conveyed the intent.
!example
generic type Item is private; package Stacks is type Stack is private;
function Is_Empty(S : in Stack) return Boolean; function Is_Full(S : in Stack) return Boolean;
procedure Push(S : in out Stack; I : in Item); pragma Precondition(Push, not Is_Full(S)); pragma Postcondition(Push, not Is_Empty(S));
procedure Pop(S : in out Stack; I : out Item); pragma Precondition(Pop, not Is_Empty(S)); pragma Postcondition(Pop, not Is_Full(S));
function Top(S : in Stack) return Item; pragma Precondition(Top, not Is_Empty(S));
function Is_Valid_Stack(S : in Stack) return Boolean;
Stack_Error : exception; private -- whatever end Stacks;
!ACATS test
!appendix

From: Tucker Taft
Sent: Sunday, February 15, 2009  3:56 PM

This is a resurrection of AI95-00288, on pre- and postconditions.
It is virtually unchanged. The proposed pragma names are:

    pragma Precondition
    pragma Inherited_Precondition
    pragma Postcondition
    pragma Inherited_Postcondition

These were discussed at some length at a meeting at AdaCore which
took place on 12/2/2008, with Tucker Taft of SofCheck as guest.

[This is version /01 of the AI - ED].

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

From: Tucker Taft
Sent: Sunday, February 15, 2009  4:27 PM

I left out one important issue:

   The names in the boolean_expression of a precondition
   or postcondition pragma are resolved not at the point
   of the pragma, but rather at the freezing point of the
   named subprogram, or at the end of the immediately
   enclosing visible part, whichever comes first.

and from the discussion:

   We defer resolving the names in the boolean_expression
   because it is natural for preconditions or postconditions
   to refer to other subprograms declared in the same
   scope, and requiring that there be no forward references
   unduly restricts the expressions.

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

From: Robert Dewar
Sent: Sunday, February 15, 2009  5:01 PM

I haven't studied the whole proposal carefully, but as far as I can
tell, the Precondition/Postcondition part of it corresponds pretty much
exactly to what has been implemented in GNAT, and used fairly extensively.

>> A resurrection of AI95-00375 on type invariants will appear shortly.

I look forward to that, we have always got stuck on invariants :-)

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

From: Tucker Taft
Sent: Sunday, February 22, 2009  4:51 AM

I'll admit I have been bitten by the syntax bug (thanks, Randy!) for
pre- and postconditions, and with invariants coming up I suspect it will
continue.  Here is a general proposal that avoids introducing new reserved words,
but is quite flexible:

  To specify aspects of an entity (at least "operational" ones)
  and link them directly to the associated declaration,
  consider a general syntax of:

   <declaration>
     WITH
       <aspect_name> [=> <aspect_value>],
       <aspect_name> [=> <aspect_value>],
       ... ;

E.g.:

     function Pop(S : in out Stack) return Elem
       with
         Pre => not Is_Empty(S),
         Post => not Is_Full(S);

     type Even is new Integer
       with
         Invariant => Even mod 2 = 0;

     type Atomic_Array is
       array(Positive range <>) of Natural
         with
           Atomic_Components;

     type Set is interface
       with
         Invariant'Class =>
           (Is_Empty(X)) = (Count(X) = 0);

     function Union(X, Y : Set) return Set
       is abstract with
         Post'Class =>
           Count(Union'Result) = Count(X) + Count(Y);

     type R is record
        X : Positive := 0
          with Independent;
        Y : Natural := 77
          with Atomic;
     end record;

     type Shared_Bit_Vector is array(0..15) of Boolean
       with Packing, Independent_Components;

     type Bit_Vector is array(0..15) of Boolean
       with Component_Size => 1;

[Find the rest of this message in AI05-0147-1.]

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

From: Bob Duff
Sent: Tuesday, February 24, 2009  10:25 AM

> I'll admit I have been bitten by the syntax bug (thanks, Randy!) for 
> pre- and postconditions, and with invariants coming up I suspect it 
> will continue.  Here is a general proposal that avoids introducing new 
> reserved words, but is quite
> flexible:
> 
>   To specify aspects of an entity (at least "operational" ones)
>   and link them directly to the associated declaration,
>   consider a general syntax of:
> 
>    <declaration>
>      WITH
>        <aspect_name> [=> <aspect_value>],
>        <aspect_name> [=> <aspect_value>],
>        ... ;

I'm not 100% convinced we need syntax (maybe 90%?), but if we do, I definitely
like this proposal.  Much nicer than adding a whole bunch of special-case
syntax for all the cases we need, along with the requisite reserved words.

> The notation <aspect_name>'Class was intended to imply an inherited, 
> non-overridable aspect.

Seems a little bit odd, to me.  I suppose I could get used to it, but I would
have said "Class_Invariant" rather than "Invariant'Class".

>...The 'Class
> might be implicit for abstract tagged types and their  primitive 
>subprograms.

Sounds confusing.  Especially since abstract types can have concrete procedures.
Make the "'Class" or "Class_" explicit.

[Find the rest of this message in AI05-0147-1.]

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

From: Robert Dewar
Sent: Thursday, February 26, 2009  12:09 AM

I agree with this, BTW, I find Tuck's syntax suggestion basically nice, and
think that pre/post conditions are important enough to warrant syntax additions.
[What he's agreeing to can be found in AI05-0146-1 - ED]

I do think that postconditions in the body are useful, and so would keep the
pragmas, certainly in GNAT anyway. It is true that preconditions in the body
are just assertions, so they are there just for symmetry, but postconditions
in the body are useful in that they come up front, which is the right position,
and they block all exits (which would be tedious to do manually with assertions).
I also think it is good to be able to control pre/post conditions separately
from normal assertions.

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

From: Bob Duff
Sent: Thursday, February 26, 2009  7:34 AM

> postconditions in the body are useful in that they come up front, 
> which is the right position, and they block all exits (which would be 
> tedious to do manually with assertions).

It is true that it's useful.  But it's a kludge.  The general problem is that
there's nowhere to put some code that you want executed on every exit point.
This solves the problem for the case where that code happens to be an assertion.

But I'm not going to fight against pre/postconditions in bodies.

>... I also think it is good to be able to control  pre/post conditions 
>separately from normal assertions.

Yes.  Precondition failures should be blamed an on the caller, postcondition
and invariant failures should be blamed on the callee.  So if you have a
library, you might have confidence (from testing, and maybe from running
SofCheck's Inspector) that it works, so you want to turn off postcondition
and invariant checks, but keep precondition checks on.

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

From: Robert Dewar
Sent: Friday, February 27, 2009  11:14 AM

...
> It is true that it's useful.  But it's a kludge.  The general problem 
> is that there's nowhere to put some code that you want executed on every exit point.
> This solves the problem for the case where that code happens to be an 
> assertion.

I would be happy to have the more general form. As you know the Ada compiler
internally has a construct AT END:

     begin
        ...
     at end
        ...
     end;

which is essentially useful for translation of several constructs, and which would
be indeed be a useful programming construct (it would be amazingly easy to implement
this in GNAT :-))
 
> But I'm not going to fight against pre/postconditions in bodies.
> 
>> ... I also think it is good to be able to control pre/post conditions 
>> separately from normal assertions.
> 
> Yes.  Precondition failures should be blamed an on the caller, 
> postcondition and invariant failures should be blamed on the callee.  
> So if you have a library, you might have confidence (from testing, and 
> maybe from running SofCheck's Inspector) that it works, so you want to 
> turn off postcondition and invariant checks, but keep precondition checks on.

Right, and that might be independent of assertions (in the case of body postconditions).
Of course in GNAT you have the nice generalization of pragma Check, which allows you
to assign a name to an arbitrary group of assertions which can then be controlled as a
group.

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

From: Arnaud Charlet
Sent: Friday, February 27, 2009  11:21 AM

> I would be happy to have the more general form. As you know the Ada 
> compiler internally has a construct AT END:
> 
>     begin
>        ...
>     at end
>        ...
>     end;
> 
> which is essentially useful for translation of several constructs, and 
> which would be indeed be a useful programming construct (it would be 
> amazingly easy to implement this in GNAT :-))

Indeed, and no new reserved word is even needed.

Delphi also has this capability BTW (and if I remember well, it's also
spelled "at end", or something very close).

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

From: Bob Duff
Sent: Friday, February 27, 2009  12:17 AM

> Indeed, and no new reserved word is even needed.

This is another feature that was proposed as part of Ada 9X, and rejected
(primarily as a general size-of-change reduction, rather than objections
to the feature itself).  It was thought that this feature isn't really needed,
because you can achieve the same thing via finalization, albeit rather verbosely.

I'm not particularly pushing for or against this feature...

> Delphi also has this capability BTW (and if I remember well, it's also 
> spelled "at end", or something very close).

So does Java: try/finally, and misc other languages.

Java is an interesting case because finalization is so badly broken, so people
use try/finally fairly heavily.

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

Questions? Ask the ACAA Technical Agent