--- 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