!standard 13.3.2 (00) 10-10-18 AI05-0145-2/09 !class amendment 09-06-12 !status Amendment 2012 10-09-02 !status WG9 Approved 10-10-28 !status ARG Approved 11-0-0 10-02-28 !status work item 10-01-14 !status ARG Approved 11-0-1 09-11-07 !status work item 09-06-12 !status received 09-06-12 !priority Medium !difficulty Medium !subject Pre- and Postconditions !summary The basic assert pragma of Ada 2005 is augmented by the specification of pre/postconditions for subprograms and entries. !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 introduced in AI05-0183-1, 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 to be satisfied). Within a postcondition, Prefix'Old denotes the value of Prefix as it was at the beginning of the execution of the subprogram. Within a postcondition on a function F, F'Result denotes the value returned by the function. !wording Add a new section: 13.3.2 Preconditions and Postconditions For a subprogram or entry, the following language-defined aspects may be specified with an aspect_specification: Pre This aspect specifies a precondition for a callable entity; it shall be specified by an expression, called a *precondition expression*. Pre'Class This aspect specifies a precondition for a callable entity and its descendants; it shall be specified by an expression, called a *precondition expression*. Post This aspect specifies a postcondition for a callable entity; it shall be specified by an expression, called a *postcondition expression*. Post'Class This aspect specifies a postcondition for a callable entity and its descendants; it shall be specified by an expression, called a *postcondition expression*. Name Resolution Rules The expected type for a precondition or postcondition expression is any boolean type. 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 interpreted as having type T'Class. Similarly, a name that denotes a formal access parameter of type access-to-T is interpreted as having type access-to-T'Class. [Redundant: This ensures the expression is well-defined for a primitive subprogram of a type descended from T.] For an attribute_reference with attribute_designator Old, if the attribute reference has an expected type or shall resolve to a given type, the same applies to the prefix; otherwise the prefix shall be resolved independently of context. 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 expression also applies to the corresponding primitive subprogram of each descendant of T. For a prefix X that denotes an object of a nonlimited type, the following attribute is defined: X'Old Denotes the value of X at the beginning of the execution of the subprogram or entry. For each X'Old in a postcondition expression that is enabled, a constant is implicitly declared at the beginning of the subprogram or entry, of the type of X, initialized to X. The value of X'Old in the postcondition expression is the value of this constant. The type of X'Old is the type of X. These implicit declarations occur in an arbitrary order. Use of this attribute is allowed only within a postcondition expression. AARM annotation: The prefix X can be any nonlimited object that obeys the syntax for prefix. Useful cases are: the name of a formal parameter of mode '[in] out', the name of a global variable updated by the subprogram, a function call passing those as parameters, a subcomponent of those things, etc. A qualified expression can be used to make an arbitrary expression into a valid prefix, so T'(X + Y)'Old is legal, even though (X + Y)'Old is not. The value being saved here is the sum of X and Y (a function result is an object). Of course, in this case "+"(X, Y)'Old is also legal, but the qualified expression is arguably more readable. Note that F(X)'Old and F(X'Old) are not necessarily equal. The former calls F(X) and saves that value for later use during the postcondition. The latter saves the value of X, and during the postcondition, passes that saved value to F. In most cases, the former is what one wants. If X has controlled parts, adjustment and finalization are implied by the implicit constant declaration. If postconditions are disabled, we want the compiler to avoid any overhead associated with saving 'Old values. 'Old makes no sense for limited types, because its implementation involves copying. It might make semantic sense to allow build-in-place, but it's not worth the trouble. end AARM annotation. For a prefix F that denotes a function declaration, the following attribute is defined: F'Result Within a postcondition expression for function F, denotes the result object of the function. The type of this attribute is that of the function result except within a Post'Class postcondition expression for a function with a controlling result or with a controlling access result. For a controlling result, the type of the attribute is T'Class, where T is the function result type. For a controlling access result, the type of the attribute is an anonymous access type whose designated type is T'Class, where T is the designated type of the function result type. Use of this attribute is allowed only within a postcondition expression for F. 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 begins with the evaluation of the precondition expressions that apply to the subprogram or entry. If and only if all the precondition expressions evaluate to False, 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 evaluated. 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 a task or protected 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 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 other postcondition expressions are evaluated. 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.] 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. If the Assertion_Policy in effect at the point of a subprogram or entry declaration is Check, then preconditions and postconditions are considered to be *enabled* for that subprogram or entry. Bounded Errors It is a bounded error to invoke a potentially blocking operation (see 9.5.1) during the evaluation of a precondition or postcondition expression. If the bounded error is detected, Program_Error is raised. If not detected, execution proceeds normally, but if it is invoked within a protected action, it might result in deadlock or a (nested) protected action. NOTE: A precondition is checked just before the call. If another task can change any value that the precondition expression depends on, the precondition may not hold within the subprogram or entry body. !discussion This is based on the previous alternative AI05-0145-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; in the face of multiple pre/postcondition failures, it would be ambiguous which message to use, and furthermore, it was deemed that an implementation could provide automatically a message that indicated which pre/postcondition(s) failed, and that would be sufficient for debugging purposes. 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. !examples Pre and Post are most useful for untagged types, since Pre'Class and Post'Class are preferred for dispatching operations. Pre and Post can be used with concrete dispatching operations - they specify more about the particular implementation of an operation - but that information can only be useful with a non-dispatching call. Using Pre and Post for an untagged type could look like the following: 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; Pre'Class and Post'Class are the only things that make sense for abstract primitive operations, since there are no non-dispatching calls to them. For example: generic type Item is private; package Stack_Interfaces is type Stack is interface; procedure Push(S : in out Stack; I : in Item) is abstract with Pre'Class => not Is_Full(S), Post'Class => not Is_Empty(S); procedure Pop(S : in out Stack; I : out Item) is abstract with Pre'Class => not Is_Empty(S), Post'Class => not Is_Full(S); function Is_Empty(S : Stack) return Boolean is abstract; function Is_Full(S : Stack) return Boolean is abstract; end Stack_Interfaces; These would be inherited by types which have Stack as an ancestor: generic type Item is private; package Intf is new Stack_Interfaces (Item); package Bounded_Stacks is type Bounded_Stack (Capacity : Natural) is new Intf.Stack with private; procedure Push(S : in out Bounded_Stack; I : in Item); procedure Pop(S : in out Bounded_Stack; I : out Item); function Is_Empty(S : Bounded_Stack) return Boolean; function Is_Full(S : Bounded_Stack) return Boolean; end Bounded_Stacks; package Intf_Inst is new Stack_Interfaces (Natural); package Stk_Inst is new Bounded_Stacks (Natural, Intf_Inst); A call on Stk_Inst.Push would evaluate "not Is_Empty(S)" as its precondition expression (that being inherited from the interface). !corrigendum 13.3.2(0) @dinsc For a subprogram or entry, the following language-defined aspects may be specified with an @fa: @xhang<@xterm
  This aspect specifies a precondition for a callable entity; it shall
  be specified by an @fa, called a @i.>

