Version 1.2 of ais/ai-00288.txt

Unformatted version of ais/ai-00288.txt version 1.2
Other versions for file ais/ai-00288.txt

!standard 11.5 (00)          02-03-08 AI95-00288/01
!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 Pre/Postconditions and Invariants
!summary
To augment the basic "assert" pragma capability proposed in AI-00286, we propose pragmas for specifying pre/post conditions for subprograms, and invariants for packages and types.
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 and/or the use of invariants associated with types or modules (i.e. packages). 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 and invariants appeared on the specification of the subprograms, types, and packages 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 and invariants 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 and invariants 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
Preconditions and Postconditions:
The pragmas Precondition, Classwide_Precondition, Postcondition, and Classwide_Postcondition have the following form:
pragma Precondition(subprogram_local_name,
boolean_expression [, [Message =>] string_expression]);
pragma Classwide_Precondition(dispatching_subprogram_local_name,
boolean_expression [, [Message =>] string_expression]);
pragma Postcondition(subprogram_local_name,
boolean_expression [, [Message =>] string_expression]);
pragma Classwide_Postcondition(dispatching_subprogram_local_name,
boolean_expression [, [Message =>] string_expression]);
The (dispatching_)subprogram_name must name the immediately preceding subprogram. For Classwide_Precondition and Classwide_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.
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 "Incoming" is defined on each of the IN OUT elementary formal parameters, yielding the value of the formal parameter at the beginning of the execution of the procedure.
If a Classwide_Precondition or Classwide_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 a Classwide_Precondition or Classwide_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 Classwide_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 a Classwide_Precondition that applies to the subprogram named in the call, then the rules for checking preconditions ensure that so long as this Classwide_Precondition is satisfied, the overall precondition check will succeed (because if any precondition evaluates to True, the call proceeds normally).
Invariants
The pragmas Package_Invariant, Type_Invariant, and Classwide_Type_Invariant have the following form:
pragma Package_Invariant(package_local_name,
boolean_function_name [, [Message =>] string_expression]);
pragma Type_Invariant(first_subtype_local_name,
boolean_function_name [, [Message =>] string_expression]);
pragma Classwide_Type_Invariant(tagged_first_subtype_local_name,
boolean_function_name [, [Message =>] string_expression]);
The package_local_name for Package_Invariant must denote the immediately enclosing program unit, which must be a package. The boolean_function_name for Package_Invariant must denote a parameterless function declared within the specified package that has a Standard.Boolean result.
The first_subtype_local_name for Type_Invariant must denote a first subtype declared in the immediately enclosing region, which must be a package. The boolean_function_name for Type_Invariant must denote a function with one parameter of the type denoted by the first_subtype_local_name, and a Standard.Boolean result.
The tagged_first_subtype_local_name for Classwide_Type_Invariant must denote a tagged first subtype declared in the immediately enclosing region, which must be a package. The boolean_function_name for Classwide_Type_Invariant must denote a dispatching function with one parameter of the type denoted by the tagged_first_subtype_local_name, and a Standard.Boolean result.
If the assertion policy at the point of an invariant pragma is "Check," then the associated check is performed at the following places:
* For a Package_Invariant pragma, upon return
from a call on any procedure defined within the declarative region of the package that is visible outside the package, a call is performed on the specified parameterless function; also, immediately after completing elaboration of the package.
* For a Type_Invariant pragma, upon return from a call
on any procedure that
- has one or more [IN] OUT parameters of the specified type, - is defined within the immediate scope of the type, and - is visible outside the immediate scope of the type,
one call is performed on the specified boolean function for each such [IN] OUT parameter. Similarly, after evaluation of a function call or type converstion that returns the specified type, a call is performed on the specified boolean function passing the result. Finally, after default initialization of an object of the type, a call is performed on the specified boolean function passing the default-initialized object.
* For a Classwide_Type_Invariant pragma, upon return from a call
on any procedure that
- has one or more [IN] OUT parameters of a type within the
derivation class of the specified type,
- is defined within the immediate scope of the type, and - is visible outside the immediate scope of the type,
one call is performed on the specified boolean dispatching function for each such [IN] OUT parameter. The parameter is view-converted to the class-wide type prior to the call, ensuring that the call is a dispatching call. Similarly, after evaluation of a function call or type conversion that returns a type within the derivation class, a dispatching call is performed on the specified boolean function passing the result. Finally, after default initialization of an object of a type within the derivation class, a dispatching call is performed on the specified boolean function passing the default-initialized object.
If any of these calls return False, Ada.Assertions.Assertion_Error is raised, with the specified Message if any.
The invariant checks are performed prior to copying back any by-copy [IN] OUT parameters. However, it is not specified whether any constraint checks associated with the copying back are performed before or after the invariant checks. If there are any postconditions associated with the procedure, it is not specified whether these checks are performed before, after, or interleaved with the invariant checks.
Assertion Policy
If the assertion policy at the point of a pre/postcondition or invariant 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. If the assertion policy at the point of the pragma is "Assume_True" then if the check associated with the pragma would have failed, execution is erroneous. If the assertion policy at the point of the pragma is "Evaluate_And_Assume_True" then the evaluations necessary to do the check are performed, but if the check fails, execution is erroneous.
!wording
!discussion
Pre/Postcondition Pragmas
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 "Classwide_" 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 "Classwide_" version necessarily must be less specific, i.e. less "tight," and hence cannot catch as many bugs by itself as the combination of an inherited condition and a condition specific to a particular body.
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( ...; Elementary_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; -- or Ada.Exceptions.Raise_Exception(..., <message>) end if;
declare -- save incoming values of elementary in/out params Elementary_Inout_Param1'Incoming : constant Inout_Type1 := Elementary_Inout_Param1; ... -- other elementary in/out params begin
-- Call the "real" procedure Proc(..., Elementary_Inout_Param1, ...);
-- 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 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. ;-)
Invariant Pragmas
We have provided both type oriented and package oriented "invariant" pragmas. This reflects the fact that some abstractions are for abstract data types, while others are for abstract state machines. We only enforce the package-oriented invariant on return from visible procedures of the package. If a visible function has side-effects, the implementor may want to insert an explicit postcondition on the function, or a Assert pragma inside.
For type invariants, we apply them on [IN] OUT parameters of procedures after the call, and on the result of functions and conversions.
The invariants are defined by referring to a boolean function. The more general boolean_expression allowed in the other assertion-like pragmas was not used because it was unlikely that the invariant could be defined in terms of visible entities, and there was no obvious way to refer to the particular instance of the type for the Type_Invariant pragma. In addition, given that the checks may be performed at the call point, space economization argues for bundling the invariant into a callable subprogram. The programmer might as well do this bundling him/herself.
Invariant checks apply to all calls on (relevant) procedures declared in the visible part of the package, even those within the package. This allows the checks to be performed inside the procedures rather than at the call point, and makes the invariant pragmas equivalent to a series of postcondition pragmas. We considered making invariant checks apply only to calls from outside the package, but this appeared to complicate the implementation and description with little additional benefit.
The invariant checks are performed as postcondition checks to ensure that violations are caught as soon as possible. Presumably the invariants could also be enforced as preconditions, but those checks would in general be redundant, and the failures would be harder to track down since the call that actually created the problem would be harder to identify.
We do not specify any inheritance of invariant pragmas. It might make sense for a type invariant to be inherited by its descendants. However, in that case, a separate Inheritable_Type_Invariant would probably be appropriate, based on the same argument given above relating to inheritable pre/postcondition pragmas. Presumably we would allow these pragmas in generic packages, with the obvious semantics in the instance.
We have not specified whether the invariants apply to any inherited primitive subprograms that are implicitly declared within the package containing the pragma. We have not specified whether invariants apply to dynamically-bound calls, which might reach subprograms that are not declared in the visible part of the package. Clearly these issues need to be resolved.
Assertion Policy
We have used the Assertion_Policy pragma defined in AI-00286, with the same options and interpretation. It might make sense to define separate pragmas, such as Precondition_Policy, Postcondition_Policy, and Invariant_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.
!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; pragma Type_Invariant(Stack, Is_Valid_Stack);
Stack_Error : exception; private -- whatever end Stacks;
!ACATS test
!appendix

