Version 1.1 of ai05s/ai05-0145-2.txt

Unformatted version of ai05s/ai05-0145-2.txt version 1.1
Other versions for file ai05s/ai05-0145-2.txt

!standard 11.5 (00)          09-06-12 AI05-0145-2/01
!standard 11.4.1 (10)
!class amendment 09-06-12
!status work item 09-06-12
!status received 09-06-12
!priority Medium
!difficulty Medium
!subject Pre- and Postconditions
To augment the basic "assert" pragma capability in Ada 2005, we propose a notation for specifying pre- and post-conditions for subprograms, including null and abstract operations on interfaces, and subprograms and entries of synchronized types.
The notation uses the notion of "aspect specification" used for other representation aspects and for type invariants.
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 they really represents part of the contract. In particular, one wants any implementation of a given operation to conform to 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.
The following aspects are defined for subprograms and entries:
Pre, Post, Inherited_Pre, Inherited_Post.
The syntax of subprogram and entry declarations is modified as follows:
subprogram_declaration ::= [overriding_indicator] subprogram_specification; [aspect_specification]
abstract_subprogram_declaration := subprogram_specification is abstract; [aspect_specification];
null_procedure_declaration ::= procedure_specification is null; [aspect_specification];
entry_declaration ::= [overriding_indicator] entry defining_identifier [(discrete_subtype_definition)] parameter_profile; [aspect_specification];
aspect_specification ::= with aspect_mark => boolean_expression {,aspect_mark => boolean-expression};
We say that a Pre aspect, a Post aspect, an Inherited_Pre aspect, an Inherited_Pro aspect, specify respectively a Precondition, a Postcondition, an Inherited_Precondition or an Inherited_Postcondition of the subprogram or entry.
At most one occurrence of each aspect is allowed for a subprogram or entry. declaration. For an Inherited_Precondition or Inherited_Postcondition, the subprogram must be a dispatching subprogram. The boolean expression is defined within the context of the specification of the operation so that the formal parameter names (and the entry family index) are directly visible.
The names in the boolean_expression of a Precondition or Postcondtion are resolved not at the point of the declaration, but rather at the freezing point of the operation.
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 is specified for a primitive subprogram, then it also applies to all its overridings. By contrast, Pre/Post aspects may be also be applied to non-primitive subprograms, and are not inherited. For abstract subprograms, only Inherited_Pre/Postconditions are meaningful.
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 pre or post aspect have the type specified in the subprogram's parameter profile.
If the assertion policy in effect at the point of a subprogram or entry declaration that includes an aspect specification is "Check," then upon a call on the specified subprogram or entry, after evaluating the actual parameters and making the parameter associations, the check associated with the aspect is performed. This consists of the evaluation of the boolean expression, If the expression is False, then Ada.Assertions.Assertion_Error is raised.. It is not specified whether any check for elaboration of the subprogram body is performed before or after the precondition check.
If multiple Preconditions apply to the same subprogram (through inheritance of Inherited_Pre aspects), 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 Post aspect specification 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,. 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 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. 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 Pre/Post aspect specification is "Check" then the semantics are as described above. If the assertion If the assertion policy at the point of the specification is "Ignore" then the aspect has no effect.
This is based on AI05-145-1. The Pre/Post aspects are specified using the syntax introduced for AI-0146. There is no message associated with the failure of an aspect check: it was deemed that these aspects are intended for verification, and that for debugging purposes the Assert pragma is sufficient.
The new version preserves the flexibility of the previous one concerning the point at which the aspect is checked: either callee or caller can perform the check, and the failure or a postcondition may be (but need not be) handled in the faulty caller itself.
These aspects can be specified for protected operations and for protected and task entries. It appears necessary that preconditions on tasks entries be evaluated by the caller, because their failure should take place before the rendezvous is attempted.
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) with Pre => not Is_Full(S), Post => not Is_Empty(S);
procedure Pop(S : in out Stack; I : out Item) with Pre => not Is_Empty(S), Post => not Is_Full(S);
function Top(S : in Stack) return Item with Pre => not Is_Empty(S);
function Is_Valid_Stack(S : in Stack) return Boolean;
Stack_Error : exception; private -- whatever end Stacks;
!ACATS test


Questions? Ask the ACAA Technical Agent