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

Differences between 1.5 and version 1.6
Log of other versions for file ai05s/ai05-0176-1.txt

--- ai05s/ai05-0176-1.txt	2010/02/23 01:05:48	1.5
+++ ai05s/ai05-0176-1.txt	2010/02/23 07:31:06	1.6
@@ -1,4 +1,4 @@
-!standard 2.9(2/2)                                  10-02-22  AI05-0176-1/03
+!standard 2.9(2/2)                                  10-02-22  AI05-0176-1/04
 !standard 3.3(19)
 !standard 4.4(7)
 !standard 4.5.9(0)
@@ -46,7 +46,7 @@
 directly an element of the collection, and we can use the proposed syntax of
 AI05-0139-2 to write:
 
-      for all X of Directory | Name (X)'Length < 20
+    for all X of Directory | Name (X)'Length < 20
 
 Where Directory is some container, or an array.
 
@@ -88,14 +88,16 @@
 
 Name Resolution Rules
 
-The expected type of a quantified expression is the predefined type Boolean.
-The predicate in a quantified_expression is expected to be of any boolean type.
+The expected type of a quantified expression is any Boolean type.
+The predicate in a quantified_expression is expected to be the same type.
 
 Dynamic Semantics
 
-The evaluation of a quantified expression evaluates the predicate for each
-value of the loop_parameter. These values are examined in the
-order specified by the loop_parameter_specification.
+For the evaluation of a quantified expression, the loop_parameter_specification
+is first elaborated. The evaluation of a quantified expression then evaluates
+the predicate for each value of the loop_parameter. These values are examined
+in the order specified by the loop_parameter_specification.
+
 The value of the quantified expression is determined as follows:
 
 * If the quantifier is "all" the expression is True if the evaluation of the
@@ -119,11 +121,12 @@
 
 The postcondition for a sorting routine on arrays with can be written:
 
-Post => (for all I:T in A'First .. A (T'Pred(A'Last)) | A (I) <= A (T'Succ (I)))
+Post => (for all I:T in A'First .. T'Pred(A'Last) | A (I) <= A (T'Succ (I)))
 
-The assertion that a positive number is composite can be written:
+The assertion that a positive number is composite (as opposed to prime) can be
+written:
 
-   (for some X in 2 .. N / 2 | N mod X /= 0)
+   (for some X in 2 .. N / 2 | N mod X = 0)
 
 !discussion
 