From: Tucker Taft
Sent: Wednesday, February 6, 2002,  12:19 PM

The semantics for inheritable preconditions is probably not quite
right in this proposal.  It should be possible to "weaken" preconditions
as you go down the type hierarchy.  This would imply that an
inherited precondition should be "or'ed" with the preconditions
specified directly on a subprogram, or perhaps simply overridden.

Probably the simplest is to say that an inherited precondition
represents a "default" precondition, which is overridden by
any other precondition specified directly on a primitive.
So if both Inherited_Precondition and Precondition are specified
on a primitive, then only the Precondition applies to the
primitive itself, while the Inherited_Precondition is the default
precondition for any overridings of the primitive.
If Inherited_Precondition is specified on an overriding, it becomes
the default for further overridings, replacing the Inherited_Precondition
applicable to the parent type's primitive.

This means that a precondition can be either strenghtened or
weakened as you go down a type hierarchy, but by default,
it stays the same.  Strengthening a precondition as you go
down is a little weird, but not completely inappropriate.

The true "classwide" precondition for a primitive would be the "and"
of the specific preconditions on each implementation of the primitive.
It would be wise for a user to define the Inherited_Precondition so
that it matches this combination, or is stronger than it.  But it is
probably not practical to try to enforce this, nor is it wise to
implicitly "weaken" a precondition specified explicitly on a primitive by
"or"ing in the Inherited_Precondition.

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