@xhang<@xterm
  This aspect specifies a precondition for a callable entity and its
  descendants; it shall be specified by an @fa, called a
  @i.>

@xhang<@xterm
  This aspect specifies a postcondition for a callable entity; it shall
  be specified by an @fa, called a @i.>

@xhang<@xterm
  This aspect specifies a postcondition for a callable entity and its
  descendants; it shall be specified by an @fa, called a
  @i.>

@s8<@i>

The expected type for a precondition or postcondition expression is
any boolean type.

Within the expression for a Pre'Class or Post'Class aspect for a primitive
subprogram of a tagged type @i, a name that denotes a formal parameter of type
@i is interpreted as having type @i'Class. Similarly, a name that denotes a
formal access parameter of type access-to-@i is interpreted as having type
access-to-@i'Class. This ensures the expression is
well-defined for a primitive subprogram of a type descended from @i.

For an attribute_reference with attribute_designator Old, if the attribute
reference has an expected type or shall resolve to a given type, the same
applies to the @fa; otherwise the @fa shall be resolved independently
of context.

@s8<@i>

The Pre or Post aspect shall not be specified for an abstract
subprogram. Only the Pre'Class and Post'Class aspects may
be specified for such a subprogram.

@s8<@i>

If a Pre'Class or Post'Class aspect is specified for a primitive
subprogram of a tagged type @i, then the associated expression also
applies to the corresponding primitive subprogram of each descendant
of @i.

For a @fa X that denotes an object of a nonlimited type,
the following attribute is defined:

@xhang<@xterm
  Denotes the value of X at the beginning of the execution
  of the subprogram or entry. For each X'Old in a postcondition
  expression that is enabled, a constant is implicitly declared
  at the beginning of the subprogram or entry, of the type of X,
  initialized to X. The value of X'Old in the postcondition
  expression is the value of this constant. The type of X'Old
  is the type of X. These implicit
  declarations occur in an arbitrary order.>

@xindent

For a @fa F that denotes a function declaration, the following attribute is
defined:

@xhang<@xterm
   Within a postcondition expression for function F, denotes
   the result object of the function. The type of this attribute is that
   of the function result except within a Post'Class postcondition
   expression for a function with a controlling result or with a
   controlling access result. For a controlling result, the type of the
   attribute is @i'Class, where @i is the function result type. For a
   controlling access result, the type of the attribute is an anonymous
   access type whose designated type is @i'Class, where @i is the
   designated type of the function result type. Use of this attribute
   is allowed only within a postcondition expression for F.>

