!standard 11.5 (00)                                09-11-02  AI05-0145-2/02
!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
to allow the specification of pre/postconditions for subprograms
and entries.

We presume the use of the "aspect_specification" syntax defined in
AI05-0183-1.

!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

Using the aspect_specification syntax, we propose to allow the
specification of pre/postconditions for subprograms and entries. 
The aspects Pre and Post are used for this purpose.  In addition, for
primitive subprograms of tagged types, the aspects Pre'Class and
Post'Class are also available.  These aspects are inherited by the
corresponding primitive subprogram of types descended from the original
tagged type. When multiple preconditions apply to a subprogram, they are
"or"ed together (that is, if any of the preconditions is satisfied, the
overall precondition is satisfied).  When multiple postconditions apply
to a subprogram, they are "and"ed together (that is, all of the
postconditions must be satisfied for the overall postcondition is
satisfied).

!wording


Modify 3.9.3(1.1/2):

  abstract_subprogram_declaration :=
    subprogram_specification IS ABSTRACT
      [aspect_specification];
    
Modify 6.1(2/2):

  subprogram_declaration ::=
    [overriding_indicator]
    subprogram_specification
      [aspect_specification]

Modify 6.7(2/2):

  null_procedure_declaration ::=
    procedure_specification IS NULL
      [aspect_specification];

Modify 9.5.2(2/2):

  entry_declaration ::=
    [overriding_indicator]
    ENTRY defining_identifier [(discrete_subtype_definition)] parameter_profile
      [aspect_specification];

Add a new section:

  13.3.2 Preconditions and Postconditions

  Preconditions and postconditions may be specified for subprograms and
  entries, using an aspect_specification for aspect Pre, Pre'Class,
  Post, or Post'Class. The expression associated with a Pre or Pre'Class
  aspect is called a *precondition expression*, and the expression
  associated with a Post or Post'Class aspect is called a *postcondition
  expression.*

           Name Resolution
           
  The expected type for a precondition or postcondition expression is
  the predefined type Boolean.  Within a postcondition expression of a
  function, the attribute Result is defined for the function, yielding
  the value returned by the function.  Within a postcondition expression
  of a subprogram or entry with at least one IN OUT formal parameter of a
  nonlimited type, the attribute Old is defined for each such formal
  parameter, yielding the value of the formal parameter at the beginning
  of the execution of the subprogram or entry.

  Within the expression for a Pre'Class or Post'Class aspect for a
  primitive subprogram of a tagged type T, a name that denotes a formal
  parameter of type T is converted to T'Class.  Similarly, a name that
  denotes a formal access parameter of type access-to-T is converted to
  access-to-T'Class. Finally, if the subprogram is a function returning
  T or access T, the Result attribute is converted to T'Class or
  access-to-T'Class, respectively.  [Redundant: This ensures the
  expression is well-defined for a primitive subprogram of a type
  descended from T.]
  
          Legality Rules
          
  The Pre or Post aspect shall not be specified for an abstract
  subprogram. [Redundant: Only the Pre'Class and Post'Class aspects may
  be specified for such a subprogram.]

          Static Semantics
          
  If a Pre'Class or Post'Class aspect is specified for a primitive
  subprogram of a tagged type T, then the associated precondition
  expression also applies to the corresponding primitive subprogram of
  each descendant of T.
  
          Dynamic Semantics
          
  If one or more precondition expressions apply to a subprogram or
  entry, and the Assertion_Policy in effect at the point of the
  subprogram or entry declaration is Check, then upon a call of the
  subprogram or entry, after evaluating any actual parameters, a
  precondition check is performed. This consists of the evaluation of
  the precondition expressions that apply to the subprogram or entry. If
  and only if all the precondition expressions evaluate to False, then
  Ada.Assertions.Assertion_Error is raised.  The order of performing the
  checks is not specified, and if any of the precondition expressions
  evaluate to True, it is not specified whether the other precondition
  expressions are checked. It is not specified whether any check for
  elaboration of the subprogram body is performed before or after the
  precondition check.  It is not specified whether in a call on a
  protected operation, the check is performed before or after starting
  the protected action.  For an entry call, the check is performed prior
  to checking whether the entry is open.

  If one or more postcondition expressions apply to a subprogram or
  entry, and the Assertion_Policy in effect at the point of the
  subprogram or entry declaration is Check, then upon successful return
  from a call of the subprogram or entry, prior to copying back any
  by-copy IN OUT or OUT parameters, a postcondition check is performed.
  This consists of the evaluation of the postcondition expressions that
  apply to the subprogram or entry.  If any of the the postcondition
  expressions evaluate to False, then Ada.Assertions.Assertion_Error is
  raised. 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 or OUT parameters are performed
  before or after the postcondition check.

  If a precondition or postcondition check fails, the exception is
  raised at the point of the call.  [Redundant: The exception cannot
  be handled inside the called subprogram.]

  For a dispatching call or a call via an access-to-subprogram value,
  the precondition or postcondition check performed is determined by the
  subprogram actually invoked.  [Redundant: Note that for a dispatching
  call, if there is a Pre'Class aspect that applies to the subprogram
  named in the call, then if the precondition expression for that aspect
  evaluates to True, the precondition check for the call will succeed.

  [Redundant: If the Assertion_Policy in effect at the point of a
  subprogram or entry declaration is Ignore, then no precondition or
  postcondition check is performed on a call on that subprogram or entry.]

!discussion

This is based on AI05-145-1. The Pre/Post aspects are specified using
the aspect_specification syntax defined in AI05-0183-1. There is no
message associated with the failure of a precondition or postcondition
check: it was deemed that these annotations 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, except for indirect calls, where a wrapper will be
required if the caller normally performs the checks. Note however that
the callee cannot handle the Assertion_Error, as there seems no reason
to allow that degree of implementation dependence.

These aspects can be specified for protected operations and for
protected and task entries. It appears necessary that preconditions on
entries be evaluated by the caller, because their failure should take
place before the caller is suspended waiting on the entry queue. In the
case of an entry that implements a primitive subprogram, the
preconditions would have to be checked by the "wrapper" prior to calling
the entry.  We allow the precondition check to be performed inside or
outside the protected action associated with a protected subprogram
call.

!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


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