Version 1.4 of ai05s/ai05-0145-1.txt
!standard 11.5 (00) 09-02-16 AI05-0145-1/02
!standard 11.4.1 (10)
!class amendment 09-02-15
!status No Action (9-0-0) 10-02-27
!status work item 09-02-15
!status received 09-02-15
!priority Medium
!difficulty Medium
!subject Pre- and Postconditions
!summary
To augment the basic "assert" pragma capability in Ada 2005,
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 Precondition, Inherited_Precondition, Postcondition,
and Inherited_Postcondition have the following form:
pragma Precondition(subprogram_local_name,
[Check =>] boolean_expression [, [Message =>] string_expression]);
pragma Inherited_Precondition(dispatching_subprogram_local_name,
[Check =>] boolean_expression [, [Message =>] string_expression]);
pragma Postcondition(subprogram_local_name,
[Check =>] boolean_expression [, [Message =>] string_expression]);
pragma Inherited_Postcondition(dispatching_subprogram_local_name,
[Check =>] boolean_expression [, [Message =>] string_expression]);
The (dispatching_)subprogram_name must name the immediately preceding
subprogram. For Inherited_Precondition and Inherited_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.
The names in the boolean_expression of a precondition
or postcondition pragma are resolved not at the point
of the pragma, but rather at the freezing point of the
named subprogram, or at the end of the immediately
enclosing visible part, whichever comes first.
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 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 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 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 Inherited_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 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 precondition or postcondition
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
This is based on AI95-0288.
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 "Inherited_" 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 "Inherited_" version necessarily must be
less specific to the particular body (Inherited_Precondition must be
more restrictive, and Inherited_Postcondition must be more lax), and
hence cannot catch as many bugs by itself as the combination of an
inherited condition and a condition specific to a particular body.
We defer resolving the names in the boolean_expression
because it is natural for preconditions or postconditions
to refer to other subprograms declared in the same
scope, and requiring that there be no forward references
unduly restricts the expressions.
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
--
begin
--
if not <precondition_bool_expr1>
and then not <precondition_bool_expr2>
and then not ...
then
raise Ada.Assertions.Assertion_Error [with <message>];
end if;
declare
--
--
Nonlimited_Inout_Param1'Old : constant Inout_Type1 :=
Nonlimited_Inout_Param1;
... --
begin
--
Proc(..., Nonlimited_Inout_Param1, ...);
--
if not <postcondition_bool_expr> then
raise Ada.Assertions.Assertion_Error [with <message>];
end if;
... --
end;
end Proc_with_check;
function Func_with_check(...) return Result_Type is
--
begin
--
if not <precondition_bool_expr1>
and then not <precondition_bool_expr2>
and then not ...
then
raise Ada.Assertions.Assertion_Error;
--
end if;
declare
--
--
Func'Result: Result_Type renames Func(...);
begin
--
if not <postcondition_bool_expr> then
raise Ada.Assertions.Assertion_Error;
--
end if;
... --
--
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 of Ada 2005, with the same
options and interpretation. It might make sense to define separate
pragmas, such as Precondition_Policy, and Postcondition_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.
Inherited vs. Inheritable vs. Classwide vs. ...
We considered other names for Inherited_Precondition and Inherited_Postcondition.
The Ada 95 AI used "Classwide_Precondition." We also considered
"Inheritable_Precondition", though that sounded a bit like a disease.
In the end we went with what seemed the simplest name that conveyed
the intent.
!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;
Stack_Error : exception;
private
--
end Stacks;
!ACATS test
!appendix
From: Tucker Taft
Sent: Sunday, February 15, 2009 3:56 PM
This is a resurrection of AI95-00288, on pre- and postconditions.
It is virtually unchanged. The proposed pragma names are:
pragma Precondition
pragma Inherited_Precondition
pragma Postcondition
pragma Inherited_Postcondition
These were discussed at some length at a meeting at AdaCore which
took place on 12/2/2008, with Tucker Taft of SofCheck as guest.
[This is version /01 of the AI - ED].
****************************************************************
From: Tucker Taft
Sent: Sunday, February 15, 2009 4:27 PM
I left out one important issue:
The names in the boolean_expression of a precondition
or postcondition pragma are resolved not at the point
of the pragma, but rather at the freezing point of the
named subprogram, or at the end of the immediately
enclosing visible part, whichever comes first.
and from the discussion:
We defer resolving the names in the boolean_expression
because it is natural for preconditions or postconditions
to refer to other subprograms declared in the same
scope, and requiring that there be no forward references
unduly restricts the expressions.
****************************************************************
From: Robert Dewar
Sent: Sunday, February 15, 2009 5:01 PM
I haven't studied the whole proposal carefully, but as far as I can
tell, the Precondition/Postcondition part of it corresponds pretty much
exactly to what has been implemented in GNAT, and used fairly extensively.
>> A resurrection of AI95-00375 on type invariants will appear shortly.
I look forward to that, we have always got stuck on invariants :-)
****************************************************************
From: Tucker Taft
Sent: Sunday, February 22, 2009 4:51 AM
I'll admit I have been bitten by the syntax bug (thanks, Randy!) for
pre- and postconditions, and with invariants coming up I suspect it will
continue. Here is a general proposal that avoids introducing new reserved words,
but is quite flexible:
To specify aspects of an entity (at least "operational" ones)
and link them directly to the associated declaration,
consider a general syntax of:
<declaration>
WITH
<aspect_name> [=> <aspect_value>],
<aspect_name> [=> <aspect_value>],
... ;
E.g.:
function Pop(S : in out Stack) return Elem
with
Pre => not Is_Empty(S),
Post => not Is_Full(S);
type Even is new Integer
with
Invariant => Even mod 2 = 0;
type Atomic_Array is
array(Positive range <>) of Natural
with
Atomic_Components;
type Set is interface
with
Invariant'Class =>
(Is_Empty(X)) = (Count(X) = 0);
function Union(X, Y : Set) return Set
is abstract with
Post'Class =>
Count(Union'Result) = Count(X) + Count(Y);
type R is record
X : Positive := 0
with Independent;
Y : Natural := 77
with Atomic;
end record;
type Shared_Bit_Vector is array(0..15) of Boolean
with Packing, Independent_Components;
type Bit_Vector is array(0..15) of Boolean
with Component_Size => 1;
[Find the rest of this message in AI05-0147-1.]
****************************************************************
From: Bob Duff
Sent: Tuesday, February 24, 2009 10:25 AM
> I'll admit I have been bitten by the syntax bug (thanks, Randy!) for
> pre- and postconditions, and with invariants coming up I suspect it
> will continue. Here is a general proposal that avoids introducing new
> reserved words, but is quite
> flexible:
>
> To specify aspects of an entity (at least "operational" ones)
> and link them directly to the associated declaration,
> consider a general syntax of:
>
> <declaration>
> WITH
> <aspect_name> [=> <aspect_value>],
> <aspect_name> [=> <aspect_value>],
> ... ;
I'm not 100% convinced we need syntax (maybe 90%?), but if we do, I definitely
like this proposal. Much nicer than adding a whole bunch of special-case
syntax for all the cases we need, along with the requisite reserved words.
> The notation <aspect_name>'Class was intended to imply an inherited,
> non-overridable aspect.
Seems a little bit odd, to me. I suppose I could get used to it, but I would
have said "Class_Invariant" rather than "Invariant'Class".
>...The 'Class
> might be implicit for abstract tagged types and their primitive
>subprograms.
Sounds confusing. Especially since abstract types can have concrete procedures.
Make the "'Class" or "Class_" explicit.
[Find the rest of this message in AI05-0147-1.]
****************************************************************
From: Robert Dewar
Sent: Thursday, February 26, 2009 12:09 AM
I agree with this, BTW, I find Tuck's syntax suggestion basically nice, and
think that pre/post conditions are important enough to warrant syntax additions.
[What he's agreeing to can be found in AI05-0146-1 - ED]
I do think that postconditions in the body are useful, and so would keep the
pragmas, certainly in GNAT anyway. It is true that preconditions in the body
are just assertions, so they are there just for symmetry, but postconditions
in the body are useful in that they come up front, which is the right position,
and they block all exits (which would be tedious to do manually with assertions).
I also think it is good to be able to control pre/post conditions separately
from normal assertions.
****************************************************************
From: Bob Duff
Sent: Thursday, February 26, 2009 7:34 AM
> postconditions in the body are useful in that they come up front,
> which is the right position, and they block all exits (which would be
> tedious to do manually with assertions).
It is true that it's useful. But it's a kludge. The general problem is that
there's nowhere to put some code that you want executed on every exit point.
This solves the problem for the case where that code happens to be an assertion.
But I'm not going to fight against pre/postconditions in bodies.
>... I also think it is good to be able to control pre/post conditions
>separately from normal assertions.
Yes. Precondition failures should be blamed an on the caller, postcondition
and invariant failures should be blamed on the callee. So if you have a
library, you might have confidence (from testing, and maybe from running
SofCheck's Inspector) that it works, so you want to turn off postcondition
and invariant checks, but keep precondition checks on.
****************************************************************
From: Robert Dewar
Sent: Friday, February 27, 2009 11:14 AM
...
> It is true that it's useful. But it's a kludge. The general problem
> is that there's nowhere to put some code that you want executed on every exit point.
> This solves the problem for the case where that code happens to be an
> assertion.
I would be happy to have the more general form. As you know the Ada compiler
internally has a construct AT END:
begin
...
at end
...
end;
which is essentially useful for translation of several constructs, and which would
be indeed be a useful programming construct (it would be amazingly easy to implement
this in GNAT :-))
> But I'm not going to fight against pre/postconditions in bodies.
>
>> ... I also think it is good to be able to control pre/post conditions
>> separately from normal assertions.
>
> Yes. Precondition failures should be blamed an on the caller,
> postcondition and invariant failures should be blamed on the callee.
> So if you have a library, you might have confidence (from testing, and
> maybe from running SofCheck's Inspector) that it works, so you want to
> turn off postcondition and invariant checks, but keep precondition checks on.
Right, and that might be independent of assertions (in the case of body postconditions).
Of course in GNAT you have the nice generalization of pragma Check, which allows you
to assign a name to an arbitrary group of assertions which can then be controlled as a
group.
****************************************************************
From: Arnaud Charlet
Sent: Friday, February 27, 2009 11:21 AM
> I would be happy to have the more general form. As you know the Ada
> compiler internally has a construct AT END:
>
> begin
> ...
> at end
> ...
> end;
>
> which is essentially useful for translation of several constructs, and
> which would be indeed be a useful programming construct (it would be
> amazingly easy to implement this in GNAT :-))
Indeed, and no new reserved word is even needed.
Delphi also has this capability BTW (and if I remember well, it's also
spelled "at end", or something very close).
****************************************************************
From: Bob Duff
Sent: Friday, February 27, 2009 12:17 AM
> Indeed, and no new reserved word is even needed.
This is another feature that was proposed as part of Ada 9X, and rejected
(primarily as a general size-of-change reduction, rather than objections
to the feature itself). It was thought that this feature isn't really needed,
because you can achieve the same thing via finalization, albeit rather verbosely.
I'm not particularly pushing for or against this feature...
> Delphi also has this capability BTW (and if I remember well, it's also
> spelled "at end", or something very close).
So does Java: try/finally, and misc other languages.
Java is an interesting case because finalization is so badly broken, so people
use try/finally fairly heavily.
****************************************************************
Questions? Ask the ACAA Technical Agent