!standard 6.1.1 (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). !comment AI05-0247-1 moves this to 6.1.1: !corrigendum 6.1.1(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.

!ASIS

Add the following values to the type Attribute_Kinds:
    An_Old_Attribute, A_Result_Attribute

** TBD: Aspect definitions. (Probably A_Pre_Aspect, A_Pre_Class_Aspect, A_Post_Aspect,
A_Post_Class_Aspect somewhere, use in new queries.)

!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: Robert Dewar
Sent: Wednesday, August 18, 2010  10:36 AM

I have implemented an approach where internally I allow multiple Pre and Post
aspects, splitting apart expressions in the single Pre/Post aspect allowed by
the syntax. This allows giving more accurate messages, as shown by the following
test:

>      1. with Text_IO; use Text_IO;
>      2. with Ada.Exceptions; use Ada.Exceptions;
>      3. procedure prepost is
>      4.    function F (X : Integer) return Integer with
>      5.    Pre  => X > 11
>      6.              and then
>      7.            X mod 2 = 1,
>      8.    Post => F'Result = X + 1
>      9.              and then
>     10.            F'Result /= 18;
>     11.
>     12.    function F (X : Integer) return Integer is
>     13.    begin
>     14.       if X = 13 then
>     15.          return X;
>     16.       else
>     17.          return X + 1;
>     18.       end if;
>     19.    end F;
>     20.
>     21.
>     22. begin
>     23.    Put_Line (F (31)'Img);
>     24.
>     25.    begin
>     26.       Put_Line (F (13)'Img);
>     27.    exception
>     28.       when E : others =>
>     29.          Put_Line ("exception raised for F (13): "
>     30.                    & Exception_Message (E));
>     31.    end;
>     32.
>     33.    begin
>     34.       Put_Line (F (12)'Img);
>     35.    exception
>     36.       when E : others =>
>     37.          Put_Line ("exception raised for F (12): "
>     38.                    & Exception_Message (E));
>     39.    end;
>     40.
>     41.    begin
>     42.       Put_Line (F (11)'Img);
>     43.    exception
>     44.       when E : others =>
>     45.          Put_Line ("exception raised for F (11): "
>     46.                    & Exception_Message (E));
>     47.    end;
>     48.
>     49.    begin
>     50.       Put_Line (F (17)'Img);
>     51.    exception
>     52.       when E : others =>
>     53.          Put_Line ("exception raised for F (17): "
>     54.                    & Exception_Message (E));
>     55.    end;
>     56. end prepost;

The output when this is run is:

>  32
> exception raised for F (13): failed postcondition from line 8
> exception raised for F (12): failed precondition from line 7 exception
> raised for F (11): failed precondition from line 5 exception raised
> for F (17): failed postcondition from line 10

So we can get the diagnostic clarity of separate Pre/Post aspects without
actually allowing them explicitly, and instead requiring the use of and then.

P.S. I have no idea what Randy is on about when he says that the ARG does not
like the idea of using Pre and Post conditions for debugging. To me that in
practice is the main use. Yes I know about input to formal tools etc, but in
practice being able to tell which pre or post condition has failed is quite
critical to their usability.

In the case of inherited post conditions, I will make sure we point to which
post condition failed.

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

From: Randy Brukardt
Sent: Wednesday, August 18, 2010  8:38 PM

...
> P.S. I have no idea what Randy is on about when he says that the ARG
> does not like the idea of using Pre and Post conditions for debugging.
> To me that in practice is the main use. Yes I know about input to
> formal tools etc, but in practice being able to tell which pre or post
> condition has failed is quite critical to their usability.

I may have done a lousy job of understanding the thinking; I didn't record much
about it in the minutes and my reconstruction may have been lacking. Whomever's
opinion it was (it wasn't mine I'm certain) clearly was compelling enough that
the entire ARG went along with that thinking.

I always hate it when I find myself defending an ARG decision that I don't have
a strong opinion on. But I do believe it is part of my job to explain the
reasoning as I understand it behind ARG decisions (whether or not I agree with
the decision); that's necessary to avoid ping-ponging between design choices by
considering only part of the concerns that have been previously discussed. So
I'll continue to do that, but I'll still probably butcher the intent from
time-to-time.

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

From: Robert Dewar
Sent: Wednesday, August 18, 2010  11:24 PM

> I may have done a lousy job of understanding the thinking; I didn't
> record much about it in the minutes and my reconstruction may have been lacking.
> Whomever's opinion it was (it wasn't mine I'm certain) clearly was
> compelling enough that the entire ARG went along with that thinking.

Since Randy won't take responsibility  for this viewpoint (fair enough if it is
not his :-)), can someone who does subscribe to this viewpoint explain their
position???

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

From: Tucker Taft
Sent: Sunday, August 22, 2010  2:29 PM

I don't remember the discussion.
Using pre/post-conditions for debugging
seems fine to me.

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

From: John Barnes
Sent: Sunday, August 22, 2010  3:26 PM

Indeed. Debugging is always a bugger and anything that helps is great.

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

From: Robert Dewar
Sent: Thursday, August 26, 2010  2:37 AM

An issue comes up with the 'Old attribute

GNAT has implemented this attribute for some time, and the definition in the AI
is incompatible. This is a problem since it makes it difficult or impossible for
us to implement the feature as described in the AI (since we don't want to
introduce unnecessary incompatibilities in the move to Ada 2012).

The issue is where to allow 'Old

In GNAT, 'Old can be used anywhere in a subprogram body, or in a Postcondition
or Precondition pragma that ends up in that subprogram body, for example, the
following is legal:

>      1. procedure p (x : in out integer) is
>      2.    procedure q (y : integer);
>      3.    pragma Precondition (y >= x'old);
>      4.
>      5.    procedure q (y : integer) is
>      6.    begin
>      7.       null;
>      8.    end;
>      9.
>     10. begin
>     11.    q (x);
>     12.    if x /= x'old then
>     13.       raise Program_Error;
>     14.    end if;
>     15. end;

Tuck feels that the usage should be restricted to Post aspect expressions.

First, for sure I think this should be allowed in assertion pragmas in the body.
For general use, you can always define constants at the point of the subprogram
entry (after all that is all the attribute does anyway), but that's not so good
for the assert case, where you don't want the constants defined if assertions
are disabled.

Second, if the restriction is retained, I think we should consider using some
name other than 'Old for the standard RM feature (perhaps Old_Value).

Incompatibilities make me very nervous, the incompatibilites in the Ada 2005
definition have very significantly delayed its adoption, and I don't want to see
small things delay adoption of Ada 2012. It's not technically an incompatibility
of course, but to define a new attribute with the same name as an attribute in
wide use in Ada 2005 implementations with different semantics is in practice an
incompatibility.

If this is not changed, GNAT is faced with two possibilities:

1. Ignore the restrictions in the RM, GNAT would still process all legal
   programs correctly, but would fail to diagnose some illegal programs.

2. Change the GNAT definition, which would create potential customer
   incompatibilities. Note that for sure we would still allow its use in
   precondition/postcondition macros, but I suppose that's marginally legal,
   since we have total freedom in defining the syntax/semantics of our own
   pragmas. It's uncomfortable for the expressions in those macros to have
   different rules than expressions anywhere else.

Probably we would choose approach 1, but it would end up being the one
non-conformance, which would be a pity. In practice it would be harmless since
there are unlikely to be any other Ada 2012 implementations around for a while.

It's possible we would choose approach 2, but the ugly business with odd rules
for precondition/postcondition pragmas are a problem, and I really see
forbidding it in pragma Assert statements as a real likely source of
incompatibilities in practice.

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

From: Tucker Taft
Sent: Thursday, August 26, 2010  8:08 AM

Actually, I have no problem allowing 'Old in pragma Assert, and certainly no
problem allowing it in implementation-defined pragmas.

I don't like 'Old in non-assertion code, as it creates hidden overhead without
obviously doing so, because a copy of the in-out parameter needs to be made
implicitly. When it is inside a pragma Assert/Postcondition, or whatever, it is
understood that such pragmas can be ignored in "production" mode.  Clearly if
'Old appears outside a pragma or Post aspect, it can't be ignored in production
mode.

Calling this an incompatibility is a bit of a stretch.  This is an
implementation-defined attribute in Ada 95 and Ada 2005.  In Ada 2012, we
happened to choose a name that an implementation is already using.  The more
common solution is for the implementation to adopt a new name, not for the
language to have to work around the existence of an implementation-defined
attribute. Clearly if 'Old becomes illegal outside pragmas or aspect clauses,
your customers will learn about it quickly and can presumably adapt to a new
name.

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

From: Robert Dewar
Sent: Thursday, August 26, 2010  8:27 AM

> Actually, I have no problem allowing 'Old in pragma Assert, and
> certainly no problem allowing it in implementation-defined pragmas.

That helps a bit, probably in practice the majority of now-illegal uses are in
assertions.

> I don't like 'Old in non-assertion
> code, as it creates hidden overhead without obviously doing so,
> because a copy of the in-out parameter needs to be made implicitly.

Doesn't seem very hidden to me (it is obvious that such a copy must be made to
use this feature).

And Ada is hardly a language where WYSIWYG when it comes to generated code (just
define a tagged type and list the -gnatG output with GNAT!!!)

I find this a very weak reason for "I don't like".
If you don't like the effect of using 'Old in more general contexts, don't use
it.

But if you really want to talk about X'Old, it is much clearer to say X'Old, and
much less verbiage than defining a constant without a fixed name and then using
that.

> Calling this an incompatibility is a bit of a stretch.

Not for a user of the compiler! As I say I know that technically it is not an
incompatibility, but in practice it IS an incompatibility for users of the
compiler (which is all that counts in real life).

> This is an implementation-defined
> attribute in Ada 95 and Ada 2005.  In Ada 2012, we happened to choose
> a name that an implementation is already using.

I think that it would be better to avoid using an existing attribute or pragma
that is in wide use if you intend to change the meaning.

> The more common solution is for the
> implementation to adopt a new name, not for the language to have to
> work around the existence of an implementation-defined attribute.

But if we change the name, that's an incompatibility as well.

> Clearly if 'Old becomes illegal outside pragmas or aspect clauses,
> your customers will learn about it quickly and can presumably adapt to
> a new name.

Software folks never seem to understand the predicament of application engineers
working with very large programs, that are under various stages of rigorous
configuration control.

If I decide to try out Ada 2012 and I get errors, I am uninclined to make the
fix, it is potentially maor work to find the poeple who are allowed to make the
changes to the affected units, do the necessary procedures for analyzing the
changes, rerun affected unit tests etc etc etc.

BTW the same goes for the very worrisome change in placement of user defined
equality. Yes, of course it is nearly always fixable by moving the declaration,
but again, the work of doing this move and verifying it is done right may be
really major.

New keywords like SOME are also problematical for the same reason.

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

From: Tucker Taft
Sent: Thursday, August 26, 2010  8:38 AM

By the way, as of July 13, 2010 you can get Ada 2005 from IBM Rational as well,
for what that's worth:

    Apex 4.4.6 (Apex with Ada05) is available for download
    ...
    Size 608mb
    Date posted 13-Jul-2010

So I guess now there are two Ada 2005 compilers!
Just in time for Ada 2012...

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

From: Robert Dewar
Sent: Thursday, August 26, 2010  8:55 AM

Right, that's why in my message I said "in wide use", if I had written this
before July, I would have said "in all available Ada 2005 compilers" :-) :-)

Anyway, it is great that Rational has released their Ada 2005 compiler, does
anyone have information on how complete the implementation is?

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

From: Steve Baird
Sent: Saturday, August 28, 2010  12:24 AM

Some additional (minor) points about this AI to consider:

1) It appears that we allow pre and post conditions to be specified for a
   non-abstract primitive subprogram of an interface type (which must be a null
   procedure). It seems clear to me that this should be disallowed. Certainly
   8.3(12.3/2) assumes that null procedures with a given profile are pretty much
   interchangeable and needs some changes if this is not the case.


2) The AI currently contains the following wording:

   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.

   I think this should be a permission; perhaps something like
   "a constant may be implicitly declared".

   Consider the following Post-Condition:

       True or else Function_Call_With_Side_Effects'Old

   There are other ways that X'Old can be dead, but it is
   essentially the same problem:

      Post_Condition => Some_Vector = Vector'(1.. 0 => X'Old)

   The point is that an implementation should not have to check
   a dead expression for uses of the Old attribute before
   eliminating it. Nobody cares about performance in these
   oddball cases - the issue is the unnecessary addition of
   implementation complexity. There are similar issues if the
   prefix of a 'Old attribute is a constant, or a function with
   side-effects but a statically known result, or ...

