CVS difference for ai05s/ai05-0146-1.txt

--- ai05s/ai05-0146-1.txt	2009/02/17 06:16:30	1.1
+++ ai05s/ai05-0146-1.txt	2009/03/15 03:48:33	1.2
@@ -229,3 +229,238 @@
 
 ****************************************************************
 
+From: Bob Duff
+Sent: Tuesday, February 24, 2009  10:25 AM
+
+[Find the message that this is replying to in AI05-0145-1.]
+
+>      type Set is interface
+>        with
+>          Invariant'Class =>
+>            (Is_Empty(X)) = (Count(X) = 0);
+
+I think invariants should apply to subtypes, not just types.
+I think they are like constraints, and at least for scalars, can be checked in
+the same places.
+
+****************************************************************
+
+From: Gary Dismukes
+Sent: Thursday, February 26, 2009  12:09 AM
+
+Randy brought up that point at the meeting and he has an action item to make a
+specific proposal along those lines.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Thursday, February 26, 2009  12:09 AM
+
+I agree with this, BTW, I find Tuck's syntax suggestion basically nice, and
+think that pre/post conditions are important enough to warrant syntax additions.
+
+I do think that postconditions in the body are useful, and so would keep the
+pragmas, certainly in GNAT anyway. It is true that preconditions in the body
+are just assertions, so they are there just for symmetry, but postconditions
+in the body are useful in that they come up front, which is the right position,
+and they block all exits (which would be tedious to do manually with assertions).
+I also think it is good to be able to control pre/post conditions separately
+from normal assertions.
+
+****************************************************************
+
+From: Alan Burns
+Sent: Thursday, February 26, 2009  7:21 AM
+
+> I think invariants should apply to subtypes, not just types.
+> I think they are like constraints, and at least for scalars, can be 
+> checked in the same places.
+   
+I've not followed the recent discussion on invariants, but am not sure how
+you deal with the usual invariant that is true most of the time but not
+during atomic updates.  Or a loop invariant that is true at the end of each
+iteration but not during an iteration.
+
+pre and post conditions are specific as to when they should evaluate to true,
+but invariants cover a region (but not the whole program)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, February 26, 2009  7:40 AM
+
+> I've not followed the recent discussion on invariants, but am not sure 
+> how you deal with the usual invariant that is true most of the time 
+> but not during atomic updates.
+
+I'm not sure, either.  That issue deserves some careful thought.
+Perhaps scalars should be different from records?
+
+>...  Or a loop invariant that is
+> true at the end of each iteration but not during an iteration.
+
+Isn't the loop-invariant case just a "pragma Assert" written at some point
+within the loop (e.g. at the end of each iteration)?  I don't see any need for
+a new feature for loop invariants.
+
+The invariants I'm thinking of should apply to [sub]types.  Maybe also to packages.
+
+> pre and post conditions are specific as to when they should evaluate 
+> to true, but invariants cover a region (but not the whole program)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, February 26, 2009  9:18 AM
+
+> I think invariants should apply to subtypes, not just types.
+> I think they are like constraints, and at least for scalars, can be 
+> checked in the same places.
+
+We discussed this, and concluded that invariants and user-defined constraints
+are both useful, but they are not the same thing.  Invariants are generally
+imposed on the implementation of an abstraction, and translate into
+*postconditions* on all operations that return values to the "outside" world.
+Constraints are often used as *preconditions* on values being passed *in* to
+a subprogram, and generally are required to be satisfied at all points, whereas
+invariants are often false in the middle of a primitive operation.
+
+So we concluded, I believe, that invariants are associated with an abstraction,
+and hence a type, or perhaps a package, while constraints define a subset of
+the values of a type, and hence are appropriately associated with a subtype.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, February 26, 2009  7:57 AM
+
+Question: In an invariant, does one refer to the "current instance" in the
+usual way, by naming the [sub]type?  As in:
+
+    type My_Int is range 0..1_000_000;
+
+    subtype My_Even_Int is My_Int with
+        Invariant => (My_Even_Int mod 2) = 0;
+
+
+> I've not followed the recent discussion on invariants, but am not sure 
+> how you deal with the usual invariant that is true most of the time 
+> but not during atomic updates.
+
+For scalars, one can use 'Base as always.  E.g. if you have X: in out My_Int,
+and you want to temporarily set it to a negative number, you do something like:
+
+    Temp : My_Int'Base := X;
+    Temp := Temp - 10; -- might be negative
+    Temp := abs Temp;
+    X := Temp; -- OK, Temp is now nonnegative
+
+Similarly, My_Even_Int'Base would be a subtype that is NOT restricted to even
+numbers.
+
+Not sure how this can work for records.
+
+By the way, I think the "in" operator should take invariants into account.
+E.g.:
+
+    if Blah in My_Even_Int then ...
+
+would be True iff Blah is an even number in the 0..1_000_000 range.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Thursday, February 26, 2009  12:50 PM
+
+> Question: In an invariant, does one refer to the "current instance"  
+> in the
+> usual way, by naming the [sub]type?  As in:
+>
+>    type My_Int is range 0..1_000_000;
+>
+>    subtype My_Even_Int is My_Int with
+>        Invariant => (My_Even_Int mod 2) = 0;
+
+Invariants are intended for private types only.  Otherwise the invariant
+may have to be verified on assignment or any operation that would visibly
+modify a value of the type outside of the defining package. This is
+impractical and not particularly useful (we have constraints for this, and
+invariants are NOT constraints).  By limiting the invariant to a private
+type, the check is limited to the visible primitive operations of the type
+(what happens otherwise in the body stays in the body).
+
+****************************************************************
+
+From: Stephen Michell
+Sent: Thursday, February 26, 2009  1:04 PM
+
+In general, I like Tucker's proposal.
+
+On the issue of invariance, Alan is completely correct. Invariance for,
+say,  the relationship between components or between state variables in a
+class only allies when they are no threads executing subprograms that may
+change that state. 
+
+You can make invariance work for every execution step, but in general that
+is going to require auxillary variables and a lot of very hard work.
+
+We need to develop syntax to express when invariance applies, or possibly
+when it does not apply, such as loop invariants only apply at the exit
+condition and state invariants only apply at the precondition and
+postcondition points of every subprogram that can see the state.
+
+As part of this effort, we need a syntax for auxillary variables, declaration,
+assignment and formal relationships.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, February 26, 2009  1:49 PM
+
+> I think invariants should apply to subtypes, not just types.
+> I think they are like constraints, and at least for scalars, can be 
+> checked in the same places.
+
+We talked about that at my insistence. We decided that invariants and
+constraints are different things that solve different problems. (Which
+is what I have been saying all along.) Invariants apply to all values of
+a type, and can be inherited. Constraints apply to particular views (not
+necessarily an object). Constraints are checked at the points that language
+currently defines (subtype conversion); invariants are checked only when
+crossing the boundary of the defining package.
+
+I was tasked in writing up a proposal for user-defined constraints
+(resurrecting my old proposal on that topic, but now using syntax and
+legality rules).
+
+If we can have only one of these, I think user-defined constraints are far
+more useful. But I can see uses for both.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Friday, February 27, 2009  12:58 AM
+
+> By limiting the invariant to
+> a private type, the check is limited to the visible primitive 
+> operations of the type  (what happens otherwise in the body stays in the body).
+ 
+I understand limited to visible operations, but why primitives?
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Friday, February 27, 2009  2:57 PM
+
+No reason, written in haste. Of course visible classwide operations are included.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Saturday, February 28, 2009  5:11 AM
+
+Actually, I was thinking of operations that are not primitive because they are
+declared, f.e., in a subpackage.
+
+****************************************************************
+