@s8<@i>

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 begins with the evaluation of
the precondition expressions that apply to the subprogram or entry. If
and only if all the precondition expressions evaluate to False,
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 evaluated. 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 a task or protected 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 @b or @b 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 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 other
postcondition expressions are evaluated. It is not specified whether any
constraint checks associated with copying back @b or @b
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. 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. 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.

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.
If the Assertion_Policy in effect at the point of a
subprogram or entry declaration is Check, then preconditions and
postconditions are considered to be @i for that subprogram or
entry.

@s8<@i>

It is a bounded error to invoke a potentially blocking operation (see
9.5.1) during the evaluation of a precondition or postcondition expression.
If the bounded error is detected, Program_Error is raised. If not detected,
execution proceeds normally, but if it is invoked within a protected action,
it might result in deadlock or a (nested) protected action.
  
@s9


!ACATS test

Various C-Tests should be created to test these features.

!appendix

From: Erhard Ploedereder
Sent: Saturday, November 7, 2009  11:42 AM

I still have 2 issues with AI-145-2.

I still am bothered about the race conditions on preconditions of protected
actions. Normally, I assume that I can use the "usual" Floyd style of
propagating the Pre across the code of the subprogram to determine what holds at
any given point.

Here, the Pre might have been checked ages ago, when I was blocked, and need no
longer hold when I am unblocked. The Floyd-style arguing about the code is not
valid any more. And I do not see how I can make it valid again, short of almost
unreasonable restrictions on the nature of Pre. See also the 2. issue. Local
state may be very  important. It is clear that references to shared global state
in Pre will introduce general data race conditions, but that is well known and
unavoidable short of drastic restrictions on Pre. I don't buy the argument that,
if we cannot prevent this general problem, it is not worth to solve the specific
problem.

There are various implementation models possible:
 a) check Pre as part of the call: has the above race condition and consequences
 b) check after the barrier check: does not "protect" the barrier check,
    but everything else. Satisfies Floyd.
 c) check before the barrier check and also as part of being unblocked:
    "protects" everything, satisfies Floyd, costs a bit more.

In a safe language, I would expect b) or c), certainly not a) as currently
proposed.

----

The other comment that I have is that the difference between subprograms
operating on any (other) composite data and protected operations is striking.
Just because "self" is not a parameter of the subprogram (but is for primitive
ops), direct access to the local state of protected objects is unavailable,
while access to local state of any other object is available in Pre. Such access
is necessary, if timed logic gets involved, e.g., "must have been initialized by
a call on xyz" presumably needs info from the local state to be an executable
Pre.

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

From: Bob Duff
Sent: Saturday, November 7, 2009  3:14 PM

...
> There are various implementation models possible:
>  a) check Pre as part of the call: has the above race condition and
> consequences
>  b) check after the barrier check: does not "protect" the barrier check,
>     but everything else. Satisfies Floyd.
>  c) check before the barrier check and also as part of being unblocked:
>     "protects" everything, satisfies Floyd, costs a bit more.
>
> In a safe language, I would expect b) or c), certainly not a) as
> currently proposed.

Yes, I see what you mean.

> ----
>
> The other comment that I have is that the difference between
> subprograms operating on any (other) composite data and protected
> operations is striking. Just because "self" is not a parameter of the
> subprogram (but is for primitive ops), direct access to the local
> state of protected objects is unavailable, while access to local state
> of any other object is available in Pre. Such access is necessary, if
> timed logic gets involved, e.g., "must have been initialized by a call
> on xyz" presumably needs info from the local state to be an executable Pre.

I don't think that's right.  The type has to be private, so Pre has to refer to
some accessor functions if it wants to depend on the innards.  So protected
types are no different, here, as far as I can see.

P.S. I'm sitting right next to you as I write this.  ;-)

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

From: Tucker Taft
Sent: Sunday, November 8, 2009  9:52 PM

I can sympathize with the desire of checking preconditions both before and after
any queuing, but if it makes a difference I believe that it is probably a "bad"
precondition.  How is the caller supposed to know if something *will be* true by
the time the entry body/accept statement finally gets executed?

From the entry body's point of view, any part of the conceptual Floyd-ish
precondition that depends on the state of the object should really be part of
the entry barrier. The only part of the precondition that should be enforced on
the caller is the part that they have control over, namely the value of their
parameters.

It would be helpful if you could give an example where a "good"
precondition can legitimately depend on the variable state of the protected
object.  That might be more convincing that appealing to Floyd here, since I
don't think he was talking about concurrent data structures.

