Version 1.4 of ais/ai-00288.txt

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

!standard 11.5 (00)          04-02-29 AI95-00288/02
!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- and Postconditions
!summary
To augment the basic "assert" pragma capability proposed in AI-00286, 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 Pre_Assert, Classwide_Pre_Assert, Post_Assert, and Classwide_Post_Assert have the following form:
pragma Pre_Assert(subprogram_local_name,
boolean_expression [, [Message =>] string_expression]);
pragma Classwide_Pre_Assert(dispatching_subprogram_local_name,
boolean_expression [, [Message =>] string_expression]);
pragma Post_Assert(subprogram_local_name,
boolean_expression [, [Message =>] string_expression]);
pragma Classwide_Post_Assert(dispatching_subprogram_local_name,
boolean_expression [, [Message =>] string_expression]);
The (dispatching_)subprogram_name must name the immediately preceding subprogram. For Classwide_Pre_Assert and Classwide_Post_Assert, 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 nonlimited formal parameters, yielding the value of the formal parameter at the beginning of the execution of the procedure.
If a Classwide_Pre_Assert or Classwide_Post_Assert pragma is specified for a primitive subprogram, then it also applies to all overridings of the primitive. By contrast, Pre_Assert/Post_Assert pragmas may be applied to non-primitive subprograms, and are not inherited.
For a Classwide_Pre_Assert or Classwide_Post_Assert, 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_Pre_Asserts), 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_Pre_Assert that applies to the subprogram named in the call, then the rules for checking preconditions ensure that so long as this Classwide_Pre_Assert 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/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.
!wording
!discussion
NOTE: We have changed the names of the pragmas to use the terms Pre_Assert and Post_Assert rather than Precondition and Postcondition, because of objections that precondition/postcondition are terms reserved for static analysis.
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( ...; 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; -- or Ada.Exceptions.Raise_Exception(..., <message>) end if;
declare -- save incoming values of nonlimited in/out params -- referenced in postconditions Nonlimited_Inout_Param1'Incoming : 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; -- 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. ;-)
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 Pre_Assert_Policy, and Post_Assert_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 Pre_Assert(Push, not Is_Full(S)); pragma Post_Assert(Push, not Is_Empty(S));
procedure Pop(S : in out Stack; I : out Item); pragma Pre_Assert(Pop, not Is_Empty(S)); pragma Post_Assert(Pop, not Is_Full(S));
function Top(S : in Stack) return Item; pragma Pre_Assert(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.

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

From: Alan Burns
Sent: Tuesday, January 7, 2003,  5:01 AM

he HRG was asked (by ARG) to look at these AIs on
assert and pre/post conditions etc.

Please find attached our considerations (which
was on the whole are not supportive). To prevent these
thoughts getting lost, perhaps they should be
incorporated into the AIs

----

Comment from the HRG on AI288 - Pre/Postconditions and Invariants

The AI proposes the extension of the assertion mechanism (AI286) to
provide support for "programming by contract".  Specifically it provides
a mechanism to express pre and postconditions for operations and
statements about invariant properties of types and packages.

As with AI286, the fundamental question to be answered is "does the
proposal aid the construction and verification of high-integrity,
software-driven systems"?

The proposal has a number of problems that, in the HRG's opinion,
results in a negative answer to this question.
In particular, as presented, the AI describes a mechanism that is
more suitable for debugging than constructing a system "by contract".
The author appears to recognise this by stating its aim as: "to ... catch
errors in usage or implementation earlier in the development cycle".

Specific weakness in the proposal include the following:

1.  It is built on the Assert mechanism proposed in AI286 and
shares all the problems associated with that AI.  Indeed, some of those
weaknesses are more severe if assert is to be employed in the
way proposed.  In particular, the desire to promote the contract to
package specifications is fundamentally incompatible with the visibility
rules of Ada.  How, for example, will the invariant condition of an
abstract state machine package be expressed in its specification if the
data to which the invariant applies is, correctly, hidden in the package
body?  Only a proliferation of extra functions (perhaps with side-
effects?) can be employed.

2. Although the attribute "incoming" provides the initial value of
parameters that are imported and exported by an operation, there is no
equivalent mechanism for global variables used by the operation. This
makes it impossible to express pre and post conditions that rely on the
initial values of global variables.  Since such globals may well be
invisible at the point where the pre/post condition is being expressed,
this deficiency may well be insoluble.

Trivial example:

X : Integer;
...
procedure Inc is
begin
  X := X + 1;
end Inc;

The postcondition of Inc, "X = X'Incoming + 1, cannot be expressed.
Furthermore, the value X'Incoming cannot be provided by the compiler
because, unlike a parameter which has its mode, we don't know whether a
global is referenced or updated until we reach the sequence of
statements in the subprogram body. The initial value could only be
provided if some form of flow analysis was performed before compilation.

3.  The AI proposes that postconditions are evaluated at the end of a
subprogram's normal execution but before any copying back of exported
parameters.  Unfortunately, if the postcondition assertion fails, then
any parameters passed by reference and updating global variables will
already have been modified.  The system "state" is therefore in an
unknown condition when the exception is raised making its use in
deployed systems problematic.  The fact that system behaviour after a
failed postcondition depends on the parameter passing mechanism used
introduces a new and unwelcome form of "undefined" behaviour which is
inappropriate for the high-integrity systems at which the AI is aimed.

4.  The proposed freedom to allow any form of pre and postcondition for
overidden tagged operations is dangerously flawed.  For any sensible
tagged type hierarchy, it must be the case that:

Root op precondition        -> Overridden op precondition and
Overridden op postcondition -> Root op postcondition.

In other words, an overriding operation must "ask less and promise
more".  These rules are well established by the work of  Barbara Liskov
and Jeannette Wing and are partially implemented in Eiffel.  Any attempt
to present Ada as providing "programming by contract" which was even
weaker than Eiffel in this respect would be very harmful to the
credibility of the language.

Conclusion
----------

The HRG cannot support this proposal in its current form.

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

From: Tucker Taft
Sent: Tuesday, January 7, 2003,  6:00 AM

Well, that is a "pan" if I ever saw one ;-).

However, I am wondering whether the HRG had any notion
of what "form" of proposal they might support?

... or do they conclude that any improvement in this area
is beyond the scope of the standard?  In other words,
was the ultimate suggestion "drop it" or "try harder"?

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

From: Alan Burns
Sent: Tuesday, January 7, 2003,  7:21 AM

In such stark terms I think the view was "drop it", but let me
deconstruct that a bit. The HRG looked at these as `do they
help verification', in other words do they help static analysis.
And the view was no they do not (for reasons explained in the
emails). But if you view these AIs as helping construct run-time
checks for protected execution then they may well be fine.

The HRG does not believe that the static analysis and dynamic protection
can be obtained from the same language primitives. Static analysis
needs so much extra stuff (specifications, visibility into inner
scopes etc) if these are represented as comments then there is no
confusion. Run-time checks are part of the execution and have a
different role.

So do not drop it if there is value in terms of dynamic protection,
just put the emphasis there.

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


Questions? Ask the ACAA Technical Agent