!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

!summary

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.

!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 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.

!proposal

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.

!wording


!discussion

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.

!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)
       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


!appendix


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