As far as the specific issue of referening the local state, the
pre/postconditions can only reference visible entities (since they are on the
spec, and are supposed to be meaningful to the caller), but they could call
visible protected functions.  Again, though, if the protected function is
returning a value that could change between the time the call is made and the
entry body is executed, then it probably shouldn't be included in a
precondition, or else there is clearly a race condition.

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

From: Randy Brukardt
Sent: Monday, December 28, 2009  11:42 PM

...
> I still am bothered about the race conditions on preconditions of
> protected actions.
> Normally, I assume that I can use the "usual" Floyd style of
> propagating the Pre across the code of the subprogram to determine
> what holds at any given point.

I don't think this works in Ada, in the general case. Ada expressions can easily
depend on functions with side-effects, on functions that modify their parameters
(think "Random"), on global variables, on aliased objects that can be modified
by other tasks, constants that aren't really constant, and the like. About all
you can say for sure about an arbitrary precondition expression is that it was
true when it was checked (at the point of the call). You most certainly cannot
assume that it holds throughout the subprogram.

Note that this has nothing whatsoever to do with protected objects; it is a
"feature" of Ada expressions that becomes a "feature" of Assertions,
preconditions, invariants, and anything else that you like.

A fine example of that is the Claw "precondition" of object validity. For
instance, in the following (written using our new syntax rather than the textual
comments actually used in Claw):

    procedure Move (Window : in out Root_Window_Type; Position : in Point_Type)
          with Pre'Class => Is_Valid (Window);

The problem is that the user of the Claw application can close a window
asynchronously to the application code. So simply putting
    if Is_Valid (Window) then
       Move (Window, Top_Left);
    end if;
is insufficient to prevent Not_Valid_Error from happening. (Indeed, there is no
way to prevent it; handling the exception is the only alternative.) [Yes, the
state changes are synchronized to prevent dangerous race conditions related to
the actual state change; we tried to prevent higher level race conditions, but
that simply made responsiveness terrible and often caused deadlocks in typical
code.]

> Here, the Pre might have been checked ages ago, when I was blocked,
> and need no longer hold when I am unblocked. The Floyd-style arguing
> about the code is not valid any more. And I do not see how I can make
> it valid again, short of almost unreasonable restrictions on the
> nature of Pre.

The *only* way to be able to argue *anything* about Pre *anywhere* is to put
"almost unreasonable restrictions" on the nature of Pre. Pretty much the only
Pre that can be guaranteed to work is one that could have been used in a
function that has Global In/Global Out equal to null -- this is substantially
stronger than the restrictions of a Pure function. Anything else will be at risk
of becoming untrue because of something some other task does (even in the
supposedly protected code).

For instance, the problem with the Claw Is_Valid function is that other tasks
have access to part of the Window object, and thus can change the state of that
object. That problem will happen for any object that has a portion that is
potentially shared with another task (which, of course, includes the variable
parts of all protected objects).

One hopes that there will exist tools that detect and warn about "bad"
preconditions (and all of the other sorts of contracts that we're planning to
add). Without that, it will be very hard to reason about anything.

My primary point here is that your concerns about protected objects are just the
tip of the iceberg. If you write "good" preconditions, there won't be any
problem with using Floyd, but if the preconditions can change (and that is true
for many preconditions that might be written in a real program), they're
essentially meaningless. The blocking of the task at the barrier might make this
problem somewhat more visible, but it is hardly worth worrying about on its own.

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

From: Tucker Taft
Sent: Tuesday, December 29, 2009  8:38 AM

I essentially agree with Randy, as I wrote on 11/8/2009.
Let me know if I need to repost that message.

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

From: Bob Duff
Sent: Tuesday, December 29, 2009  11:03 AM

(How did you get to be such an egregious top-poster, Tuck?  ;-))

Tucker Taft wrote:

> I essentially agree with Randy, as I wrote on 11/8/2009.

I agree with Randy's conclusion, that the precondition should be checked before
an entry call (after locking the lock), and not at the beginning of the entry
body.  I suppose it should also be checked on a requeue, right? The caller has
to ensure that the precondition is true, and the caller can't be expected to
know what goes on between enqueueing the call and starting the body.

Yes, that could cause race conditions -- it's the responsibility of the
protected type to deal with it (e.g. don't write preconditions that can change
in that time).

But I don't entirely agree with Randy's reasoning -- Randy is overly
pessimistic, as is his wont ;-), when he says:

> The *only* way to be able to argue *anything* about Pre *anywhere* is
> to put "almost unreasonable restrictions" on the nature of Pre.

One can prove that:

    If there are no shared variables, then procedure P's precondition
    is True at the start of P.