3)

Tucker Taft wrote:
 > Actually, I have no problem allowing 'Old
 > in pragma Assert, and certainly no problem
 > allowing it in implementation-defined pragmas.

I think we would want
    pragma Assert (X = T'()'Old);
to evaluate the attribute prefix upon entering the enclosing subprogram. This
doesn't work if  references declarations which don't exist at that
point. It also doesn't work if the pragma doesn't occur within a subprogram. Not
fundamental problems, but wording would be needed.

Otherwise, what is the following supposed to mean:

     procedure Foo is
         X : Integer := 1;
     begin
         for I in 1 .. 10 loop
            pragma Assert (X >= X'Old);
            ...

?

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

From: Robert Dewar
Sent: Saturday, August 28, 2010  5:53 AM

> I think we would want
>     pragma Assert (X = T'()'Old); to evaluate the
> attribute prefix upon entering the enclosing subprogram. This doesn't
> work if  references declarations which don't exist at that
> point.

That's a point indeed. In GNAT the rule is that 'Old can only reference
parameters and global variables, it cannot reference local variables:

>      1. procedure t (a : integer) is
>      2.    x : integer;
>      3.    y : integer := a + a;
>      4.    pragma Assert (a /= y'old);
>                                |
>         >>> attribute "old" cannot refer to local variable "y"
>
>      5. begin
>      6.    null;
>      7. end;

The actual definition in GNAT currently is:

> The attribute Prefix'Old can be used within a subprogram body or
> within a precondition or postcondition pragma. The effect is to refer
> to the value of the prefix on entry. So for example if you have an
> argument of a record type X called Arg1, you can refer to
> Arg1.Field'Old which yields the value of Arg1.Field on entry. The
> implementation simply involves generating an object declaration which
> captures the value on entry. Any prefix is allowed except one of a
> limited type (since limited types cannot be copied to capture their
> values) or an expression which references a local variable (since
> local variables do not exist at subprogram entry time).


> It also doesn't work if the pragma doesn't occur within a subprogram.

Right, I certainly don't propose that

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

From: Bob Duff
Sent: Saturday, August 28, 2010  7:40 AM

> 1) It appears that we allow pre and post conditions to be specified
> for a non-abstract primitive subprogram of an interface type (which
> must be a null procedure).
> It seems clear to me that this should be disallowed.
> Certainly 8.3(12.3/2) assumes that null procedures with a given
> profile are pretty much interchangeable and needs some changes if this
> is not the case.

I don't see the problem.  The pre/post conditions should be or'ed or and'ed as usual, then the null procedure does nothing.  It might even be useful, once in a blue moon.

> 2) The AI currently contains the following wording:
>
>    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.
>
>    I think this should be a permission; perhaps something like
>    "a constant may be implicitly declared".