From: Robert Dewar
Sent: Sunday, March 10, 2002,  11:05 AM

I find this the kind of proposal that should be made AFTER people have
some experience with the facility. If you can't get anyone to implement
a trial version, then that is itself an indication that the proposal is
reaching. I certainly don't see any serious users of Ada champing at the
bit for this type of capability, but it would seem quite reasonable for
someone to experiment with the implementation of something like this.

I certainly do NOT think it is reasonable to try to even semi-standardize
a facility of this kind without implementation and usage experience.

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

From: Tucker Taft
Sent: Monday, March 11, 2002,  9:01 PM

> > Also, we do provide an inheritable type invariant,
> > even though the discussion says we don't.   Sorry about that...
>
> Umm, I can't find anything in the proposal that says that either
> Type_Invariant or Class_Type_Invariant is inherited. Thus, I left the
> discussion alone.

The Class_Type_Invariant applies to all types in the
derivation class, so that implies it is inherited.

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

From: Randy Brukardt
Sent: Monday, March 11, 2002,  9:16 PM

Humm, OK, I didn't view that as "inheritance". (The difference between
classwide operations and inherited ones is very important to keep straight
in Ada.) What else with a class_type_invariant apply to except to all
members of the class?

But if this is inheritance, you would need to say something about overriding
(as you did for pre and post conditions). OTOH, if it is additive, then it
isn't inheritance (at least not in the traditional sense).

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

From: Tucker Taft
Sent: Friday, October 18, 2002,  4:00 PM

When we last discussed AI-288, which introduced the concept
of pre/post condition pragmas (and invariants), we expressed
concern about the infinite recursion problem, if a two subprograms
were mutually recursive when the pre/post conditions were
taken into account.  An example used was:

    function Is_Empty(S : Stack) return Boolean;
    pragma Postcondition(Is_Empty, not (Is_Empty'Result and Is_Full(S)));

    function Is_Full(S : Stack) return Boolean;
    pragma Postcondition(Is_Full, not (Is_Full'Result and Is_Empty(S)));

Apparently Eiffel suppresses pre/post conditions when evaluating
pre/post conditions.  This seems like a kludge, and certainly
makes implementation significantly harder, since you need
non-checking versions, and you have to compile pre/post conditions
using a different mode.

In thinking more about this, the simplest solution seems to be
"programmer beware."  The above example is not a very good one,
and perhaps if there were a more convincing example I would
be more sympathetic, but it seems easy enough for the programmer
to watch out for these situations.

In general, the functions used in pre/post conditions should
be pure (or nearly so ;-), and should not have significant
preconditions of their own.  Postconditions on a function
seem like somewhat odd beasts in any case, and would probably
be used sparingly.  They would presumably express properties
of the returned value such as /= 0, or /= null.   Using them
to express an identity would seem to be adequately handled
by having the identity on only one of the functions involved,
rather than on both.  E.g.

    function "/="(Left, Right : T) return Boolean;
    pragma Postcondition("/=", "/="'Result = not (Left = Right));

There would seem no need to put the complementary identity
on the "=" function.

Similarly, one might express the effect of "<", "<=", and ">="
in terms of ">", but then it would be odd to express the
effect of ">" in terms of "<", because then you effectively
have a circular definition.

In any case, in my revision of AI-288 (which will also be
split into two), I plan to propose to treat the problem of
infinite recursion for pre/post conditions as the programmer's
problem, rather than the implementor's problem.

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

From: Robert A. Duff
Sent: Friday, October 18, 2002,  4:31 PM

>   Postconditions on a function
> seem like somewhat odd beasts in any case, and would probably
> be used sparingly.  They would presumably express properties
> of the returned value such as /= 0, or /= null.

Please explain why they are "odd beasts".  I agree that they normally
"express properties of the returned value".  But why are the examples
"/= 0, or /= null" usual?  Why not properties expressed in terms of the
input parameters?

> In any case, in my revision of AI-288 (which will also be
> split into two), I plan to propose to treat the problem of
> infinite recursion for pre/post conditions as the programmer's
> problem, rather than the implementor's problem.

That seem wise.  I can't think of any better way to deal with mutual
recursion.

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


Questions? Ask the ACAA Technical Agent