(I'm assuming we have globals annotations.) A tool that knows that could be
extremely useful, so long as its users understand that they must analyze any
shared variables separately "by hand".

Alternatively, one could come up with annotations that allow the proof tool (the
compiler?) to know about shared variables. I should have suggested that before
the deadline for new ideas -- at least part of my brain understood the issue,
because such annotations exist in my hobby language. Too late -- but it could be
an impl-def pragma or something.

Another alternative (which I don't like) would be for the tool to do
whole-program analysis.  I don't like it because it's slow.  I also don't like
it because it's not modular:  I don't just want to prove that a procedure works
in this particular program; I want to prove that it works, period, even if other
parts of the program are modified.

P.S. Because you have to read the conversation backwards.
P.P.S. Why is top-posting evil?

;-)

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

From: Pascal Leroy
Sent: Tuesday, December 29, 2009  5:18 AM

> One hopes that there will exist tools that detect and warn about "bad"
> preconditions (and all of the other sorts of contracts that we're planning
> to add). Without that, it will be very hard to reason about anything.

I couldn't agree more: these contracts are either pure-ish and not terribly
useful, or full of dependencies on global/external state, and devilishly hard to
analyze.  This is exactly why I think that all this contract business is useless
at best and actively harmful at worst.

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

From: Tucker Taft
Sent: Tuesday, December 29, 2009  1:41 PM

...
> This is exactly why I think that all this
> contract business is useless at best and actively harmful at worst.

Yeah, but how do you really feel? ;-)

I'll admit I am curious why you have developed such negative feelings toward
"all this contract business." Is it based on bad experience, or on the potential
for trouble if preconditions are impure?

We certainly use "pragma Assert" heavily, to good effect, for the equivalent of
preconditions in our static analysis tool.  Usually there is also a comment such
as "--#pre XXX" or "-- Requires: XXX". In most cases these would translate
rather directly into "with Pre => XXX" which would seem to be a feature.  Where
does the "active harm" arise?

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

From: Bob Duff
Sent: Tuesday, December 29, 2009  2:12 PM

> I couldn't agree more: these contracts are either pure-ish and not
> terribly useful, or full of dependencies on global/external state, and
> devilishly hard to analyze.  This is exactly why I think that all this
> contract business is useless at best and actively harmful at worst.

I'm puzzled by that comment.  Why would anyone want to refer to lots of global
variables in a precondition?  I'd expect them to be mostly "pure-ish" and
"terribly useful".

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

From: Steve Baird
Sent: Wednesday, January 13, 2010  11:15 PM

The pragma-based version of the AI-145 included an intended implementation model
for the 'Old attribute. [That's AI-0145-1 - Editor.]

It was defined in terms of a wrapper which saves the needed values as local
constants, calls the "real" subprogram, and then uses the saved values as needed
in order to provide 'Old attribute values in postconditions.

It seems like we need to say something about the case where the parameter type
has controlled parts. We'd better get the right Adjust/Finalize calls, or
problems will result.

1) Do you agree that some action is needed to address this issue?

2) If so, then what?

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

From: Randy Brukardt
Sent: Thursday, January 14, 2010  1:20 AM

The current definitions of the attributes is just completely wrong, in that it
doesn't follow the style of the RM for defining attributes at all. E'Count is
similar to these (in that its use is highly restricted), and it manages to be
defined in the correct style (see 9.9(4-5)). Following that style is necessary
for them to show up in the automatically generated Annex K, which I think most
Ada programmers refer to frequently.

Moreover, I agree that there is no explanation of the *real* dynamic semantics
of these attributes. We did agree that copies of the parameter values are made
on entry to the call (using the normal Ada semantics), and that needs to be
explained. Moreover, we need to decide when that happens (Always? That's
expensive. Only when the attribute is used in a postcondition? That's yucky as
improving a postcondition could change the behavior of the program rather
dramatically [the copy of the parameter would prevent the original parameter
from being freed after a re-assignment, for instance].)

Anyway, this gives me a good excuse for not putting this AI into the current
standard draft, which is good because the associated syntax, resolution rules,
and freezing rules are in the unfinished AI-183. We shouldn’t have approved this
one anyway without.

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

From: Randy Brukardt
Sent: Thursday, January 14, 2010  1:55 AM

It seems to me that in extreme cases, the use of 'Old could invalidate the
entire Postcondition. So the semantics need to be nailed down.

For example, consider:

   package Ref_Count is
       type Ref_Counted_Type is new Controlled with private;

       function Count (Obj : Ref_Counted_Type) return Natural;
          -- Return the reference count for Obj.

       procedure Free (Obj : in out Ref_Counted_Type);
          -- Free this instance of Obj.

   private
       ... -- Define Initialize, Adjust, and Finalize as needed.
   end Ref_Count;


   procedure Do_It (Obj : in out Ref_Counted_Type; ...) with
      Post => (if  then (if Count(Obj'Old) = 1 then Count(Obj) = 0)
               else (Count(Obj'Old) = Count(Obj))) is
   begin
       if  then Free (Obj)
       else ...
       end if;
   end Do_It;

The problem is, the copy of Obj made to support the 'Old attribute will increase
the reference count, so the object will not be freed when the Postcondition is
executed: Count(Obj) could not be zero yet.

(Yes, I know this is a lousy Postcondition -- I said it was in extreme cases...)

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

From: Bob Duff
Sent: Wednesday, February 3, 2010  11:24 AM

Here's an Old message from Randy that nicely illustrates the issue with 'Old
that I mentioned at the last phone meeting. There seems to be an
assumption/requirement in ai05-0145-1 (the other variant of this AI) that 'Old
applies only to formal parameters. That makes no sense to me, and Randy's
message illustrates why.

[Bob repeats the previous message.]

It seems clear (to me) that you want "Count(Obj)'Old" above, instead of
"Count(Obj'Old)".  The semantics of "Count(Obj)'Old" are to evaluate
"Count(Obj)", and save that value. We are not saving the value of Obj in that
case, so Adjust or whatever is not called.

Of course, you are allowed to say "Count(Obj'Old)", and then you'd get a saved
copy of Obj -- with Adjust, Finalize, whatever.  So don't do that, if it's not
what you want.

My homework is to write up the wording for 'Old and 'Result.  To be included in
AI05-0145-2, right? My plan is that the prefix of 'Old can be any non-limited
object.

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

From: Bob Duff
Sent: Wednesday, February 3, 2010  2:33 PM

AI05-0145-2/03 Pre- and Postconditions

Here is my homework to write the !wording for the 'Old and 'Result attributes.

Add to the end of the !proposal:

Within a postcondition, Prefix'Old denotes the value of Prefix as it was at the
beginning of the execution of the subprogram.

Within a postcondition on a function F, F'Result denotes the value returned by
the function.


For reference, the current (version 03 of this AI) Name Resolution section under
!wording says:

  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 interpreted as having type T'Class. Similarly, a name that denotes a
  formal access parameter of type access-to-T is interpreted as having type
  access-to-T'Class. Finally, if the subprogram is a function returning T or
  access T, the Result attribute is interpreted as having type 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.]

Replace with:

  The expected type for a precondition or postcondition expression is
  the predefined type Boolean.

  For a prefix X that is of a nonlimited type,
  the following attribute is defined.
  This attribute is allowed only within a postcondition.

       X'Old    Denotes the value of X at the beginning of the execution
                of the subprogram or entry. In particular, if X'Old appears in
                a postcondition, and postconditions are enabled, a constant
                is implicitly declared at the beginning of the subprogram or
                entry, of the type of X, initialized to X. The value of X'Old
                in the postcondition is the value of this constant.
                These implicit declarations occur in an arbitrary order.

AARM annotation:

  The prefix X can be anything nonlimited that obeys the syntax for
  prefix. Useful cases are: the name of a formal parameter of mode
  '[in] out', the name of a global variable updated by the subprogram,
  a function call passing those as parameters, a subcomponent
  of those things, etc.

  A qualified expression can be used to make an arbitrary expression into a
  valid prefix, so T'(X + Y)'Old is legal, even though (X + Y)'Old
  is not. The value being saved here is the sum of X and Y.

  Note that F(X)'Old and F(X'Old) are not necessarily equal.
  The former calls F(X) and saves that value for later use during
  the postcondition. The latter saves the value of X,
  and during the postcondition, passes that saved value
  to F. In most cases, the former is what one wants.

  If X has controlled parts, adjustment and finalization are implied
  by the implicit constant declaration.

  If postconditions are disabled, we want the compiler to avoid any
  overhead associated with saving 'Old values.

  'Old makes no sense for limited types, because its implementation
  involves copying, in general. Well, it might make semantic sense to
  allow build-in-place, but it's not worth the trouble.

end AARM annotation.

  For a prefix F that denotes a function, the following attribute is
  defined. This attribute is allowed only within a postcondition for F.

       F'Result Denotes the result of the function.
                The type of this attribute is normally that of the function
                result. The only exception is that within Post'Class
                of a primitive function of type T, F'Result is of type
                T'Class.

  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 interpreted as having type T'Class. Similarly, a name that denotes a
  formal access parameter of type access-to-T is interpreted as having type
  access-to-T'Class. Finally, if the subprogram is a function returning T,
  the Result attribute is interpreted as having type T'Class.
  [Redundant: This ensures the expression is well-defined for a primitive
  subprogram of a type descended from T.]

[Note from Bob: The last para above used to talk about "access T"
for function results, but I don't see why, since those aren't primitive in T.
So I deleted that part.]

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

From: Randy Brukardt
Sent: Wednesday, February 3, 2010  2:47 PM

> [Note from Bob: The last para above used to talk about "access T"
> for function results, but I don't see why, since those aren't
> primitive in T.  So I deleted that part.]

Huh? They surely are primitive for T: see 3.2.3(6) (which says that the
primitives are the ones that "operate on the type") and 3.2.3(1/2) which defines
"operate on the type" to include access result types. So a function like:

    function Foobar (A : Natural) return access T;

is surely primitive on T. That's good, because such a function is
tag-indeterminate and can be dispatched on!

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

From: Bob Duff
Sent: Wednesday, February 3, 2010  5:13 PM

Right.  I somehow got stuck in Ada 95.

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

From: Robert Dewar
Sent: Wednesday, February 3, 2010  3:09 PM

> My plan is that the prefix of 'Old can be any non-limited object.

That's what we implement now, and I think that is the desirable choice.

In general it is always possible to write preconditions and postconditions with
unacceptable side effects. We don't prevent that, and the ability to be able to
do this is not a legitimate argument against a particular class of usage.

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

From: Gary Dismukes
Sent: Wednesday, February 3, 2010  3:53 PM

>   For a prefix F that denotes a function, the following attribute is
>   defined. This attribute is allowed only within a postcondition for F.
>
>        F'Result Denotes the result of the function.
>                 The type of this attribute is normally that of the function
>                 result. The only exception is that within Post'Class
>                 of a primitive function of type T, F'Result is of type
>                 T'Class.

I think the phrase "primitive function of type T" should be changed to something
like "primitive function of a tagged type T whose result is T", since the
primitive function might have some other result type.

>   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 interpreted as having type T'Class. Similarly, a name that denotes a
>   formal access parameter of type access-to-T is interpreted as having type
>   access-to-T'Class. Finally, if the subprogram is a function returning T,
>   the Result attribute is interpreted as having type T'Class.
>   [Redundant: This ensures the expression is well-defined for a primitive
>   subprogram of a type descended from T.]

The earlier paragraph says that F'Result *is* of type T'Class, whereas here
you're saying that it's interpreted as having type T'Class.  I think the former
is all that is needed, right?  Also, for consistency, should the earlier
description of X'Old include the stuff related to Pre'Class/Post'Class? (Of
course, that would make most of the above paragraph redundant.)

> [Note from Bob: The last para above used to talk about "access T"
> for function results, but I don't see why, since those aren't
> primitive in T.  So I deleted that part.]

But those *are* primitive for type T (as also noted by Randy).

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

From: Steve Baird
Sent: Wednesday, February 3, 2010  4:46 PM

> I think the phrase "primitive function of type T" should be changed to
> something like "primitive function of a tagged type T whose result is
> T", since the primitive function might have some other result type.

This seems like a good place to somehow use the terms "controlling result" and
"controlling access result".

Maybe

    F'Result Denotes the result of the function.
           The type of this attribute is that of the function result
           except within a Post'Class postcondition for a function
           with a controlling result or with a controlling access result.
           In the former case, the type of the attribute is T'Class,
           where T is the function result type. In the latter case,
           the type of the attribute is an anonymous access type whose
           designated type is T'Class, where T is the designated type
           of the function result type.

Do we need to define the accessibility level of this access type?
Do we need to say anything more to ensure that F'Result does not make a copy
(except in the elementary case)?

> The earlier paragraph says that F'Result *is* of type T'Class, whereas
> here you're saying that it's interpreted as having type T'Class.  I
> think the former is all that is needed, right?

I agree.

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

From: Randy Brukardt
Sent: Wednesday, February 3, 2010  10:48 PM

For the record, I made these changes and also put the attributes in the Static
Semantics section where they belong in the posted AI.

[I also reorganized the wording to be consistent with E'Caller,
the only other attribute that I could think of that is only
allowed in a single contexts.]

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

From: Steve Baird
Sent: Thursday, February 4, 2010  4:42 PM

>    F'Result Denotes the result of the function.
>           ... . In the latter case,
>           the type of the attribute is an anonymous access type whose
>           designated type is T'Class, where T is the designated type
>           of the function result type.
>
> Do we need to define the accessibility level of this access type?

There was a request for an example to illustrate whatever issue it was that I
had in mind when I asked this question.

Consider

     Type Root is tagged null record;

     type Ref is access constant Root'Class;

     function F (Ptr : Ref) return Boolean;

     procedure Enclosing is

         package Pkg is
             type T is new Root with ... ;
             function F (...) return access T
               with Post'Class => F (Ref (F'Result));
         end Pkg;
         ...
     begin ... end Enclosing;