I agree, but I think it might be easier to understand if we keep the current
wording, then add a permission to omit that object if it's not needed.  Similar
to the way we allow omission of Finalize calls.

>    Consider the following Post-Condition:
>
>        True or else Function_Call_With_Side_Effects'Old
>
>    There are other ways that X'Old can be dead, but it is
>    essentially the same problem:
>
>       Post_Condition => Some_Vector = Vector'(1.. 0 => X'Old)
>
>    The point is that an implementation should not have to check
>    a dead expression for uses of the Old attribute before
>    eliminating it. Nobody cares about performance in these
>    oddball cases - the issue is the unnecessary addition of
>    implementation complexity. There are similar issues if the
>    prefix of a 'Old attribute is a constant, or a function with
>    side-effects but a statically known result, or ...

Const'Old seems fishy -- maybe deserves a warning.

> 3)
>
> Tucker Taft wrote:
>  > Actually, I have no problem allowing 'Old  > in pragma Assert, and
> certainly no problem  > allowing it in implementation-defined  >
> pragmas.
>
> I think we would want
>     pragma Assert (X = T'()'Old); to evaluate the
> attribute prefix upon entering the enclosing subprogram. This doesn't
> work if  references declarations which don't exist at that
> point.
> It also doesn't work if the pragma doesn't occur within a subprogram.
> Not fundamental problems, but wording would be needed.

Right, we would need wording to disallow references to locals.

> Otherwise, what is the following supposed to mean:
>
>      procedure Foo is
>          X : Integer := 1;
>      begin
>          for I in 1 .. 10 loop
>             pragma Assert (X >= X'Old);
>             ...
>
> ?

Should be illegal.  It certainly should NOT mean "the value of X from last time
around the loop"!

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

From: Tucker Taft
Sent: Saturday, August 28, 2010  8:36 AM

> 1) It appears that we allow pre and post conditions to be specified
> for a non-abstract primitive subprogram of an interface type (which
> must be a null procedure).
> It seems clear to me that this should be disallowed.
> Certainly 8.3(12.3/2) assumes that null procedures with a given
> profile are pretty much interchangeable and needs some changes if this
> is not the case.

I'm not convinced of this.  I think it is easy enough to combine the
pre/post-conditions in an appropriate way when inherited, so that we don't need
to make this restriction.  Putting Post'Class on a null procedure of an
interface makes some sense, if you want to specify, say:

    Post'Class => Global = Global'Old

to ensure that some overriding of the null procedure doesn't have some
undesirable effect.

