CVS difference for ai05s/ai05-0145-2.txt

--- ai05s/ai05-0145-2.txt	2010/01/09 01:31:29	1.4
+++ ai05s/ai05-0145-2.txt	2010/01/21 05:29:15	1.5
@@ -1,6 +1,7 @@
 !standard 13.3.2 (00)                                09-12-28  AI05-0145-2/03
 !class amendment 09-06-12
 !status Amendment 201Z 09-12-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
@@ -540,5 +541,90 @@
 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 <some_condition> then (if Count(Obj'Old) = 1 then Count(Obj) = 0)
+               else (Count(Obj'Old) = Count(Obj))) is
+   begin
+       if <Some_condition> 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...)
 
 ****************************************************************