We want to be sure that the right RM wording exists to support rejecting this
type conversion.

4.6(24.17/3) requires that in this case
    The accessibility level of the operand type shall not be
    statically deeper than that of the target type, ...

For this to make sense, the accessibility level of the operand type must be
defined.

I think this boils down to a question of whether 3.10/2(7/2) applies in this
case:

   An entity or view defined created by a declaration and created as part
   of its elaboration has the same accessibility level as the innermost
   enclosing master of the declaration except in the cases of renaming
   and derived access types described below.

I think we can decide that this rule does apply (don't spend too much time
pondering that "created as part of its elaboration" clause) and that  therefore
the type conversion in the example is illegal and no action is required.

Comments?

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

From: Randy Brukardt
Sent: Thursday, February 4, 2010  4:58 PM

...
> Comments?

The example would make a whole lot more sense if the two functions had different
names. I briefly thought you were trying to illustrate a recursive Post
expression.

Which does beg the question: is a self-recursive Post expression allowed? (I
suppose; the name of the function must not be hidden from all visibility or the
attribute 'Result could never work.) If so, I presume it will eventually raise
Storage_Error.

i.e.

       function F (Whatever : Natural) return Natural with
           Post => F (Whatever'Old) = F'Result;

Obviously this is a totally goofy postcondition, but it is also one that is true
and someone might write by being too clever for their own good. A warning would
be good, I guess.

P.S. If you don't see the problem, recall that the call of F in Post also has a
Postcondition, and that postcondition also calls F. The net effect is that the
evaluation of postconditions will never terminate until the task runs out of
stack space. That's irrespective of whatever the body of F does.

P.P.S. None of this really has anything to do with Steve's example, but it's the
sort of flight of fancy that us ARG members are known for. Gotta keep up the
status quo on that. :-)

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

From: Steve Baird
Sent: Thursday, February 4, 2010  5:10 PM

> The example would make a whole lot more sense if the two functions had
> different names. I briefly thought you were trying to illustrate a
> recursive Post expression.

Good point. I didn't mean to give them the same name.

[And recursive calls from within a post condition seem fine; the recursion might
even bottom out and accomplish something useful.]

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

From: Gary Dismukes
Sent: Thursday, February 4, 2010  5:48 PM

> ...
> I think this boils down to a question of whether 3.10/2(7/2) applies
> in this case:
>
>    An entity or view defined created by a declaration and created as part
>    of its elaboration has the same accessibility level as the innermost
>    enclosing master of the declaration except in the cases of renaming
>    and derived access types described below.
>
> I think we can decide that this rule does apply (don't spend too much
> time pondering that "created as part of its elaboration" clause) and
> that  therefore the type conversion in the example is illegal and no
> action is required.
>
> Comments?

Yes, I think that paragraph does apply.  So no further action needed, I'd say.

(At first I was thinking that the level had something to do with the point of
calls, but that was confused.  Accessibility is often that way...)

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

From: Florian Weimer
Sent: Saturday, September 25, 2010  2:41 PM

To me, the decision to use disjunction for multiple preconditions seems rather
strange.  I have never seen this approach before, and I expect that most
programmers will assume that the preconditions are "and"ed together.

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

From: Yannick Moy
Sent: Monday, September 27, 2010  4:46 AM

Note that you cannot define more than one precondition directly on a subprogram.
Thus, to have more than one condition here you must conjoin them:

procedure F with Pre => Cond_1 and then Cond_2 and then ...;

Hence, the case where you have multiple preconditions corresponds to inherited
preconditions on a primitive operation. Here, you must be careful that the
subprogram could be called as a result of a dispatching operation.

In order to respect the Liskov Subtitutability Principle (LSP), you would want
the precondition on the derived operation to be weaker than the precondition
on the inherited operation. This calls for or'ing the explicit precondition
on the derived operation with the ones it inherits.

But you may as well not want to enforce the LSP, in which case you don't want
such or'ing of preconditions, and you'd rather use only the direct precondition
on the derived operation.

To make a distinction between the 2 cases, you should use Pre'Class in the
first case and Pre in the second case. Robert Dewar has suggested this scheme
where you cannot change in a derived operation what kind of precondition you use
(whether Pre'Class or Pre) so that you either enforce LSP globally for a primitive
operation.

Here is a summary he sent to the ARG list on 2010/09/08:

> We keep the oring of inherited Pre'Class aspects, and if there is a 
> Pre'Class for the current subprogram it is also Or'ed in. [GNAT has a 
> nice exception message which shows all the preconditions that have 
> failed if the or fails.]
> 
> We do not allow the Pre aspect if there is an explicit Pre'Class or 
> any inherited Pre'Class. This avoids the confusion that happens with 
> Or'ing Pre'Class stuff where it is expected, and Pre stuff (where it 
> probably is not)
> 
> For Post, we have no restrictions, Post and Post'Class can both be 
> specified and just get and'ed with any inherited Post'Class aspects. 
> The idea is that no confusion arises in this case, and it is harmless 
> to pile up postconditions (and may well be useful).

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