...
> Otherwise, what is the following supposed to mean:
>
>     procedure Foo is
>         X : Integer := 1;
>     begin
>         for I in 1 .. 10 loop
>            pragma Assert (X >= X'Old);
>            ...
>
> ?

Agreed, anything referenced in a blah'Old would have to be based on a parameter
or be global to the subprogram.  Basically, it would have to be well-defined at
the point of the "is" of the enclosing subprogram body.

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

From: Steve Baird
Sent: Saturday, August 28, 2010  12:31 PM

> Actually, I have no problem allowing 'Old in pragma Assert, and
> certainly no problem allowing it in implementation-defined pragmas.

References to the 'Old attribute of a parameter should probably be disallowed
from within a separate subunit, as in

    procedure Foo (X : in out T) is

        ....
        ... Bar ... is separate;
     begin ... end Foo;


    separate (Foo)
    ... Bar ... is
        pragma Assert (Some_Predicate (X'Old));
        ...
    end Bar;

If an implementation generates code for the parent before seeing the separate
subunit body (as some implementations do), then implementing this case without
distributed overhead would be difficult.

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

From: Bob Duff
Sent: Saturday, August 28, 2010  1:03 PM

> References to the 'Old attribute of a parameter should probably be
> disallowed from within a separate subunit, as in

It's only a problem in package subunits, right?

It seems bad to disallow something in subunits that is allowed for a
non-separate, because you might want to switch back and forth. That would argue
for making it illegal immediately within a package body.

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

From: Tucker Taft
Sent: Saturday, August 28, 2010  1:40 PM

Interesting issue.
I agree, I guess.

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

From: Robert Dewar
Sent: Saturday, August 28, 2010  1:49 PM

Interesting indeed, a very obscure case, but GNAT does indeed allow this, and of
course we don't want a stupid thing like this to cause implementation
difficulties in implementations with different models (and more importantly I
think Rational has this different model??)

I really dislike this special rule though, and Bob points out that it really has
to be extended to any package body, not just subunits, for consistency. So we
lose the nice simple rule anyway.

HMMMM ....

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

From: Tucker Taft
Sent: Saturday, August 28, 2010  2:30 PM

I don't understand the issue with package bodies.
Can you explain further?

Now that I think more about Steve's example, I believe it should not actually be
a problem, presuming expr'Old refers to the value of the expr at the entry to
the immediately enclosing body, which should be required to be a subprogram or
entry body.  Hence in his example, X'Old refers to the value of X on entry to
the nested subprogram.

Doesn't that eliminate all subunit problems?

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

From: Robert Dewar
Sent: Saturday, August 28, 2010  2:46 PM

> I don't understand the issue with package bodies.

It seems undesirable to ahve a situation where you can have a ppackage body
within a subprogram, but you can't make it into a subunit, are there any other
cases of such a restriction?

> Can you explain further?
>
> Now that I think more about Steve's example, I believe it should not
> actually be a problem, presuming expr'Old refers to the value of the
> expr at the entry to the immediately enclosing body, which should be
> required to be a subprogram or entry body.  Hence in his example,
> X'Old refers to the value of X on entry to the nested subprogram.
>
> Doesn't that eliminate all subunit problems?

We are talking about a nested package, consider this example:

procedure t (a : integer) is
    x : integer;
    y : integer := a + a;
    package r is end;
    package body r is separate;
begin
    null;
end;

separate (t)
package body r is
    pragma assert (a'old < 13);
end r;

GNAT allows this, rational would find it very hard to implement (the compile the
package body truly separately, and we don't want a rule that makes this hard to
do!)

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

From: Bob Duff
Sent: Saturday, August 28, 2010  3:30 PM

> I don't understand the issue with package bodies.
> Can you explain further?

I think maybe my e-mails to arg are getting stuck in the usual trap.  They'll
get through eventually, perhaps with some prodding from Randy.

Anyway, my point is that if you have a physically nested package (or other
thing), you might want to turn it into a subunit, or into a child unit.  Or vice
versa.  The language should guarantee that that always works.  It doesn't quite,
but it almost does, so let's not make it worse.

In this case, that implies that if we want to forbid 'Old in a package body
subunit (of a subprogram), then we should also forbid 'Old in a non-separate
package body within a subprogram.

> Now that I think more about Steve's example, I believe it should not
> actually be a problem, presuming expr'Old refers to the value of the
> expr at the entry to the immediately enclosing body, which should be
> required to be a subprogram or entry body.

Yes, that's exactly the right rule.

>...Hence in his example,
> X'Old refers to the value of X on entry to the nested  subprogram.

I thought we were talking about subprograms that have package (or task?)
subunits.  Your rule above solves Steve's problem.

If, on the other hand, you have a procedure with a procedure subunit, then of
course a 'Old in the inner one refers to the state upon entry to the inner one
-- that was never in question.

> Doesn't that eliminate all subunit problems?

Yes.

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

From: Bob Duff
Sent: Saturday, August 28, 2010  3:54 PM

> It seems undesirable to ahve a situation where you can have a ppackage
> body within a subprogram, but you can't make it into a subunit, are
> there any other cases of such a restriction?

Yes.  One example is:

    procedure P is
        procedure Q is
            ...
            package body R is separate; -- Illegal, but
            -- putting the package body here would be OK.

But that's pretty rare!

Maybe that case doesn't count -- if you say "procedure Q is separate"
it works.  And I can't think of any other cases where replacing a proper body
with a subunit doesn't work.

Ideally, it would always be possible to switch back and forth between separate
compilation and non-separate compilation of packages (whether for subunits or
library units).

Going the other direction (subunit to physically nested unit), there's a
different obscure problem -- with/use clauses on the subunit need to be moved to
the top of the parent unit, and that can cause illegality.

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

From: Steve Baird
Sent: Saturday, August 28, 2010  6:52 PM

> I'm not convinced of this.  I think it is easy enough to combine the
> pre/post-conditions in an appropriate way when inherited, so that we
> don't need to make this restriction.  Putting Post'Class on a null
> procedure of an interface makes some sense, if you want to specify,
> say:
>
>    Post'Class => Global = Global'Old
>
> to ensure that some overriding of the null procedure doesn't have some
> undesirable effect.
>

I think you misunderstood me (possibly because I was unclear).
I was talking about the Pre and Post aspects, not the Pre'Class and Post'Class
aspects.

With regard to the Pre'Class and Post'Class aspects, I agree with you about how
we want the language to work. We may need to look carefully at the wording to
verify that this case is handled correctly.

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

From: Randy Brukardt
Sent: Sunday, August 29, 2010  7:09 PM

> Actually, I have no problem allowing 'Old in pragma Assert, and
> certainly no problem allowing it in implementation-defined pragmas.

Well, I do have a problem with allowing it in language-defined stuff that is not
in the subprogram header. (Obviously, I don't care about implementation-defined
pragmas.)

Janus/Ada is essentially a one-pass compiler so far as semantics is concerned.
'Old requires code to be generated at the "is" of the subprogram. If 'Old is
allowed outside of the subprogram header (that is, in the aspect clause), we
would have no way to know whether any code is needed. Typically, such cases are
handled by adding thunks, which would mean this feature would have a distributed
overhead (every subprogram would need a thunk call at the top since there would
be no way to know ahead of time whether 'Old appears in an Assert pragma at some
later point).

The net effect is that a general 'Old would add a significant expense to every
subprogram call in Janus/Ada. Which is simply unacceptable; I doubt that I would
implement it if that is the case.


A second point is that I object to making the contents of pragma Asserts
different in some material way than regular code. I personally never use pragma
Assert as it does not have enough control over when it is or is not executed. My
experience (in our projects, YMMV) is that a dynamic method of controlling this
sort of code is needed. That necessary if the check is expensive enough to be a
significant drag on performance (if it is cheap, it should always be done so
there is no need to be able to turn it off -- many of the worst bugs in our
compiler have come where cheap checks were eliminated for a false efficiency).

The self-checks in our code usually look something like:

    if Trace_Manager() and then (not ) then
        Internal_Error ();
    end if;

Trace_Manager is usually a function controlled from a run-time menu; but if
minimum-sized code is needed, the function is replaced by a constant aggregate
with all values False. Then dead code elimination removes all of the code
overhead of the checks.

I would find it very annoying if this technique could not be used to replace an
existing pragma Assert, or that you would be forced to use pragma Assert instead
of writing some more effective code. That argues for either the restriction in
the AI, or allow using anywhere in the subprogram body (but of course that runs
afoul of my first concern).

(I still believe that dynamic pragmas like pragma Assert are an abuse of the
intent of the language [one that the Ada 95 team made part of the language], and
I am automatically against anything that would require expanding their use.)


If we are going to make any substantive changes to this attribute, I ask that we
reopen the AI so that all of the issues (and Steve had some as well) can be
properly discussed. (And I'd like to know if we're going to do that ASAP,
because this AI is the last thing I need to add to the AARM before starting the
review; if we're reopening it, I can start the review right away).

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

From: Tucker Taft
Sent: Sunday, August 29, 2010  8:16 PM

GNAT already has a pragma Check, I believe, which is roughly equivalent to
Assert but has a bit more flexibility.  Perhaps we should simply suggest that
GNAT limit the use of 'Old to their implementation-defined pragmas, such as
Check and Postcondition, and then other implementors don't need to worry about
it.

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

From: Robert Dewar
Sent: Sunday, August 29, 2010  9:54 PM

I would be inclined to continue to recognize 'Old in Assert pragmas in GNAT,
otherwise I think we would be introducing an unacceptable incompatibility and it
really does not matter if GNAT fails to diagnose the "error" of using 'Old in an
assert pragma (there are zillions of ways in GNAT of introducing non-portability
using the large number of implementation defined pragmas and attributes so one
more is no big deal).

I find the argument that Randy has trouble implementing it in his compiler weak.
The implementation model he has chosen is inappropriate and very limiting. In
any case here you only get the distributed overhead if assertions are enabled,
so that's not too bad.

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

From: Robert Dewar
Sent: Sunday, August 29, 2010  9:59 PM

BTW, I think it is no big deal if Randy's compiler fails to allow 'Old in assert
pragmas. Also I find Randy's attitude to pragma assert plain bizarre (this
pragma is VERY widely and heavily used throughout the GNAT sources, and many of
our customers use it widely).

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

From: Steve Baird
Sent: Monday, August 30, 2010  2:50 AM

More thoughts to consider.

   1) If a "Old attribute occurs within the prefix of another, as in

          F (G (X)'Old)'Old

      this requires that the implicitly declared constant for the
      inner 'Old must precede that for the outer but the AI says
         "These implicit declarations occur in an arbitrary order".

      Perhaps all that is needed here is an AARM "to be honest"
      note saying that the order isn't really 100% arbitrary.
      Or perhaps this is such an angels-on-the-head-of-a-pin
      issue that we can just ignore it.

      Incidentally, I think that X'Old'Old is legal. I don't see
      that this situation is any different then the example above -
      the initial value for one implicitly declared constant
      includes a reference to another such constant.

  2) I think we want to disallow at least some allocators within
     the prefix of a 'Old attribute in order to avoid having to
     talk about these implicit constant declarations in the
     definitions of "master" and/or "accessibility level"

     If this example
         function F (X : access Some_Task_Type) return Boolean is .... ;

         procedure Foo is
         begin
              ...;
              pragma Assert (F (new Some_Task_Type)'Old);

     were allowed, then I think extra wording would be needed in
     order to ensure that this was equivalent to

          procedure Foo
              Temp : constant Boolean := F (new Some_Task_Type);
          begin
               ...;
               pragma Assert (Temp);

    And who really wants to work out the consequences (either for the
    RM or for their favorite compiler) of allowing
    a 'Old prefix to include the creation of a coextension? Anyone
    who didn't take two steps backward just volunteered.

3)

Tucker Taft writes:
 > Actually, I have no problem allowing 'Old in pragma Assert,
 > and certainly no problem allowing it in
 > implementation-defined pragmas.

It seems a bit odd that transforming

       begin
          -- identifiers P1 and P2 occur nowhere in this block
          1;
          2;
          3;
          4;
       end;

     into

        declare
            procedure P1 is
            begin
                1;
                2;
            end P1;
            procedure P2 is
            begin
                3;
                4;
            end P2;
       begin
           P1;
           P2;
       end;

would no longer be semantics-preserving (e.g. if 3 contains
Some_Expression'Old). Tools that implement this sort of refactoring would have
to be aware of this issue. Users who wrap subprograms around large blocks of
code may be unpleasantly surprised. This is not a fundamental objection - just
an observation. [and yes, I know that the above transformation wasn't always
semantics-preserving in Ada05 even if both versions compiled successfully, but
those cases were pretty pathological - the one I'm thinking of involves the
Address attribute of a label].

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

From: Robert Dewar
Sent: Monday, August 30, 2010  5:01 AM

...
>       Incidentally, I think that X'Old'Old is legal. I don't see
>       that this situation is any different then the example above -
>       the initial value for one implicitly declared constant
>       includes a reference to another such constant.

This is definitely angels on a pin!
'Old'Old is stupid, never useful, never worth bothering about IMO

...
>     And who really wants to work out the consequences (either for the
>     RM or for their favorite compiler) of allowing
>     a 'Old prefix to include the creation of a coextension? Anyone
>     who didn't take two steps backward just volunteered.

Yes, just outlaw allocators alltogether if it makes someone more confident,
whether the compiler will bother with this check when there are lots more
important things to do??? :-) :-)

...
> would no longer be semantics-preserving (e.g. if 3 contains
> Some_Expression'Old). Tools that implement this sort of refactoring
> would have to be aware of this issue. Users who wrap subprograms
> around large blocks of code may be unpleasantly surprised. This is not
> a fundamental objection - just an observation. [and yes, I know that
> the above transformation wasn't always semantics-preserving in Ada05
> even if both versions compiled successfully, but those cases were
> pretty pathological - the one I'm thinking of involves the Address
> attribute of a label].

This is worrying too much, there are LOTS of cases where such refactoring does
not work, e.g. return statements and requeue statements! not to mention goto
statements :-)

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

From: Robert Dewar
Sent: Monday, August 30, 2010  5:03 AM

One thing one could say is that if the prefix of 'Old involves ANY side effects
of ANY kind, then the effect is implementation dependent (this takes care of the
business of not generating the copy if the compiler can tell that the 'Old is
not needed.

In practice, for me 100% of the uses of 'Old are simple variable references, and
I would not mind this restriction!

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

From: Bob Duff
Sent: Monday, August 30, 2010  6:01 AM

> One thing one could say is that if the prefix of 'Old involves ANY
> side effects of ANY kind, then the effect is implementation dependent
> (this takes care of the business of not generating the copy if the
> compiler can tell that the 'Old is not needed.

OK with me, I suppose, but this might lead to an endless discuss about what
constitutes "side effect".

> In practice, for me 100% of the uses of 'Old are simple variable
> references, and I would not mind this restriction!

We had this discussion (on ada-comment@, I think).  I am strongly opposed to
such an onerous restriction.  I certainly want to allow function calls.

But I'd be happy to forbid alligators (in the 'Old -- we're not going to forbid
allocators in functions called).

By the way, why don't we fix the syntax to allow:

    (X + Y)'Old

I mean, for all attributes.  It's really stupid that that's not allowed, but
these:

    "+"(X, Y)'Old
    My_Integer'(X + Y)'Old

are allowed.

(Let's see if this e-mail gets through without Randy doing some magic by hand.)

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

From: Bob Duff
Sent: Monday, August 30, 2010  5:07 AM

>       Incidentally, I think that X'Old'Old is legal.

X'Old'Old = X'Old, right?

>     And who really wants to work out the consequences (either for the
>     RM or for their favorite compiler) of allowing
>     a 'Old prefix to include the creation of a coextension? Anyone
>     who didn't take two steps backward just volunteered.

Consider me back-stepped.

> It seems a bit odd that transforming
>
>        begin
>           -- identifiers P1 and P2 occur nowhere in this block
>           1;
>           2;
>           3;
>           4;
>        end;
>
>      into
>
>         declare
>             procedure P1 is
>             begin
>                 1;
>                 2;
>             end P1;
>             procedure P2 is
>             begin
>                 3;
>                 4;
>             end P2;
>        begin
>            P1;
>            P2;
>        end;
>
> would no longer be semantics-preserving (e.g. if 3 contains
> Some_Expression'Old).

This doesn't seem SO bad.

What about finalization?  Moving things into a nested procedure can make them
finalize early.

What if P1 is "if Blah then return; end if;"?

Seems like there are various ways in which the above transformation doesn't
quite work, so one more isn't a disaster.

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

From: Tucker Taft
Sent: Monday, August 30, 2010  12:16 PM

I've come around to thinking that 'Old should only be defined as usable in Post
and Post'Class aspects, and let implementors support it if they want in their
own implementation-defined pragmas inside bodies (and/or cheat and support it in
standard pragmas as well).  I don't think we should waste verbiage in the
standard trying to define what 'Old means in an arbitrary Assert pragma.

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

From: Steve Baird
Sent: Monday, August 30, 2010  2:39 PM

>>       Incidentally, I think that X'Old'Old is legal.
>
> X'Old'Old = X'Old, right?

Typically, yes.

If controlled types are involved, this wouldn't strictly have to be true,

> What if P1 is "if Blah then return; end if;"?
>
> Seems like there are various ways in which the above transformation
> doesn't quite work, so one more isn't a disaster.

Agreed.

Incidentally, I think that my fears about accessibility/master complications for
allocators may extend to other object-creating constructs (at least aggregates;
I'm not sure about function calls).

Is there any need for a more detailed exploration of this?

When we have rules based on the enclosing whatever and then we invent an
attribute which introduces an implicit declaration which is supposed to behave
as though it syntactically encloses the attribute prefix, it does not seem
surprising that we would have to describe this interaction in the rules
somewhere.

I'd prefer to see some clean, simple restrictions (perhaps on the form of the
expressions, perhaps on their placement) which would spare us from dealing with
this stuff.

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

From: Robert Dewar
Sent: Monday, August 30, 2010  5:53 PM

> I've come around to thinking that 'Old should only be defined as
> usable in Post and Post'Class aspects, and let implementors support it
> if they want in their own implementation-defined pragmas inside bodies
> (and/or cheat and support it in standard pragmas as well).  I don't
> think we should waste verbiage in the standard trying to define what
> 'Old means in an arbitrary Assert pragma.

At this stage, that sounds reasonable to me! Although I would be happier if the
name did not clash with the incompatible GNAT implementation, but perhaps 'Old
is the only good name in the world? :-)

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

From: Robert Dewar
Sent: Monday, August 30, 2010  5:54 PM

> We had this discussion (on ada-comment@, I think).  I am strongly
> opposed to such an onerous restriction.  I certainly want to allow
> function calls.

Hard to imagine a situation where F(X'Old) is not an OK substitute for F(X)'Old.
I really dislike calling functions with side effects in a situation like this.

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

From: Randy Brukardt
Sent: Tuesday, August 31, 2010  12:07 AM

...
> Incidentally, I think that my fears about accessibility/master
> complications for allocators may extend to other object-creating
> constructs (at least aggregates; I'm not sure about function calls).
>
> Is there any need for a more detailed exploration of this?

I'm afraid so. We spent a lot of effort in Ada 2005 dealing with masters of
function calls to explain what happens for tasks and controlled created in
return objects then passed to another function call and other such silly things.

Robert will say (correctly) that no one would ever do any of these things in the
prefix of the 'Old attribute, but that doesn't absolve the Standard from
explaining what happens if someone does. (And I don't think
implementation-defined works; we've never done that for any issue involving
masters and it would seem bizarre to start with this feature.)

> When we have rules based on the enclosing whatever and then we invent
> an attribute which introduces an implicit declaration which is
> supposed to behave as though it syntactically encloses the attribute
> prefix, it does not seem surprising that we would have to describe
> this interaction in the rules somewhere.
>
> I'd prefer to see some clean, simple restrictions (perhaps on the form
> of the expressions, perhaps on their placement) which would spare us
> from dealing with this stuff.

The only "clean, simple" restriction that I can think of is objects (and
literals) only, and Bob has already said that isn't acceptable to him.
Perhaps that could be extended a bit to allow predefined operators, but I don't think we can allow arbitrary function calls if we want to avoid this mess.

OTOH, I'm not sure I really understand why Bob wants function calls in the
prefixes of these attributes, since that seems to be an abuse of the intended
functionality, which is to give access to the initial values of formal
parameters -- ain't no function calls in formal parameters. So perhaps these
restrictions are acceptable (as always, it is easier to relax restrictions in
future versions of the language than to add them if they prove to be needed).

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

From: Robert Dewar
Sent: Tuesday, August 31, 2010  3:18 AM

> OTOH, I'm not sure I really understand why Bob wants function calls in
> the prefixes of these attributes, since that seems to be an abuse of
> the intended functionality, which is to give access to the initial
> values of formal parameters --

or globals .. if the purpose of a procedure call is to modify some global
variables, it is quite reasonable to have post conditions that test that the
right thing has been done to them using 'Old.

> ain't no function calls in formal parameters. So perhaps these
> restrictions are acceptable

To me they are certainly acceptable. If you have a situation where

    F(X)'Old and F (X'OLd)

are different, it means that F is a nasty impure function. I don't think impure
functions are nasty in general, but I sure do thing that using functions with
side effects or other impurities is bad form in a postcondition in any case, let
alone in the prefix of 'Old!

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

From: Randy Brukardt
Sent: Tuesday, August 31, 2010  12:45 AM

[Slightly off-topic, and I know I should let this go, but...]

From Robert Dewar:
> BTW, I think it is no big deal if Randy's compiler fails to allow 'Old
> in assert pragmas. Also I find Randy's attitude to pragma assert plain
> bizarre (this pragma is VERY widely and heavily used throughout the
> GNAT sources, and many of our customers use it widely).

I think the fact that customers use it widely is simply because if you give
someone a hammer, a lot of problems start to look like a nail. (That is, it is
used because it is there.) It simply doesn't provide enough for the projects
I've worked on, and I usually find that it is better to use "regular" Ada code
to handle these sorts of checks. There are a number of reasons for this:

(1) I don't find that binary on/off is sufficient. There is often a need to
    partition the program into multiple parts for testing/debugging purposes.
    (This was especially true back in the bad old days of MS-DOS, with very
    little memory available.) AdaCore seems to have recognized this, given the
    invention of pragma Check in GNAT.

(2) In addition, I find that some of these checks are too expensive to leave on
    all of the time, and recompiling to turn them on and off is a significant
    pain. (Again, this was worse in the past than it is now; builds don't take
    two hours anymore.) Moreover, there is a similar pain for tracing/logging
    support. Tracing/logging tends to get a runtime manager UI of some sort in
    my programs for control/ease-of-debugging; once that exists, it makes sense
    to use it (rather than pragma Assert) to control expensive checks.

(3) I'm in the camp of turning off checks is like
    using-seatbelts-only-in-the-garage. So I don't see much reason to make it
    possible to eliminate cheap checks. Where we used to do that to save space
    in very early Janus/Ada compilers almost always seemed to lead to regrets
    down the road. One common example is the "dangling else", where after
    testing a bunch of conditions, we're left with an else case that doesn't
    seem to have an logical reason to exist. These days, I always try to stick
    an internal error into such cases, because they seem to get executed a lot
    more often than one would think, and simply ignoring them simply postpones a
    problem to a place where it is later much harder to find. So there is no
    need for pragma Assert in cases like this; the check should never be turned
    off and has little or no runtime cost unless there is a bug anyway.

(4) Pragma Assert only takes expressions, and that is too limiting for many
    tasks (Ada 2012 will mitigate this somewhat). If you have to write a support
    function, you've lost the ability to remove it easily (as it is not clearly
    part of the asserts).

(5) In Janus/Ada at least, dead code elimination is very effective and little
    vestige of unused code is left behind (that's a consequence of our
    memory-limited days). I expect that most modern compilers are similar. There
    isn't much need for a special feature that does what the compiler will do
    anyway (given an appropriate False expression, as explained in my original
    message on this subject). Pragma Assert doesn't help much with the real
    difficult problem of dead global data elimination (given that it only works
    on expressions).

(6) Finally, I think that the use of pragmas for runtime evaluation of things is
    an abuse of the concept as intended by Ada 83. I realize Ada 95 added a
    number of these things; I argued against them at the time (and obviously
    lost) and have not changed my opinion on that. Ada 2012 finally has a proper
    way to do things like pragma Priority; while we're obviously not going to
    get rid of any of the existing ones, we can finally move them to the dustbin
    in which they belong -- and thus anything that gives them more promenence is
    a bad idea IMHO.

Honestly, the only one of these things that can be considered "bizarre" is the
last, and even it is grounded in early Ada standards.

As I said, all of this comes from *my experience* with various systems.
Surely other sorts of systems have different requirements, so I can surely
believe that someone else finds more use for pragma Assert than I do. Even so, I
don't find it a very important part of Ada.

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

From: Bob Duff
Sent: Tuesday, August 31, 2010  9:54 AM

If we're really going to rehash this argument, we all ought to look at the old
'Old discussions!  ;-)

> To me they are certainly acceptable. If you have a situation where
>
>     F(X)'Old and F (X'OLd)
>
> are different, it means that F is a nasty impure function.

I don't think that's true (see (*) below).

>...I don't think impure functions are nasty  in general, but I sure do
>thing that using functions  with side effects or other impurities is
>bad form  in a postcondition in any case, let alone in the  prefix of
>'Old!

I basically agree with your attitude toward side effects.
(Not sure what "other impurities" means.) But I think this isn't the point.

I think F(X)'Old is more readable than F(X'Old).
This becomes more apparent when referring to multiple params/globals: F(X,
Y)'Old is better than F(X'Old, Y'Old).  I'd rather say:

    (((X**2) + (Y**2)) / Z)'Old

than:

    (((X'Old**2) + (Y'Old**2)) / Z'Old)

I realize I have to say:

    My_Type'(((X**2) + (Y**2)) / Z)'Old

which is annoying, but still preferable to sprinkling 'Old on all the variables.

Suppose somebody says:

    (((X'Old**2) + (Y'Old**2)) / Z)

Is that a bug (forgot 'Old on Z)?  Or is Z constant, so it doesn't need 'Old?
Or is Z a variable, but it doesn't get modified by this procedure, so doesn't
need 'Old?  This analysis requires a lot of thought, which is completely
obviated by putting 'Old on the whole expression.  (And I think I'd like a
warning if 'Old is applied to an expression whose value couldn't possibly have
changed since the start of the procedure.)

Efficiency issue: Consider F(X, Y)'Old.  Suppose X and Y are giant records, and
F returns Integer.  You really don't want to save copies of the giant records --
you want to save a copy of that Integer.

(*) As to my claim above: A long time ago, Randy gave a good example why.
Reference-counted (controlled) type.  We want to refer to Count(X)'Old.  That
saves the old value of the reference count. We do NOT want Count(X'Old), because
that saves the old value of X, which involves calling Adjust, thus MODIFYING the
ref count.  It is precisely to AVOID that side effect that we want Count(X)'Old.
In other words, your claim (with which I agree), "side effects [are] bad form
... in the prefix of 'Old!" argues for allowing Count(X)'Old.

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

From: Steve Baird
Sent: Tuesday, August 31, 2010  11:12 AM

> ... , but that doesn't absolve the Standard from explaining what
> happens if someone does [do these oddball things].

Agreed.

> The only "clean, simple" restriction that I can think of is objects (and
> literals) only, and Bob has already said that isn't acceptable to him.
> Perhaps that could be extended a bit to allow predefined operators,
> but I don't think we can allow arbitrary function calls if we want to
> avoid this mess.

I don't see any problem with allowing calls to most (but see Has_Polka_Dots
below) elementary-valued functions. But then where do you draw the line?

Are there problems if the type of the 'Old attribute is anonymous, as in

     Param.Array_Of_Limited_Discriminated(I).Access_Discriminant'Old
or
     Has_Polka_Dots (Anon_Access_Param =>
       Param.Array_Of_Aliased(I)'Access'Old)
?

We are certainly stretching the model here:
   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.

What is the type of this constant for these examples?

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

From: Steve Baird
Sent: Tuesday, August 31, 2010  11:21 AM

> I don't see any problem with allowing calls to most (but see
> Has_Polka_Dots below) elementary-valued functions.

Correction: please ignore the above reference to the Has_Polka_Dots example.
In that example, the function call did not occur as part of the prefix of the
'Old attribute. Oops.

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

From: Bob Duff
Sent: Tuesday, August 31, 2010  1:38 PM

> > The only "clean, simple" restriction that I can think of is objects
> > (and
> > literals) only, and Bob has already said that isn't acceptable to him.

Well, "acceptable" is a bit strong.  I'm not the boss, just one ARG member
trying convince the rest that we don't need these restrictions we are
discussing.  And anything that forbids calls is suspect, because calls are the
main tool of abstraction in Ada (or any other language).

> I don't see any problem with allowing calls to most (but see
> Has_Polka_Dots below) elementary-valued functions.

