CVS difference for ai05s/ai05-0153-3.txt

--- ai05s/ai05-0153-3.txt	2011/01/25 08:00:08	1.3
+++ ai05s/ai05-0153-3.txt	2011/01/27 06:06:16	1.4
@@ -1267,6 +1267,37 @@
 
 ****************************************************************
 
+From: Robert Dewar
+Sent: Tuesday, January 25, 2011   6:14 AM
+
+> Or perhaps something like:
+>
+>     pragma Restrictions(No_Aspect_Specification =>
+> Dynamic_Predicate);
+>
+> to be analogous to "No_Dependence =>  ...".
+
+Can't we just have
+
+   No_Aspect => name
+
+I see no advantage to reader or writer in adding the Specification part here,
+especially if it also bans a corresponding pragma or attribute.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, January 25, 2011   6:15 AM
+
+> Yes, that's better.  For those aspects that are also attributes, you
+> probably want to restrict the specification, but not the query.
+>
+>> to be analogous to "No_Dependence =>  ...".
+
+OK, I see, grumble, I guess the long name will have to do
+
+****************************************************************
+
 From: Randy Brukardt
 Sent: Monday, January 24, 2011  9:29 PM
 
@@ -1444,6 +1475,259 @@
 me at least) to be biased against the solution we chose. I realize that it is
 asking a lot of you to provide those arguments, as you don't believe in them.
 I'll help you do it if needed.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Tuesday, January 25, 2011   10:07 AM
