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

--- ai05s/ai05-0145-2.txt	2009/12/29 05:54:24	1.3
+++ ai05s/ai05-0145-2.txt	2010/01/09 01:31:29	1.4
@@ -78,15 +78,14 @@
   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 converted to T'Class. Similarly, a name that
-  denotes a formal access parameter of type access-to-T is converted to
-  access-to-T'Class. Finally, if the subprogram is a function returning
-  T or access T, the Result attribute is converted to 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.]
+  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.]
 
           Legality Rules
 
@@ -175,8 +174,16 @@
 outside the protected action associated with a protected subprogram
 call.
 
-!example
+!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
@@ -206,6 +213,51 @@
     --  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).
+
 !ACATS test
 
 
@@ -390,5 +442,103 @@
 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.
+
+- Bob
+
+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".
 
 ****************************************************************