I still don't see why we need restrictions.  Why do you say "elementary"?
(Sorry if I'm being dense!)

(We do need a restriction forbidding 'Old applying to a package body.)

> But then where do you draw the line?
>
> Are there problems if the type of the 'Old attribute is anonymous, as
> in
>
>      Param.Array_Of_Limited_Discriminated(I).Access_Discriminant'Old
> or
>      Has_Polka_Dots (Anon_Access_Param =>
>        Param.Array_Of_Aliased(I)'Access'Old)
> ?
>
> We are certainly stretching the model here:
>    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.
>
> What is the type of this constant for these examples?

For the first, can't we say the type is "access Blah"?
I.e. a different anon access type, and if that causes illegality/weirdness due
to accessibility, then so be it. (I realize the current wording doesn't quite
say that. And I could live with a "no anon access" rule, since I hate anon
access anyway.)

For the second example, well you withdrew that in a subsequent message.

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

From: Steve Baird
Sent: Tuesday, August 31, 2010  2:01 PM

> For the second example, well you withdrew that in a subsequent
> message.

I didn't withdraw the example. I just noted that it had no bearing on the
question of whether function calls are ok as part of the prefix of a 'Old
attribute. Nonetheless, I think your comments about the 1st apply equally well
to the 2nd - we could support this or forbid it but the existing wording needs a
little work in either case.

> I still don't see why we need restrictions.  Why do you say
> "elementary"?

If a function call returns an elementary result, then there is no way that we
care about the accessibility level or the master of the function result object.
If it returns a composite result (e.g., a result with task components,
controlled components, and aliased components), then perhaps we do care. We
would like to avoid having to define the accessibility level or the master in
these cases, so (I think) we would like to avoid constructs which would require
such a definition.

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

From: Bob Duff
Sent: Tuesday, August 31, 2010  9:57 AM

> ...
> > Incidentally, I think that my fears about accessibility/master
> > complications for allocators may extend to other object-creating
> > constructs (at least aggregates; I'm not sure about function calls).
> >
> > Is there any need for a more detailed exploration of this?
>
> I'm afraid so. ...

I don't understand what the problem is.

'Old is defined by putting an implicit constant decl at the start of the
procedure.  That equivalence should explain what the
accessibility/master/blah/blah/blah rules are. No need to state them explicitly
in the RM. And no need for the compiler to do anything special -- just apply the
normal semantic analysis to that implicit decl.

Yesterday, Steve got me all frightened about coextensions and whatnot in
prefixes 'Old.  But now I think there's nothing to be afraid of.

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

From: Bob Duff
Sent: Tuesday, August 31, 2010  10:08 AM

> At this stage, that sounds reasonable to me! Although I would be
> happier if the name did not clash with the incompatible GNAT
> implementation, but perhaps 'Old is the only good name in the world?
> :-)

I really don't like the idea of having both 'Old and 'Old_Value existing in the
world, with subtly different rules, and people not being able to remember which
of them are standard vs. compiler specific.

I don't buy Tuck's argument against 'Old in arbitrary code.
It's basically the WYSIWYG-for-efficiency argument, and I rarely buy that.  I
mean, this is a language where "X: T;" might just allocate 4 bytes in the stack
frame and do nothing else.  Or, it might do all kinds of default initialization,
then later fire up some tasks, then later do finalization, with abort deferral
and so on.  And that's a good thing!

WYSIWYG is exactly the opposite of high-level language design.
If you want WYSIWYG, use assembly language.

So my preferred rule is that 'Old applies to the innermost body, and that body
must be a subprogram or entry.  No requirement that it be inside certain
pragmas.

If I can't convince folks of that, then I'd prefer GNAT change its handling of
'Old to include the arbitrary restrictions in the RM.  For compatibility, GNAT
can eliminate these restrictions in -X (allow extensions) mode.

Yes, 'Old "is the only good name in the world".  ;-) Please don't invent
'Old_Value.  'Old is the perfect name.

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

From: Robert Dewar
Sent: Wednesday, September  1, 2010  3:23 PM

>> To me they are certainly acceptable. If you have a situation where
>>
>>     F(X)'Old and F (X'OLd)
>>
>> are different, it means that F is a nasty impure function.
>
> I don't think that's true (see (*) below).


OK, these are convincing arguments!

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

From: Robert Dewar
Sent: Wednesday, September  8, 2010  9:44 AM

Just to summarize what I think the consensus was on some issues (and this is
what GNAT has implemented :-))

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

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

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

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