+
+> It would be nice to say more in *favor* of the split as well; the text
+> seems (to me at least) to be biased against the solution we chose.
+
+Indeed, it is biased in that direction.
+
+>..I realize that
+> it is asking a lot of you to provide those arguments, as you don't
+>believe  in them. I'll help you do it if needed.
+
+I can cut&paste your other e-mail (the one that mentions snapping) as a
+counter-argument.
+
+****************************************************************
+
+From: John Barnes
+Sent: Wednesday, January 26, 2011   7:57 AM
+
+I have lost track of this topic slightly.
+
+If we have to have two and the static one is just like the dynamic one but
+requires the stuff to be static then why don't we call them Subtype_Predicate
+and Static_Subtype_Predicate.
+
+Without Subtype it is not so clear what they refer to.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Wednesday, January 26, 2011   8:11 AM
+
+> I have lost track of this topic slightly.
+>
+> If we have to have two and the static one is just like the dynamic one
+> but requires the stuff to be static
+
+That's one difference.  The other difference is that the static ones are allowed
+in more places (e.g. in case stms).
+
+>...then why don't we call them
+> Subtype_Predicate and Static_Subtype_Predicate.
+>
+> Without Subtype it is not so clear what they refer to.
+
+    subtype Nonzero is Integer with Static_Predicate => Nonzero /= 0;
+
+It seems pretty clear from the syntax what the predicate refers to!
+
+I think adding "Subtype_" is just extra noise.
+The names are too long as it is.
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Wednesday, January 26, 2011   8:48 AM
+
+>> Without Subtype it is not so clear what they refer to.
+>
+>     subtype Nonzero is Integer with Static_Predicate => Nonzero /= 0;
+>
+> It seems pretty clear from the syntax what the predicate refers to!
+>
+> I think adding "Subtype_" is just extra noise.
+> The names are too long as it is.
+
+plus it would be confusing when the predicate aspect is applied to a type
+definition, I think:
+
+  type Nonzero_Small is range -10 .. 10 with
+    Subtype?_Static_Predicate => Nonzero_Small /= 0;
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, January 26, 2011   9:33 AM
+
+I think the difference is bigger than what you imply.
+
+Dynamic_Predicates aren't reevaluated every time they might become false,
+whereas Static_Predicates are designed so that (barring erroneous execution)
+they are rechecked at every point where they might become false.
+
+So Dynamic_Predicates are sort of like assertions that are periodically
+rechecked, while a Static_Predicate is something that is continuously True.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, January 26, 2011  10:31 AM
+
+> plus it would be confusing when the predicate aspect is applied to a
+> type definition, I think:
+>
+>    type Nonzero_Small is range -10 .. 10 with
+>      Subtype?_Static_Predicate =>  Nonzero_Small /= 0;
+
+Right, I agree, in the above, Nonzero_Small is technically a subtype name, but
+real programmers consider it a type name :-)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Wednesday, January 26, 2011  10:41 AM
+
+> So Dynamic_Predicates are sort of like assertions that are
+> periodically rechecked, while a Static_Predicate is something that is
+> continuously True.
+
+That's not quite true.  I suppose you could say it's almost true.  ;-) It's as
+true for static predicates as it is for constraints. And you're right that it's
+less true for dynamic predicates that for static predicates and constraints.
+
+    subtype S is Integer range -10..10 with Static_Predicate => S /= 0;
+
+    X : S;
+    Y : S := 1; -- (1)
+
+    Y := X; -- (2)
+
+The constraint and predicate of Y are both true at (1), but either could become
+false at (2).  This is of course a bounded error, but it's not quite erroneous.
+
+The AI allows to omit the predicate check at (2), but I'm not sure I got the
+wording right.  I wanted to defer arguing about that until after we agree on the
+other (more important) rules.
+
+In any case, I think it's important to keep the "invalid data"
+loophole in mind, when arguing about whether the sky is falling or the colander
+is leaky or whatever.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, January 26, 2011   5:19 PM
+
+> The constraint and predicate of Y are both true at (1), but either
+> could become false at (2).  This is of course a bounded error, but
+> it's not quite erroneous.
+
+Your point is technically correct, but this example doesn't illustrate it very
+well. Virtually every compiler implementation has some concept like "known to be
+valid". For any object that is "known to be valid", checks on assignment can
+only be eliminated if the source is also "known to be valid" (otherwise the
+property is a lie). In this example, Y is "known to be valid" in Janus/Ada (and
+I would expect in most other compilers). The reason for the property is so that
+checks can be eliminated on use; array and case checks, for example, can never
+be eliminated unless the source object is "known to be valid" (since eliminating
+the checks would change from a bounded error to erroneous execution, which is
+not allowed).
+
+So I would consider any implementation that removed the checks at (2) broken, in
+a practical if not language lawyer sense. (It's also *very* user-unfriendly.)
+[All of the above is assuming no pragma Suppresses and no erroneous execution,
+of course.]
+
+However, if you make the example more complex, the issue becomes murkier.
+Janus/Ada is very syntax-based, and thus just moving the initialization changes
+the "known to be valid" property:
+
+      X, Y : S;
+
+      Y := 1; -- (1)
+      Y := X; -- (2)
+
+Y is not "known to be valid", so the checks at (2) aren't generated unless the
+user has set strict checking mode.
+
+A static_predicate will follow the same exact model for checking and checking
+elimination in Janus/Ada (and I would expect other compilers as well). I'm not
+sure about dynamic_predicates; I would guess that eliminating them would be a
+serious mistake unless the compiler can prove no side-effects (often hard).
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, January 26, 2011   5:41 PM
+
+> So I would consider any implementation that removed the checks at (2)
+> broken, in a practical if not language lawyer sense. (It's also *very*
+> user-unfriendly.) [All of the above is assuming no pragma Suppresses
+> and no erroneous execution, of course.]
+
+You can consider what you like, but the language quite deliberately does NOT
+require a check here, and I personally would consider any compiler which always
+did the check here as broken. Certainly GNAT will NOT do the check by default
+(though it can be forced on with full non-standard validity checking).
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, January 26, 2011   6:18 PM
+
+There seem to be (at least) two basic strategies for dealing with uninitialized
+variables in Ada 95+:
+
+One approach deals with the potential for invalid values on the few uses where
+they can turn into erroneous execution, such as array indexing and case
+statements.  The other approach has the notion of objects whose subtypes can be
+"trusted" and objects whose subtypes cannot be trusted.  With this latter
+approach, when assigning from an "untrusted" object to a "trusted" object, you
+always do a check.
+
+Either approach can work, and I don't consider either approach "broken."  I
+believe GNAT takes the first approach by default, but can be convinced to take
+one more nearly approximating the second approach. AdaMagic (and it sounds like
+Janus/Ada) takes the second approach, or something close to it.
+
+We should try to keep these two approaches in mind rather than making overly
+general statements about how code involving uninitialized variables should be
+compiled.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, January 26, 2011   6:30 PM
+
+Fair enough!
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, January 26, 2011   9:17 PM
+
+I apologize for using an inflamatory word like "broken" in relationship to a
+particular compiler. It's unfair mainly because the problem is with the language
+and not the compiler.
+
+The only people who ought to have to even consider the effect of uninitialized
+variables in code are language lawyers and compiler implementers. To the extent
+that that is not true, it is the language, and not any specific implementation,
+that is broken.
+
+It is very unfriendly to the user to allow values that are out of range to be
+assigned to objects. Period. We allow that for code efficiency reasons, of
+course, but that also makes it far harder for the user to understand their
+programs.
+
+To the extent possible, checks should be made as early as possible, and should
+be as close as possible to the canonical semantics. The "trusted" approach (as
+Tucker called it) does this better (IMHO) than any other approach. And I think
+compilers always should go for user-friendliness when the choice of two nearly
+equal approaches occur.
+
+But of course there are other considerations as well. And the real issue is that
+the language allows unfriendly approaches in the first place.
+
+In any case, all of this is not relevant to any current discussion. So let's
+drop it here.
 
 ****************************************************************