@@ -1613,5 +1616,332 @@
 implies N is prime.
 
 Or am I confused?
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Monday, February 22, 2010  8:20 PM
+
+No, you are right, my slip of the finger (was translating from the predicate for
+primality, one negation too many)
+
+****************************************************************
+
+From: Steve Baird
+Sent: Monday, February 22, 2010  7:02 PM
+
+> The postcondition for a sorting routine on arrays with can be written:
+>
+> Post => (for all I:T in A'First .. A (T'Pred(A'Last)) | A (I) <= A
+> (T'Succ (I)))
+
+Am I right in assuming that you meant
+      T'Pred (A'Last)
+as opposed to
+      A (T'Pred (A'Last))
+?
+
+
+I'm also not sure about
+>    The expected type of a quantified expression is the
+>    predefined type Boolean.
+
+I think we want to replace this sentence with something that more closely
+follows the rule for a qualified expression. That is, say nothing about the
+expected type of a quantified expression (that, after all, is determined by
+its context) and instead add a static semantics rule along the lines of
+4.7(3.1/3):
+    The nominal subtype of a quantified_expression is the predefined
+    type Boolean.
+
+It would seem oddly fitting to have some sort of parallel between quantified
+expressions and qualified expressions.
+
+Finally, do we need to state (in the dynamic semantics section) that the
+loop_parameter_specification is elaborated? See 5.5(9).
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, February 22, 2010  7:20 PM
+
+Shouldn't the type of the expression be the same as the type of the predicate?
+Otherwise you have some weird implicit conversion going on here, which might
+require a change of representation (if the encoding of the boolean types is
+different).
+
+Else I agree with the rest of your comments.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Monday, February 22, 2010  8:24 PM
+
+>Am I right in assuming that you meant
+>    T'Pred (A'Last)
+>as opposed to
+>    A (T'Pred (A'Last))
+>?
+
+No, I want  A(A'Last -1),  T is the index type.
+
+...
+>It would seem oddly fitting to have some sort of parallel between
+>quantified expressions and qualified expressions.
+
+I don't know, I also see quantified expressions as conditions in an
+if-statement, for which we do state the expected type. That parallel does not
+work for me.
+
+>Finally, do we need to state (in the dynamic semantics section) that
+>the loop_parameter_specification is elaborated? See 5.5(9).
+
+Yes.  in particular now that it can include some complex container-valued
+expression
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Monday, February 22, 2010  8:33 PM
+
+>>> The postcondition for a sorting routine on arrays with can be
+>>> written:
+>>> Post => (for all I:T in A'First .. A (T'Pred(A'Last)) | A (I) <= A
+>>> (T'Succ (I)))
+>>
+>> Am I right in assuming that you meant
+>>     T'Pred (A'Last)
+>> as opposed to
+>>     A (T'Pred (A'Last))
+>> ?
+
+Indeed, you are right, this is the range for the index.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Monday, February 22, 2010  8:58 PM
+
+> Shouldn't the type of the expression be the same as the type of the
+> predicate? Otherwise you have some weird implicit conversion going on
+> here, which might require a change of representation (if the encoding
+> of the boolean types is different).
+
+I thought about this exact point and decided that I prefer Ed's proposed rule.
+The rule you propose would be somewhat more complex to specify and (probably)
+somewhat more complex to implement. The only benefit would be slightly more
+intuitive semantics in a case that nobody cares about.
+
+I say "slightly" because I have no problem thinking of
+
+     (for all I in Some_Range | Some_Derived_Boolean_Type'(Foo (I)))
+
+as being equivalent to a call to a function with body
+
+     Temp : Standard.Boolean := True;
+   begin
+     for I in Some_Range loop
+        if Some_Derived_Boolean_Type'(Foo (I)) = False then
+           Temp := False;
+           exit;
+        end if;
+     end loop;
+     return Temp;
+.
+
+On the other hand, I don't feel strongly about this. There are good arguments
+for the rule you suggest. Either way is ok with me.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Monday, February 22, 2010  9:41 PM
+
+>> It would seem oddly fitting to have some sort of parallel between
+>> quantified expressions and qualified expressions.
+>
+> I don't know, I also see quantified expressions as conditions in an
+> if-statement, for which we do state the expected type. That parallel
+> does not work for me.
+
+At the very least we should replace the proposed "is" rule with a "shall be"
+rule:
+     The expected type of a quantified expression shall be the
+     predefined type Boolean.
+
+Consider a bad construct such as
+
+     X : Float := (for all I in ...);
+
+. We do not want to define the expected type of the quantified expression to be
+Boolean - that would conflict with the definition of expected type that is
+inherited from context (in this case, 3.3.1(4)).
+
+I think (but this would have to be checked - I'm not sure) that the rule I
+originally suggested would then follow as a consequence.
+
+Still, an expression whose type is known independently of the context in which
+it occurs strikes me as being very similar to a qualified expression and I think
+it would be clearest to follow that example.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Monday, February 22, 2010  9:51 PM
+
+...
+>At the very least we should replace the proposed "is" rule with a
+>"shall be" rule:
+>   The expected type of a quantified expression shall be the
+>   predefined type Boolean.
+
+or "any boolean type" as for conditions in if-statements.
+
+...
+>Still, an expression whose type is known independently of the context
+>in which it occurs strikes me as being very similar to a qualified
+>expression and I think it would be clearest to follow that example.
+
+Not sure I follow, this is the same phrasing as for conditions in if-statements,
+and those are not qualified expressions. Of course, those conditions are in one
+specific context, while quantified expressions are just expressions that can
+appear anywhere.  So whatever is clearer.  Still, the expected type of the
+predicate must be the same as that of the expression as a whole.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, February 22, 2010  10:10 PM
+
+>Not sure I follow, this is the same phrasing as for conditions in
+>if-statements, and those are not qualified expressions.
+
+Steve is right. An if-statement is a context that *provides* an expected type.
+Kinds of expressions are defined to match certain expected types, they don't
+have them
+
+>Of course, those conditions are in one specific context, while
+>quantified expressions are just expressions that can appear anywhere.
+>So whatever is clearer. Still, the expected type of the predicate must
+>be the same as that of the expression as a whole.
+
+I had suggested that, and Steve thought it was better that quantified
+expressions always returned type Boolean. I don't think it matters that much.
+Steve now seems to be suggesting a resolution rule like that of qualified
+expressions:
+
+A quantified_expression shall resolve to type Boolean.
+
+But this is a bit different than regular resolution, as it doesn't include
+implicit conversions. Not sure that matters in this case (I can't think of a
+reason).
+
+An alternative would be to have a legality rule:
+
+The expected type of a quantified_expression shall be a boolean type.
+
+Not sure that works, though, so probably following the model of qualified
+expressions is better.
+
+Note that we might want the equivalent of the 4.7(3.1/3) rule, which specifies
+the nominal subtype. But since we didn't do that for conditional or case
+expressions (and I really don't want to go there!), maybe we don't need it here,
+either. (But note that 4.7(3.1/3) has nothing to do with resolution; we
+definitely need *some* rule about the resolution of a quantified_expression.)
+
+****************************************************************
+
+From: Steve Baird
+Sent: Monday, February 22, 2010  10:21 PM
+
+>> At the very least we should replace the proposed "is" rule with a
+>> "shall be" rule:
+>>    The expected type of a quantified expression shall be the
+>>    predefined type Boolean.
+>
+> or "any boolean type" as for conditions in if-statements.
+
+That would be fine too.
+As I mentioned in an earlier reply to Randy, I prefer your original rule but I don't feel strongly about it.
+
+...
+>> Still, an expression whose type is known independently of the context
+>> in which it occurs strikes me as being very similar to a qualified
+>> expression and I think it would be clearest to follow that example.
+>>
+> Not sure I follow, this is the same phrasing as for conditions in
+> if-statements, and those are not qualified expressions.
+
+I was just repeating myself, stating that the proposed "shall be"
+wording is my second choice; I still prefer
+   The nominal subtype of a quantified_expression is the predefined
+   type Boolean.
+
+On the other hand, if we adopt the "any boolean type" rule that you mentioned
+above, then the parallel with qualified expressions falls apart (the type of a
+quantified expression could no longer be determined independently of its
+context). In that case, I think the "shall be" wording would be best.
+
+ >  So whatever is clearer.
+
+Agreed. Let's see what others think.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, February 22, 2010  10:40 PM
+
+> Corrected text follows.
+
+I changed the example again, as you forgot to change 1 to 2 in the loop.
+Moreover, everytime I read the leadin "The assertion that a positive number is
+composite can be written:" I think the answer is "False" (because "composite"
+has a meaning in Ada, and a number is never composite in Ada). I changed it to:
+
+The assertion that a positive number is composite (as opposed to prime) can be
+written:
+
+So as to avoid confusion for Ada-lawyer readers.
+
+---
+
+You changed the resolution rule to:
+
+The expected type of a quantified expression is any Boolean type.
+The predicate in a quantified_expression is expected to be the same type.
+
+This is completely backwards. As Steve says, expected types always come from
+context. Moreover, not all expressions have expected types at all (qualified
+expressions don't, for instance). So it is dangerous to talk about the expected
+type of the expression. (We fought this for conditional_expressions; we
+eventually used the rules that () would have if they actually had rules.)
+
+We could use similar rules here:
+
+If a quantified_expression is expected to be of a type T, the expected type for
+each *dependent_*expression of the quantified_expression is T. If a
+quantified_expression shall resolve to a type T, each dependent_expression shall
+resolve to T.
+
+And then we'd need a legality rule:
+
+The type of a quantified_expresion shall be a boolean type.
+
+Alternatively, we could follow Steve's suggestion. However, that is unfortunate
+as the only place the type (as opposed to the subtype, and we just added that
+very recently) of a qualified_expression is defined is in the informal
+introductory text. (Ignore my previous message on this subject.) So there isn't
+a good example to copy.
+
+Aside: We didn't try to identify the type of a conditional expression, much less
+the subtype. So what is the completeness rule for a case statement? Consider:
+
+    case (if Func then 1 else 2) is
+       when 1 => null;
+       when 2 => null;
+    end case;
+
+Is an others required or not?? Same applies to a case_expression. (Darn, I'm
+thinking like Steve now.)
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent