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

Differences between 1.1 and version 1.2
Log of other versions for file ai05s/ai05-0147-1.txt

--- ai05s/ai05-0147-1.txt	2009/03/14 08:05:26	1.1
+++ ai05s/ai05-0147-1.txt	2009/03/15 03:48:09	1.2
@@ -1,4 +1,4 @@
-!standard 4.4 (07)                                09-03-13  AI05-0147-1/01
+!standard 4.4 (07)                                09-03-14  AI05-0147-1/02
 !standard 4.5.7 (0)
 !standard 4.7(2)
 !standard 4.7(3)
@@ -44,6 +44,10 @@
 Similar problems occur avoiding overflow in the expressions of the bounds of a
 range.
 
+One could write a local function to evaluate the expression properly, but that
+doesn't work if the expression is used in a context where it has to be static
+(such as specifying the size of a subtype).
+
 A conditional expression would make writing this expression easy:
 
          subtype Calculation_Range is Natural range 0 ..
@@ -68,7 +72,7 @@
 
 In 4.4(7), add:
 
-primary ::= 
+primary ::=
    numeric_literal | null | string_literal | aggregate
  | name | allocator | (expression) | conditional_expression
 
@@ -115,20 +119,21 @@
 
 In 4.7(2), add conditional_expression:
 
-qualified_expression ::= 
+qualified_expression ::=
    subtype_mark'(expression) | subtype_mark'aggregate |
    subtype_mark'conditional_expression
 
 In 4.7(3), modify the start of the paragraph:
 
-The *operand* (the expression{,}[ or] aggregate{, or conditional_expression}) shall...
+The *operand* (the expression{,}[ or] aggregate{, or conditional_expression})
+shall...
 
 In 4.7(5), modify the note:
 
 When a given context does not uniquely identify an expected type, a
-qualified_expression can be used to do so. In particular, if an overloaded name{,}[ or]
-aggregate{, or conditional_expression} is passed to an overloaded subprogram, it might
-be necessary to qualify the operand to resolve its type. 
+qualified_expression can be used to do so. In particular, if an overloaded
+name{,}[ or] aggregate{, or conditional_expression} is passed to an overloaded
+subprogram, it might be necessary to qualify the operand to resolve its type.
 
 Add after 4.9(12):
 
@@ -140,56 +145,82 @@
 A static expression is evaluated at compile time except when:
  * it is part of the right operand of a static short-circuit control form whose value
    is determined by its left operand;
- * it is the dependent_expression of some part of a conditional_expression,
-   and one or more conditions of preceeding parts of the conditional_expression
-   has the value True.
-
-[Editor's note: This wording requires all conditions of a conditional_expression
-to be evaluated at compile-time (including ones after the first true one); we could
-try to include the order of evaluation but that would require a much messier definition,
-because we would have to talk about the actual order of evaluation. Boolean expressions
-are fairly unlikely to overflow anyway.]
+ * it is part of a condition of some part of a conditional_expression, and at
+   least one and at least one condition of a preceeding part of the
+   conditional_expression has the value True; or
+ * it is part of the dependent_expression of some part of a
+   conditional_expression, and the associated condition evaluates to False; or
+ * it is part of the dependent_expression of some part of a
+   conditional_expression, and at least one condition of a preceeding part of
+   the conditional_expression has the value True.
+
+AARM Reason: We need the last bullet so that only a single dependent_expression is
+evaluated if there is more than one condition that evaluates to True.
+End AARM Reason.
 
 The compile-time evaluation of a static expression is performed exactly, without
-performing Overflow_Checks. For a static expression that is evaluated: 
+performing Overflow_Checks. For a static expression that is evaluated:
+
+[Editor's note: Adam Beneschan suggested in AC-0171 to add another cases to this
+list - an aggregate others clause known to denote zero elements:
+
+  * it is part of the expression of an array_component_association whose
+    discrete_choice_list is statically known to denote zero
+    components.
+
+I don't think this level of detail is common enough to add to the language, but
+the rewrite of this paragraph would make it easy to add here if desired.]
 
 
 !discussion
 
-The syntax of Ada requires that we require some sort of surrounding syntax to make
-a conditional expression different than a if statement. Without that requirement,
-we would have code like:
+The syntax of Ada requires that we require some sort of surrounding syntax to
+make a conditional expression different than a if statement. Without that
+requirement, we would have code like:
 
    if if Func1 then Func2 then Proc1; end if;
 
-Even if the compiler can figure it out (which is not clear to the author), it would be
-dicey for a human, and small errors such as leaving out a semicolon could change the
-meaning of a statement drastically.
-
-The obvious choice is to surround a conditional expression with parenthesis. This is
-already a common Ada design choice, and will be familar to Ada programmers. Other choices,
-such as using square brackets (currently unused in Ada), or using syntax other than
-"if", would be less familar and would cause programmers a confusion as to which syntax
-to use in a given location.
-
-Thus, we design conditional expressions work like and look like aggregates. This the
-reason that they are defined to be a primary rather than some other sort of expression.
-The fact that the parenthesis are required makes this preferable (it would be confusing
-otherwise).
-
-One could imagine rules allowing the parenthesis being omitted in contexts where they
-are not needed, such as a pragma argument. However, this would simply add conceptual
-overhead - it important to note that this was not done for aggregates except in the
-case of qualified expressions. We follow the same strategy here.
+Even if the compiler can figure it out (which is not clear to the author), it
+would be dicey for a human, and small errors such as leaving out a semicolon
+could change the meaning of a statement drastically.
+
+The obvious choice is to surround a conditional expression with parentheses.
+This is already a common Ada design choice, and will be familar to Ada
+programmers. Other choices, such as using square brackets (currently unused in
+Ada), or using syntax other than "if", would be less familar and would cause
+programmers a confusion as to which syntax to use in a given location.
+
+Thus, we design conditional expressions work like and look like aggregates. This
+the reason that they are defined to be a primary rather than some other sort of
+expression. The fact that the parentheses are required makes this preferable (it
+would be confusing otherwise).
+
+One could imagine rules allowing the parenthesis being omitted in contexts where
+they are not needed, such as a pragma argument. However, this would add
+conceptual overhead - it important to note that this was not done for aggregates
+except in the case of qualified expressions. It also would make syntax error
+correction much harder. Consider the following syntactically incorrect Ada code:
+
+     exit when if Foo then B := 10; end if;
+
+Currently, syntax error correction most likely would identify a missing
+expression and semicolon. With the conditional expression syntax without
+parentheses, the syntax is correct up until the ":=", at which point it is
+likely too late for the compiler to determine that the real error occurred much
+earlier. Nor would it be easy for the programmer to see where the error is.
+(Remember that Foo and B can be arbitrarily complex and on multiple lines.) With
+a required parenthesis, syntax correction would either identify the parenthesis
+or the expression as missing, showing the correct point of the error.
 
+
 Following the model of aggregates also simplifies the resolution of conditional
-expressions. This avoids nasty cases of resolution, in which a compiler
-might be able to figure out a unique meaning but a human could not. For instance,
-given the declarations:
+expressions. This avoids nasty cases of resolution, in which a compiler might be
+able to figure out a unique meaning but a human could not. For instance, given
+the declarations:
 
    procedure Q (A, B : Integer);
    procedure Q (A, B : float);
- 
+
    function F return Integer;
    function F return Boolean;
 
@@ -199,10 +230,15 @@
    Q (if X > 3 then F else G(1)), (if X > 12 then G(2) else G(3)));
 
 If we used full resolution, this would resolve to Integer because there is no F
-for Float. With the unlimited number of terms available in a conditional expression,
-one can construct ever more complex examples.
+for Float. With the unlimited number of terms available in a conditional
+expression, one can construct ever more complex examples.
 
+Should we eventually find this to be too restrictive, changing to a full resolution
+model would be compatible (it would only make illegal programs legal), whereas
+going in other direction is would be incompatible. So it is best to start with
+the more restrictive rule.
 
+
 We allow the "else" branch to be omitted for boolean-valued conditional
 expressions. This eases the use of conditional expressions in preconditions
 and postconditions, as it provides a very readable form of the "implies"
@@ -212,6 +248,22 @@
     (if A then B)
 In this case, the "else" branch is more noise than information.
 
+
+Conditional_Expressions are static if all of their conditions and expressions
+are static. But expressions that are not used are not evaluated (and thus the
+program is not illegal if one of those expressions would raise an exception).
+This is similar to the rules for short circuit operations.
+
+This means that:
+
+(if False then Some_Constant / 0 else 123) is static (with a value of 123).
+
+but
+
+(if False then Some_Function_Call / 0 else 123) is not static.
+
+[Editor's note: Sorry, Steve. ;-)]
+
 !examples
 
 Another usage is fixing plurals in output. Much Ada code doesn't even try to
@@ -220,10 +272,10 @@
 For instance, we have to write:
 
    if Num_Errors = 1 then
-      Put_Line ("Compilation of " & Source_Name & "completed with" & 
+      Put_Line ("Compilation of " & Source_Name & "completed with" &
                 Error_Count'Image(Num_Errors) & "error detected.");
    else
-      Put_Line ("Compilation of " & Source_Name & "completed with" & 
+      Put_Line ("Compilation of " & Source_Name & "completed with" &
                 Error_Count'Image(Num_Errors) & "errors detected.");
    end if;
 
@@ -231,9 +283,9 @@
 to each message during maintenance.
 
 Using a conditional expression, we can eliminate this duplication:
- 
 
-   Put_Line ("Compilation of " & Source_Name & "completed with" & 
+
+   Put_Line ("Compilation of " & Source_Name & "completed with" &
              Error_Count'Image(Num_Errors) &
              (if Num_Errors = 1 then "error" else "errors")
              & " detected.");
@@ -276,7 +328,7 @@
 "implies then"?  Seems more uniform.
 
 I don't see why anybody would "worry" about user-defined "implies", any more
-than they would worry about user-defined "and".  
+than they would worry about user-defined "and".
 "Implies" on arrays is not terribly useful, but the implementation is trivial,
 so I'd go for uniformity.
 
@@ -285,30 +337,33 @@
 >    I suspect "implies" will be used almost exclusively in Assert
 >    and pre/post conditions.
 
-...which makes any efficiency argument in favor of short-circuits not so important.
+...which makes any efficiency argument in favor of short-circuits not so
+important.
 
-By the way, coding convention at AdaCore is to always use "and then" and "or else",
-and never "and" or "or".  (Well, at least for Booleans -- I suppose we're allowed to
-"and" arrays.)  I don't agree with this policy -- I think the short-circuit forms
-should be used when the meaningfulness of the right-hand side depends on the value
-of the left-hand side, and perhaps for efficiency in some cases.
-
-If I were writing an assertion using "implies" (in my own code, not subject to AdaCore
-rules!), I would normally want non-short-circuit, so that if the right-hand side is
-buggy, it will get evaluated and cause an exception.
-I'd reserve short-circuits for things like "Assert(X /= null implies then X.all > 0);".
+By the way, coding convention at AdaCore is to always use "and then" and "or
+else", and never "and" or "or".  (Well, at least for Booleans -- I suppose we're
+allowed to "and" arrays.)  I don't agree with this policy -- I think the
+short-circuit forms should be used when the meaningfulness of the right-hand
+side depends on the value of the left-hand side, and perhaps for efficiency in
+some cases.
+
+If I were writing an assertion using "implies" (in my own code, not subject to
+AdaCore rules!), I would normally want non-short-circuit, so that if the
+right-hand side is buggy, it will get evaluated and cause an exception. I'd
+reserve short-circuits for things like "Assert(X /= null implies then X.all >
+0);".
 
 Eiffel has "and then", "or else", and "implies", which are short-circuit (called
-"semi-strict").  It also has "and" and "or", which _might_ be short-circuit, depending
-on the whim of the compiler writer -- yuck.
+"semi-strict").  It also has "and" and "or", which _might_ be short-circuit,
+depending on the whim of the compiler writer -- yuck.
 
 ****************************************************************
 
 From: Robert Dewar
 Sent: Thursday, February 26, 2009  3:28 AM
 
-> It rubs me the wrong way to have short-circuit and non-short-circuit 
-> versions of and[then] and or[else], but not for implies.  How about 
+> It rubs me the wrong way to have short-circuit and non-short-circuit
+> versions of and[then] and or[else], but not for implies.  How about
 > "implies" and "implies then"?  Seems more uniform.
 
 This is uniformity run amok. The non-short circuited versions of AND and OR
@@ -317,20 +372,20 @@
 implies :-) In fact you already have the horrible name <=, those who insist
 on the non-short-circuited form can use that name.
 
-> I don't see why anybody would "worry" about user-defined "implies", 
+> I don't see why anybody would "worry" about user-defined "implies",
 > any more than they would worry about user-defined "and".
-> "Implies" on arrays is not terribly useful, but the implementation is 
+> "Implies" on arrays is not terribly useful, but the implementation is
 > trivial, so I'd go for uniformity.
 
 Again, this is uniformity run amok to me, implies on arrays is like NOT on
 non-binary modular types, an unhelpful result of orthogonality likely to
 correspond to a coding error.
 
-> By the way, coding convention at AdaCore is to always use "and then" 
-> and "or else", and never "and" or "or".  (Well, at least for Booleans 
-> -- I suppose we're allowed to "and" arrays.)  I don't agree with this 
-> policy -- I think the short-circuit forms should be used when the 
-> meaningfulness of the right-hand side depends on the value of the 
+> By the way, coding convention at AdaCore is to always use "and then"
+> and "or else", and never "and" or "or".  (Well, at least for Booleans
+> -- I suppose we're allowed to "and" arrays.)  I don't agree with this
+> policy -- I think the short-circuit forms should be used when the
+> meaningfulness of the right-hand side depends on the value of the
 > left-hand side, and perhaps for efficiency in some cases.
 
 Actually the other case where AND/OR are allowed is for plain boolean
@@ -351,8 +406,8 @@
 flight), and then calculate that (False AND True) Is False so you can ignore
 the announcement after all.
 
-> If I were writing an assertion using "implies" (in my own code, not 
-> subject to AdaCore rules!), I would normally want non-short-circuit, 
+> If I were writing an assertion using "implies" (in my own code, not
+> subject to AdaCore rules!), I would normally want non-short-circuit,
 > so that if the right-hand side is buggy, it will get evaluated and cause an
 > exception. I'd reserve short-circuits for things like "Assert(X /= null
 > implies then X.all > 0);".
@@ -361,9 +416,9 @@
 would coutenance the syntax in this implies then" example, it's nothing like
 english usage, whereas "AND THEN" and "OR ELSE" are reasonably in the domain
 of normal english.
- 
-> Eiffel has "and then", "or else", and "implies", which are 
-> short-circuit (called "semi-strict").  It also has "and" and "or", 
+
+> Eiffel has "and then", "or else", and "implies", which are
+> short-circuit (called "semi-strict").  It also has "and" and "or",
 > which _might_ be short-circuit, depending on the whim of the compiler writer -- yuck.
 
 Sounds the right choice to me, Eiffel has it right, and Ada has it wrong, and
@@ -381,84 +436,22 @@
 
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  9:13 AM
-
->>    I suspect "implies" will be used almost exclusively in Assert
->>    and pre/post conditions.
-> 
-> ...which makes any efficiency argument in favor of short-circuits not 
-> so important.
-
-I don't think it is an efficiency argument.  To me, it seems quite clear
-in "A implies B" that if A is False, then you have no reason to evaluate B,
-and my brain would intuitively take advantage of that.  E.g.
-
-    X /= null implies X.Kind = Abc
-
-There seems no particular advantage to having a non-short-circuit version,
-and if you need short-circuiting, as in the above case, you can't get it.
-
-> By the way, coding convention at AdaCore is to always use "and then" 
-> and "or else", and never "and" or "or".  (Well, at least for Booleans 
-> -- I suppose we're allowed to "and" arrays.)  I don't agree with this 
-> policy -- I think the short-circuit forms should be used when the 
-> meaningfulness of the right-hand side depends on the value of the 
-> left-hand side, and perhaps for efficiency in some cases.
-
-I do agree with this convention, but I realize you don't.
-I think in part it depends on what is your first language.
-You were a heavy Pascal user for a while, I believe, and in Pascal, all you
-have are "and" and "or."
-
-To me it is always safer, and frequently more efficient, to use "A and then B."
-Also, in the case when the compiler could convert "A and B" into "A and then B"
-for efficiency, it could go the other way as well.  Hence if I always write
-"A and then B," the compiler will use short-circuiting by default, but if it
-is smart and B is sufficiently simple as to clearly have no side-effects, and
-for some reason "A and B" is more efficient (e.g. it eliminates a branch),
-then the compiler can choose it.  On the other hand, if I use "A and B" always,
-and "B" is at all expensive to compute, then the compiler has to be pretty highly
-optimizing to determine that it can do the short-circuiting, in exactly the
-cases where it is most important to do so.
-
-> If I were writing an assertion using "implies" (in my own code, not 
-> subject to AdaCore rules!), I would normally want non-short-circuit, 
-> so that if the right-hand side is buggy, it will get evaluated and cause an
-> exception. I'd reserve short-circuits for things like "Assert(X /= null implies 
-> then X.all > 0);".
-
-I'm not convinced.  To me "implies" suggests short circuiting quite strongly,
-since if the antecedent is False, the whole thing is uninteresting.  It is an infix
-form for "if A then B" in my mind.
-
-> Eiffel has "and then", "or else", and "implies", which are 
-> short-circuit (called "semi-strict").  It also has "and" and "or", 
-> which _might_ be short-circuit, depending on the whim of the compiler writer -- yuck.
-
-I don't like the last part, but I agree with the first part.
-I think Ada's rules are right, but I choose to think of them as the compiler
-can short-circuit "and"/"or" only if the second operand has no side-effects,
-which is the usual "as if" rules.
- 
-****************************************************************
-
 From: Bob Duff
 Sent: Thursday, February 26, 2009  7:27 AM
 
-> > It rubs me the wrong way to have short-circuit and non-short-circuit 
-> > versions of and[then] and or[else], but not for implies.  How about 
+> > It rubs me the wrong way to have short-circuit and non-short-circuit
+> > versions of and[then] and or[else], but not for implies.  How about
 > > "implies" and "implies then"?  Seems more uniform.
-> 
+>
 > This is uniformity run amok.
 
 Of course -- it's no surprise that someone who never uses "and" would see
 no use in a non-short-circuit version of "implies".
 
->... The non-short circuited versions of AND and  OR are dubious in any 
->case, and "implies then" is plain horrible, if you  must have two 
->different operators, use a horrible name for the non-sc  form of 
->implies :-) In fact you already have the horrible name <=, those  who 
+>... The non-short circuited versions of AND and  OR are dubious in any
+>case, and "implies then" is plain horrible, if you  must have two
+>different operators, use a horrible name for the non-sc  form of
+>implies :-) In fact you already have the horrible name <=, those  who
 >insist on the non-short-circuited form can use that name.
 
 I sometimes write:
@@ -471,13 +464,13 @@
 I can live with that, but I'd prefer to say "implies" instead of
 "<= -- implies".
 
-> > I don't see why anybody would "worry" about user-defined "implies", 
+> > I don't see why anybody would "worry" about user-defined "implies",
 > > any more than they would worry about user-defined "and".
-> > "Implies" on arrays is not terribly useful, but the implementation 
+> > "Implies" on arrays is not terribly useful, but the implementation
 > > is trivial, so I'd go for uniformity.
-> 
-> Again, this is uniformity run amok to me, implies on arrays is like 
-> NOT on non-binary modular types, an unhelpful result of orthogonality 
+>
+> Again, this is uniformity run amok to me, implies on arrays is like
+> NOT on non-binary modular types, an unhelpful result of orthogonality
 > likely to correspond to a coding error.
 
 I doubt it would cause coding errors.  I think "implies" on arrays, like "not"
@@ -486,22 +479,22 @@
 [*] I don't think anybody should use non-binary modular types, with or
 without "not".  ;-)
 
-> > By the way, coding convention at AdaCore is to always use "and then" 
-> > and "or else", and never "and" or "or".  (Well, at least for 
-> > Booleans -- I suppose we're allowed to "and" arrays.)  I don't agree 
-> > with this policy -- I think the short-circuit forms should be used 
-> > when the meaningfulness of the right-hand side depends on the value 
+> > By the way, coding convention at AdaCore is to always use "and then"
+> > and "or else", and never "and" or "or".  (Well, at least for
+> > Booleans -- I suppose we're allowed to "and" arrays.)  I don't agree
+> > with this policy -- I think the short-circuit forms should be used
+> > when the meaningfulness of the right-hand side depends on the value
 > > of the left-hand side, and perhaps for efficiency in some cases.
-> 
-> Actually the other case where AND/OR are allowed is for plain boolean 
+>
+> Actually the other case where AND/OR are allowed is for plain boolean
 > variables. where indeed the operations are more like boolean arithmetic.
-> 
-> The reason I think that Bob's preference is plain horrible is that it 
-> is VERY rare but not impossible to have a situation where you rely on 
+>
+> The reason I think that Bob's preference is plain horrible is that it
+> is VERY rare but not impossible to have a situation where you rely on
 > the
   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-> non-short-circuited semantics, and in such a case you use AND/OR 
-> relying on this. If you use AND/OR routinely, then such rare cases are 
+> non-short-circuited semantics, and in such a case you use AND/OR
+> relying on this. If you use AND/OR routinely, then such rare cases are
 > seriously buried.
 
 Probably the root of our disagreement is that I disagree with your "not
@@ -510,20 +503,20 @@
 cases: (1) I rely on short-circuit semantics ("and then"), (2) I do not
 rely on it ("and").
 
-> In English AND/OR short circuit, if you hear an announcement at an 
-> airport that says "All passengers who are reserved on China Airlines 
-> flight 127 and who have not checked in at the checkin counter should 
+> In English AND/OR short circuit, if you hear an announcement at an
+> airport that says "All passengers who are reserved on China Airlines
+> flight 127 and who have not checked in at the checkin counter should
 > now proceed directly to the gate".
-> 
+>
 > you stop listening at 127.
 
 You had better not -- what if the next word is "or".  ;-)
 
 Your analogy proves that you spend too much time traveling.  ;-)
 
->... You do not carefully evaluate the first  part to False, then the 
->second part to true (because you have checked  in for your flight), and 
->then calculate that (False AND True) Is  False so you can ignore the 
+>... You do not carefully evaluate the first  part to False, then the
+>second part to true (because you have checked  in for your flight), and
+>then calculate that (False AND True) Is  False so you can ignore the
 >announcement after all.
 
 Shrug.  If you say "multiply the number of unicorns in the world by the
@@ -531,15 +524,15 @@
 It doesn't mean that 0 * F(X) should fail to evaluate F(X) in Ada.
 
 ...
-> > Eiffel has "and then", "or else", and "implies", which are 
-> > short-circuit (called "semi-strict").  It also has "and" and "or", 
+> > Eiffel has "and then", "or else", and "implies", which are
+> > short-circuit (called "semi-strict").  It also has "and" and "or",
 > > which _might_ be short-circuit, depending on the whim of the compiler writer -- yuck.
-> 
-> Sounds the right choice to me, Eiffel has it right, and Ada has it 
-> wrong, and Ada will be even wronger if it has "implies then". The nice 
-> thing about the Eiffel choice is that it clearly indicates that AND/OR 
-> are to be used when you don't care about short circuiting, but they 
-> don't imply the inefficiency of forced evaluation, or worse still 
+>
+> Sounds the right choice to me, Eiffel has it right, and Ada has it
+> wrong, and Ada will be even wronger if it has "implies then". The nice
+> thing about the Eiffel choice is that it clearly indicates that AND/OR
+> are to be used when you don't care about short circuiting, but they
+> don't imply the inefficiency of forced evaluation, or worse still
 > cover up a case where the full evaluation is required for correctness.
 
 The problem with the Eiffel rule is that if you _accidentally_ care, you've
@@ -548,11 +541,11 @@
 that you _shouldn't_ care, but bugs do happen, and bugs discovered "later" are
 very costly.
 
-> In Eiffel, I would go for Bob's view of using AND/OR routinely and 
-> reserving AND THEN/OR ELSE for the cases where left to right short 
+> In Eiffel, I would go for Bob's view of using AND/OR routinely and
+> reserving AND THEN/OR ELSE for the cases where left to right short
 > circuiting is required for correctness.
-> 
-> I did not know this feature in Eiffel, definitely the right choice I 
+>
+> I did not know this feature in Eiffel, definitely the right choice I
 > think.
 
 I guess you and I will never agree on this issue.
@@ -562,67 +555,2293 @@
 ****************************************************************
 
 From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+Sent: Thursday, February 26, 2009  9:13 AM
+
+>>    I suspect "implies" will be used almost exclusively in Assert
+>>    and pre/post conditions.
+>
+> ...which makes any efficiency argument in favor of short-circuits not
+> so important.
+
+I don't think it is an efficiency argument.  To me, it seems quite clear
+in "A implies B" that if A is False, then you have no reason to evaluate B,
+and my brain would intuitively take advantage of that.  E.g.
+
+    X /= null implies X.Kind = Abc
+
+There seems no particular advantage to having a non-short-circuit version,
+and if you need short-circuiting, as in the above case, you can't get it.
+
+> By the way, coding convention at AdaCore is to always use "and then"
+> and "or else", and never "and" or "or".  (Well, at least for Booleans
+> -- I suppose we're allowed to "and" arrays.)  I don't agree with this
+> policy -- I think the short-circuit forms should be used when the
+> meaningfulness of the right-hand side depends on the value of the
+> left-hand side, and perhaps for efficiency in some cases.
+
+I do agree with this convention, but I realize you don't.
+I think in part it depends on what is your first language.
+You were a heavy Pascal user for a while, I believe, and in Pascal, all you
+have are "and" and "or."
+
+To me it is always safer, and frequently more efficient, to use "A and then B."
+Also, in the case when the compiler could convert "A and B" into "A and then B"
+for efficiency, it could go the other way as well.  Hence if I always write "A
+and then B," the compiler will use short-circuiting by default, but if it is
+smart and B is sufficiently simple as to clearly have no side-effects, and for
+some reason "A and B" is more efficient (e.g. it eliminates a branch), then the
+compiler can choose it.  On the other hand, if I use "A and B" always, and "B"
+is at all expensive to compute, then the compiler has to be pretty highly
+optimizing to determine that it can do the short-circuiting, in exactly the
+cases where it is most important to do so.
+
+> If I were writing an assertion using "implies" (in my own code, not
+> subject to AdaCore rules!), I would normally want non-short-circuit,
+> so that if the right-hand side is buggy, it will get evaluated and cause an
+> exception. I'd reserve short-circuits for things like "Assert(X /= null implies
+> then X.all > 0);".
+
+I'm not convinced.  To me "implies" suggests short circuiting quite strongly,
+since if the antecedent is False, the whole thing is uninteresting.  It is an
+infix form for "if A then B" in my mind.
 
+> Eiffel has "and then", "or else", and "implies", which are
+> short-circuit (called "semi-strict").  It also has "and" and "or",
+> which _might_ be short-circuit, depending on the whim of the compiler
+> writer -- yuck.
+
+I don't like the last part, but I agree with the first part.
+I think Ada's rules are right, but I choose to think of them as the compiler
+can short-circuit "and"/"or" only if the second operand has no side-effects,
+which is the usual "as if" rules.
+
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+From: Bob Duff
+Sent: Thursday, February 26, 2009 10:53 AM
 
+...
+> I don't think it is an efficiency argument.
+
+And having said that, you proceed to argue based (partly) on efficiency, below.
+;-)
+
+I understand that efficiency is not the entire issue, but it is part of the
+issue. And I think you agree with that.
+
+>...To me,
+> it seems quite clear in "A implies B" that if A is  False, then you
+>have no reason to evaluate B, and  my brain would intuitively take
+>advantage of that.
+
+Of course you think that -- you think the same way about "and[then]".
+Same reason as Robert, with his airport analogy.  Your view is internally
+consistent, but inconsistent with the way Ada is.
+
+>...E.g.
+>
+>     X /= null implies X.Kind = Abc
+>
+> There seems no particular advantage to having a non-short-circuit
+> version, ...
+
+The advantage is that the cases where s-c is needed stand out in the
+code -- readability. There's something "special" or "interesting" about
+the above example (as compared to, say, "X.This = 0 and X.That = 1").
+
+>...and if you need
+> short-circuiting, as in the above case, you can't  get it.
+
+No, my proposal is to provide both s-c and non-s-c, as we do for and[then].
+You and I and Robert all agree there's a need for a s-c version of implication.
+
+...
+> I do agree with this convention, but I realize you don't.
+> I think in part it depends on what is your first language.
+> You were a heavy Pascal user for a while, I believe, and in Pascal,
+> all you have are "and" and "or."
+
+I realize that many programmers think that whatever they learned first is
+"the way things ought to be".  But no, I am immune to that mistake.
+Proof: there are very few things I think Pascal does better than Ada.
+
+Anyway, my first language was Fortran.
+
+The rule in Pascal, which I just looked up, is that the operands of and/or are
+both evaluated, and are evaluated left-to-right -- same as all other operators.
+I'm talking about Jensen and Wirth's "Pascal User Manual and Report". I'm
+ignoring the ISO Pascal standard, because I didn't read it until after I had
+quit using Pascal, and I don't have a copy, and I'm too lazy to google for it.
+
+However, I have used at least one Pascal compiler that did s-c evaluation for
+and/or.  The Pascal culture never cared a lot about obeying standards, and
+anyway J&W's book is too vague to take seriously in that way (although it does
+clearly specify what I said above about and/or).
+
+> To me it is always safer, and frequently more efficient, to use "A and
+> then B."  Also, in the case when the compiler could convert "A and B"
+> into "A and then B" for efficiency, it could go the other way as well.
+> Hence if I always write "A and then B," the compiler will use
+> short-circuiting by default, but if it is smart and B is sufficiently
+> simple as to clearly have no side-effects, and for some reason "A and
+> B" is more efficient (e.g. it eliminates a branch), then the compiler
+> can choose it.  On the other hand, if I use "A and B" always, and "B"
+> is at all expensive to compute, then the compiler has to be pretty
+> highly optimizing to determine that it can do the short-circuiting, in
+> exactly the cases where it is most important to do so.
+>
+> > If I were writing an assertion using "implies" (in my own code, not
+> > subject to AdaCore rules!), I would normally want non-short-circuit,
+> > so that if the right-hand side is buggy, it will get evaluated and cause an exception.
+> > I'd reserve short-circuits for things like "Assert(X /= null implies
+> > then X.all > 0);".
+>
+> I'm not convinced.  To me "implies" suggests short circuiting quite
+> strongly, since if the antecedent is False, the whole thing is
+> uninteresting.
+
+I think you mean "the right-hand side is uninteresting" -- the "whole thing"
+is False, which is perfectly "interesting".
+
+I understand how you can see it that way, but only if you say the same thing
+about "and" -- if the first argument is False, the rest is uninteresting.
+
+...
+> > Eiffel has "and then", "or else", and "implies", which are
+> > short-circuit (called "semi-strict").  It also has "and" and "or",
+> > which _might_ be short-circuit, depending on the whim of the compiler
+> > writer -- yuck.
+>
+> I don't like the last part, but I agree with the first part.
+> I think Ada's rules are right, but I choose to think of them as the
+> compiler can short-circuit "and"/"or" only if the second operand has
+> no side-effects, which is the usual "as if" rules.
+
+The second operand never has important side effects, unless the code is buggy.
+Unfortunately, an Ada compiler can't know that.
+
+Anyway, I don't think I'll ever convince you or Robert, and we haven't heard
+anyone else's opinion.  So I guess I'll quit arguing, for now.
+
+For the record, I can tolerate the language as it is, and I can tolerate a s-c
+"implies", but my preference is still to provide both s-c and non-s-c versions
+of implication.
+
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+From: Randy Brukardt
+Sent: Saturday, March 14, 2009  7:45 PM
+
+>The rule in Pascal, which I just looked up, is that the operands of
+>and/or are both evaluated, and are evaluated left-to-right -- same as
+>all other operators. I'm talking about Jensen and Wirth's "Pascal User
+>Manual and Report".
+>I'm ignoring the ISO Pascal standard, because I didn't read it until
+>after I had quit using Pascal, and I don't have a copy, and I'm too
+>lazy to Google for it.
+
+I have the IEEE Pascal standard (ANSI/IEEE 770X3.97.97-1983) on the shelf
+here (that's on paper, of course). There is nothing special about Boolean
+operators (there are only two sentences).
 
+The overall expression rule is:
+
+    The order of evaluation of the operands of a dyadic operator shall be
+    implementation-dependent.
+
+[Shall be implementation-dependent? That means "must be anything you want",
+which is not much of a requirement! Terrible use of "shall".]
+
+They then follow that up with a note to make sure that everyone knows that
+they didn't specify anything at all:
+
+NOTE: This means, for example, that the operands may be evaluated in textual
+order, or in reverse order, or in parallel or they may not both be evaluated.
+
+So Pascal doesn't specify anything at all. Which probably has nothing to do
+with anything. :-)
+
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+From: Randy Brukardt
+Sent: Thursday, February 26, 2009  1:41 PM
+
+...
+> Anyway, I don't think I'll ever convince you or Robert, and we haven't
+> heard anyone else's opinion.  So I guess I'll quit arguing, for now.
+>
+> For the record, I can tolerate the language as it is, and I can
+> tolerate a s-c "implies", but my preference is still to provide both
+> s-c and non-s-c versions of implication.
+
+Well, you essentially asked for someone else's opinion, so here it is:
+
+I have no idea what logic operation "implies" represents; I have enough trouble
+figuring out whether to use "and" or "or". (I sometimes still have to fall back
+to constructing truth tables, even after 25 years of programming.) So I doubt
+that I would use "implies" at all.
+
+I could be convinced to add it only if doing so was really simple (obviously,
+there are others that would like to use it). Having two versions, an
+overrideable operator, best named "?" or "?" (that's the Unicode single and
+double right-pointing arrows, in case you aren't using a full Unicode font),
+and other cruft does not appear to be simple in my book.
+
+I would probably vote against adding anything that complex (especially as this
+is supposed to be a "modest" update).
 
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+From: Robert I. Eachus
+Sent: Thursday, February 26, 2009  8:39 PM
+
+>[*] I don't think anybody should use non-binary modular types, with or
+>without "not".  ;-)
 
+Well, sooorry about that. They may be esoterica for most people, but they show
+up all over the place in cryptography, hash tables, factoring large numbers,
+random number generators, and radar.  Radar?  Yes, remember the Chinese
+Remainder Theorem?  Pulse Doppler radar works by sending out pulses alternately
+at two (or more) pulse rates which are evenly divisible by two (or more)
+relatively prime numbers. The Chinese Remainder Theorem is then used to
+disambiguate the range information. I'm sure you recognize that the distance to
+another aircraft--or a mountain--is safety critical information.   Having
+support for non-binary moduli in Ada simplifies that code a lot, which makes
+validating it much easier.  Yes, belt and suspenders type checking is done on
+some of machine code.  It is also easier to check the algorithm for correctness,
+then check that the machine code implements the algorithm as written, with
+hardware support for non-binary moduli..
+
+I know it is difficult to implement support for non-binary moduli greater than
+65535 on some hardware, but that is fine.  Most uses of non-binary moduli on
+such systems fit nicely.  For  the number theory and crypto people, even
+(2**1023)-1 can be too small, but we are used to rolling our own when efficient
+bignum arithmetic is needed.
+
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+From: Robert Dewar
+Sent: Friday, February 27, 2009  11:20 AM
+
+> Well, sooorry about that. They may be esoterica for most people, but
+> they show up all over the place in cryptography, hash tables,
+> factoring large numbers, random number generators, and radar.  Radar?
+> Yes, remember the Chinese Remainder Theorem?
+
+You misunderstand Bob entirely, he doesn't think that it is wrong to use modular
+integers with a non-binary modulus in programming, he just thinks the use of the
+Ada language feature is a VERY bad idea, and I strongly agree. I would always
+ban them in any Ada coding standard, and thus insist that people make the mod
+operators explicit, which I think makes code in all these areas much clearer.
+
+As you say there are many applications where such modular types make sense, but
+that does not mean you should use the nasty implicit feature in Ada (especially
+as this is uniquely an Ada oddity).
 
+This is a place where Ada has a seductive feature that sounds great for all
+these kind of applications, but in fact it is a bad idea to use it.
+
+And if anyone uses NOT on such a type, they should be banned from using this
+feature permanently.
+
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+From: Robert I. Eachus
+Sent: Friday, February 27, 2009  2:50 PM
+
+There are two problems with that position.  The first is that the compiler can
+and does use the knowledge that the arguments are both of the same modular type
+in implementing the code.  You want A + B mod M to be implemented as:
+
+C := A + B;
+if C > M
+then C := C-M;
+end if;
+
+You certainly don't want the integer division that will normally be used by the
+compiler if the code is at all time critical.  Also you often can't use (full
+word) binary modular types because overflow silently results in wrong answers.
+Using integer types is better, but you can still get overflows that may have to
+be handled. Using integer types can also result in code paths that cannot be
+reached, and therefore cannot be tested.  This is considered a very bad thing in
+safety critical software. With the (right) non-binary modular type there is no
+possibility of a Constraint_Error, and the code is clean.
+
+The net result is that I have/had (I might have to dig it up) a package that
+implemented modular arithmetic for arbitrary moduli less than 2**32.  The
+problem was that it was originally written for Ada 83, so some of the operations
+use code inserts.  Constants had to be explicitly converted to the private type,
+but other than that, the math is intuitive and what you want to see.   I
+probably should rewrite things to use Ada 9x at least and support moduli up to
+2**63.  Hmm... really nice would be a version that had three versions based on
+the size of the modulus where compilers should do conditional compilation of the
+instances.  (What is the best way to do that?  It would really be nice to write
+the bodies separately, then have the compiler choose the correct one at compile
+time.)
+
+> This is a place where Ada has a seductive feature that sounds great
+> for  all these kind of applications, but in fact it is a bad idea to
+> use it.
+
+Shrug.  I find using the compiler supported types slightly easier than using a
+package.  I think that the way that non-binary moduli are included in the
+language is best, a separate package could be added in the numeric annex, but
+that would probably be more work for compiler vendors not less, and of course,
+it would be more work for programmers.  On the other hand, supporting it in the
+compilers the way it is should result in better code for hash tables, which are
+used quite often in places hidden from the (application) programmer.
+
+> And if anyone uses NOT on such a type, they should be banned from
+> using this feature permanently.
+
+Lol!  I've done the dirty deed, but only to test the package described above
+with the identity:  not A =  - A-1 Incidentally I think that the expression -A-1
+should be written (-A)-1 in this context.  Even so, it is still more misleading
+than not A.
 
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+From: Robert Dewar
+Sent: Friday, February 27, 2009 11:11 AM
 
+> I sometimes write:
+>
+>     pragma Assert (Is_Good (X) <= -- implies
+>                    Is_Gnarly (Y));
+>
+> The comment is necessary.  ;-)
+
+I find this an obscure coding style, with or without the comment, I realy have
+to think about what it means, and would far rather see an equiavlent form with
+NOT/OR/AND which I can easily understand.
+
+> Probably the root of our disagreement is that I disagree with your
+> "not impossible" above -- one should NEVER, EVER write code that
+> relies on non-short-circuited semantics.  Therefore, I only want to
+> distinguish two
+> cases: (1) I rely on short-circuit semantics ("and then"), (2) I do
+> not rely on it ("and").
+
+But people can and do write such code, and the language encourages such a coding
+style by having non-short-circuited forms. Note that if you believe that no one
+should EVER write such code, you should like the nice Eiffel convention, which
+essentially enshrines that principle in the language.
+
+>> In English AND/OR short circuit, if you hear an announcement at an
+>> airport that says "All passengers who are reserved on China Airlines
+>> flight 127 and who have not checked in at the checkin counter should
+>> now proceed directly to the gate".
+>>
+>> you stop listening at 127.
+>
+> You had better not -- what if the next word is "or".  ;-)
+
+Right, OK type, you stop listening at the AND, does not change my argument.
+
+> It doesn't mean that 0 * F(X) should fail to evaluate F(X) in Ada.
+
+A lot of damage to the design of programming languages is done by creating a
+false analogy between arithmetic operators and "boolean operators", they are in
+fact totally different, and it is uniformity going off the rails to force them
+into the same mould.
+
+> The problem with the Eiffel rule is that if you _accidentally_ care,
+> you've got a latent bug that will rear its ugly head when you turn on
+> the optimizer, or switch compilers, or make a seemingly-unrelated code
+> change.  We both agree that you _shouldn't_ care, but bugs do happen,
+> and bugs discovered "later" are very costly.
+
+Yes, but in Ada, you can equally have the bug of requiring the evaluation of the
+right hand side, and it gets covered up by the use of AND/OR. It is a bug if
+code does not mean what it seems to mean. So if you read AND/OR in Ada to never
+mean that the right side needs to be evaluated, you will misunderstand the code
+(and misunderstanding code is just as evil as the code not doing what the writer
+wants, in fact much more evil, because the former affects maintenance, which is
+the expensive part of programming).
+
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+From: Bob Duff
+Sent: Friday, February 27, 2009  6:20 PM
+
+...
+> I find this an obscure coding style, with or without the comment, I
+> realy have to think about what it means, and would far rather see an
+> equiavlent form with NOT/OR/AND which I can easily understand.
+
+OK, I shall refrain from writing that in the future.
 
+...
+> But people can and do write such code, and the language encourages
+> such a coding style by having non-short-circuited forms. Note that if
+> you believe that no one should EVER write such code, you should like
+> the nice Eiffel convention, which essentially enshrines that principle
+> in the language.
+
+Not at all.  We shouldn't write such code.  But we do (by accident).
+A bug 2 years hence is too severe as a punishment for writing such code.
+If we can't detect this sort of error at compile time, it's better to at least
+make the behavior portable across all implementations.
+
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+From: Robert Dewar
+Sent: Friday, February 27, 2009 11:15 AM
 
+The more examples I see of "implies" the more I think this is a horrible
+feature, and I oppose its addition to the language, I think it is a recipe for
+obscure coding by mathematical types who know too much :-)
+
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+From: Randy Brukardt
+Sent: Friday, February 27, 2009 12:30 PM
 
+Since Robert has come out and acknowledged the elephant in the room, let me add
+my voice to his by saying I do not think that this feature belongs in the
+language (especially if it comes at the expense of real conditional expressions
+- these are both "nice to haves", and conditional expressions are far harder to
+write with existing constructs). The fact that it does not have the same meaning
+as it does in English (a point I made privately to Bob yesterday) means that it
+would be confusing to 75% of the programmers out there. While we could avoid
+using it, we'd still have to be able to read it, and thus the confusion would
+continue.
+
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+From: Ben Brosgol
+Sent: Friday, February 27, 2009 12:43 PM
 
+> The more examples I see of "implies" the more I think this is a
+> horrible feature, and I oppose its addition to the language, I think
+> it is a recipe for obscure coding by mathematical types who know too
+> much :-)
+
+I agree.  In English "implies" has connotations of causality or logical
+deduction: "'Socrates is a man' implies 'Socrates is mortal'"; "'It's raining'
+implies 'I'll take an umbrella today'".  This is totally absent in something
+like:
+
+pragma Assert (X /= null implies X.all > 0);
+
+When I first read this, I asked "How could X being non-null imply that X.all is
+positive?"
+
+There is also a subtle type error (in the sense of logical types) with this use
+of "implies".  A construct such as "if then" is an operator within the language
+itself.  You say:
+   "If Socrates is a man, then Socrates is mortal".
+On the other hand "implies" is an operator in the metalanguage used to reason
+about constructs in the language, and quotation marks are necessary.  You do not
+write
+   Socrates is a man implies Socrates is mortal.
+You need to say
+   "Socrates is a man" implies "Socrates is mortal".
+(It's been decades since I last had a course in Symbolic Logic, but for some
+reason the distinction between "if then" and "implies" has pretty much stayed
+with me :-)
+
 ****************************************************************
 
-From: Tucker Taft
-Sent: Thursday, February 26, 2009  4:51 AM
+From: Bob Duff
+Sent: Friday, February 27, 2009  6:08 PM
+
+> The more examples I see of "implies" the more I think this is a
+> horrible feature, and I oppose its addition to the language, I think
+> it is a recipe for obscure coding by mathematical types who know too
+> much :-)
+
+I find your and Randy's arguments convincing.  I'm not exactly a "mathematical
+type", but I accept the fact that lots of folks find "implies" confusing, even
+though I don't understand why.  So let's drop the idea.
+
+****************************************************************
+
+From: Brad Moore
+Sent: Friday, February 27, 2009  8:21 PM
+
+> Anyway, I don't think I'll ever convince you or Robert, and we haven't
+> heard anyone else's opinion.  So I guess I'll quit arguing, for now.
+
+Regarding the use of short circuit operator, my opinion goes both ways,
+depending on who is writing the code.
+
+To me it makes sense that a software vendor such as Adacore would want to
+always use short circuit operators as a coding convention because the code they
+produce is intended for use in a wide variety of applications for a wide variety
+of client code. Some users need high performance tight code, others have needs
+for validation/certification etc. The code written in such an environment should
+consider the needs of all potential clients. In such an environment, the short
+circuit forms probably are a better match for the entire universe of client
+usage.
+
+However, I can see that in a particular clients environment, particularly one
+where performance of language syntax constructs is generally not an issue, a
+coding convention of using short circuit forms only where needed can be a better
+choice for a coding convention. This makes such uses stand out better, and in an
+environment that relies more on informal testing, one can make the case that you
+can get better coverage of the boolean expressions of the conditional statement,
+with non s-c forms.
+
+e.g.
+
+if A > B and Divide_By_Zero(A,B) then
+
+Will generate an error for one pass through the code, whereas and then, might
+not have tested the call to Divide_By_Zero
+
+
+Regarding "implies", A non-sc form is a nice to have but it doesn't bother me
+much if we have to live without the non s-c form. I would prefer not to see the
+non-sc form if it means introducing a syntax that does not read well or is not
+intuitive. "Implies then" doesn't work for me. I do like "implies" for the s-c
+form though.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, February 28, 2009  3:03 AM
+
+> To me it makes sense that a software vendor such as Adacore would want
+> to  always use short circuit operators as a coding convention because
+> the code they produce is intended for use in a wide variety of
+> applications for a wide variety of client code.
+
+Actually that's not a motivation, since we are talking primarily about the
+coding style used internally for tools, so the choice is made on aesthetic
+grounds (basically a viewpoint that non-short-circuiting logical operators are
+fundamentally not a good idea, though I must say the Eiffel convention makes
+good sense to me. I really dislike the idea of being able to write code where
+full evaluation is necessary for functional correctness. Bob says "never write
+code like that", but the language allows it, and any time you have a language
+feature that you feel like saying "never use it", something is wrong.
+
+Probably the most important thing is consistency, and it is a bit unfortunate
+that there are two entirely different consistent coding styles possible here,
+and people can't agree on which they prefer. That means you end up with
+essentially two different languages in this respect, and you have to learn both
+of these languages to be able to read Ada code.
+
+It's like the situation with variant records, where there are two entirely
+different implementation strategies (allocate max, or allocate actual size and
+fiddle with the heap implicitly), again you get two languages, and unfortunately
+compilers only have to implement one of those languages, causing significant
+portability problems (I believe that all the mainstream compilers allocate the
+max now, so that this is not as much of a problem as it might be).
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, February 28, 2009  7:51 PM
+
+> Actually that's not a motivation, since we are talking primarily about
+> the coding style used internally for tools, so the choice is made on
+> aesthetic grounds (basically a viewpoint that non-short-circuiting
+> logical operators are fundamentally not a good idea, though I must say
+> the Eiffel convention makes good sense to me.
+
+I don't understand this attitude at all (re: the Eiffel "compiler-writer's whim"
+rule).  It goes against the entire design of Ada, which is based on the
+assumption that programmers make mistakes, and that the language should try to
+prevent such mistakes (preferably by static checks).  Not by threatening to
+introduce bugs 2 years hence.
+
+After all, it's quite clear from the C standard that you're not supposed to
+index arrays out-of-bounds.  But it happens all the time.
+
+>...I really dislike
+> the idea of being able to write code where full evaluation is
+>necessary for functional correctness.
+
+But you ARE able to write such code in Eiffel.  You depend (by accident) on the
+evaluations and order chosen by your current compiler.  There is no rule in
+Eiffel (or Ada) that prevents that.  Then 2 years later, the code mysteriously
+quits working -- that costs thousands of dollars, each time.
+
+I really think the following language design is better:
+
+    Rule: The operands of "and" are both evaluated, left to right.
+    NOTE: It is considered bad style to depend on the fact that both are
+    evaluated when one is True, or to depend on the order.  Please try not to
+    do that.
+
+>...Bob says "never write code
+> like that", but the language allows it, and any time you have a
+>language feature that you feel like saying "never use it", something
+>is wrong.
+
+Something is indeed wrong, but we don't know how to fix it.  That is, we cannot
+forbid (at compile time) the thing that you and I both agree is evil.  Two
+reasons:
+
+    - Ada doesn't provide enough information to the compiler to so it can know
+      about side effects.  (SPARK is a bit different, here.)
+
+    - Even if the compiler had that info, it's not clear how to formally define
+      what is forbidden.  It's not clear which side effects matter.  Lots of
+      software has the side effect of heating up the CPU chip, but we don't
+      care about that.  We probably don't care about memo-izing functions,
+      which have the side effect of modifying some cache.  We probably don't
+      care in which order two "new" operations are done, even though it can
+      certainly affect the output of the program (e.g. convert to
+      Integer_Address and print it out, for debugging).
+
+> Probably the most important thing is consistency, and it is a bit
+> unfortunate that there are two entirely different consistent coding
+> styles possible here, and people can't agree on which they prefer.
+
+Yes it's unfortunate, but we don't really HAVE to agree.  For example, it's just
+fine that I am forced against my will by AdaCore to write "and then".
+
+> That means you end up with essentially two different languages in this
+> respect, and you have to learn both of these languages to be able to
+> read Ada code.
+
+I agree, that's bad.  But I can't get too excited about it, when I regularly
+have to read those two dialects of Ada, plus programs written in C, Python,
+make, bash, Perl, awk, autoconfjunk, etc etc.  Maybe 100 years from now, people
+will agree on these things (I hope they agree autoconf is junk).
+
+> It's like the situation with variant records, where there are two
+> entirely different implementation strategies (allocate max, or
+> allocate actual size and fiddle with the heap implicitly), again you
+> get two languages, and unfortunately compilers only have to implement
+> one of those languages, causing significant portability problems (I
+> believe that all the mainstream compilers allocate the max now, so
+> that this is not as much of a problem as it might be).
+
+Yes, but not much the language design could do about that, IMHO.
+
+Another (trivial) example is "procedure P(X: Integer);"
+versus "procedure P(X: in Integer);".  Some folks like the "in", others think
+it's just noise.
+
+****************************************************************
+
+From: Brad Moore
+Sent: Friday, February 27, 2009  9:28 PM
+
+The recent arguments against using "implies" have me convinced also.
+I agree that "Implies" should be dropped from the proposed syntax.
+
+****************************************************************
+
+[Here we finally start talking about conditional expressions - ED]
+
+From: Randy Brukardt
+Sent: Thursday, February 26, 2009  2:11 PM
+
+...
+> I'm not convinced.  To me "implies" suggests short circuiting quite
+> strongly, since if the antecedent is False, the whole thing is
+> uninteresting.  It is an infix form for "if A then B"
+> in my mind.
+
+If that's the case, why the heck don't we say that! Ada has needed conditional
+expressions since the beginning of time; I find myself using
+Boolean'Pos(<some-expr>)*<some-other-expr>+Boolean'Pos(not
+<some-expr>)*<some-third-expr> periodically and it is impossible to read and
+potentially buggy to boot.
+
+(if A then B else False) makes more sense for readability than "A implies B"
+because there cannot be a programmer who doesn't know what the first means,
+while the second seems to require a college course in Boolean algebra [and
+actually remembering what was taught there :-)]. (I took Probability instead, it
+sounded more interesting.)
+
+P.S. We had this discussion at dinner Sunday night after most of you left, and
+the four of us that were there all were in favor of conditional expressions.
+
+P.P.S. The hotel elevators still were not fixed when I left Wednesday
+morning (the service elevator thankfully was still working). And they
+cleaned my room Tuesday (only the second time it was done out of 6 nights),
+but they surprised me by leaving new a new shampoo. So I got something out
+of the stay. ;-)
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Thursday, February 26, 2009  2:46 PM
+
+So, the spartan accommodations were conducive to creative thought (and clean
+hair)!   Is there a forthcoming AI on conditional expressions?  I'm all in favor
+of them, but note that (if A then B else false)  is equivalent to (A and B)  not
+to (A implies B) !
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, February 26, 2009  2:55 PM
+
+Sigh. I need more work like a hole in the head, but I'll add it to my list.
+(Unless someone else does it first.)
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Thursday, February 26, 2009  3:05 PM
+
+You mean our undying gratitude is not reward enough?
+
+****************************************************************
 
+From: Randy Brukardt
+Sent: Thursday, February 26, 2009  3:15 PM
+
+Do you think that the credit union will take your undying gratitude for my next
+mortgage payment?? :-)
+
+Perhaps you've hit on the solution to the mortgage crisis!!
+
+****************************************************************
+
+From: Stephen Michell
+Sent: Thursday, February 26, 2009  2:33 PM
+
+Because A implies B is
+   if A then B else True end if
+not .............false
+"implies" is far less error prone.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, February 26, 2009  2:51 PM
+
+Only if you know what it means. And obviously I don't!! And I suspect that 3/4s
+of Ada programmers are like me, not like the people here wanting "implies".
+
+Conditional expressions are far more generally useful (since they can return a
+type other than Boolean), and they will be readable to every Ada programmer (I
+can't imagine anyone being confused by the meaning of "if").
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, February 26, 2009  10:56 AM
+
+> Because A implies B is
+>    if A then B else True end if
+> not .............false
+> "implies" is far less error prone.
+
+I disagree, I find implies to be peculiar, and I certainly have to think about
+what it means, since the else is indeed non intuitive.
+
+A implies B in english means that if A is true then B is true, but there is no
+else in english, the else is an artifact of mathematics.
+
+"If a stronger economy imples better exchange rates, then we should bla bla bla"
+
+Says nothing at all in english about what to do if the economy is weaker ...
+
+****************************************************************
+
+From: Stephen Michell
+Sent: Friday, February 27, 2009  12:39 PM
+
+   if A implies B then...
+Does make sense
+   if A implies B and not A then X
+will always execute X.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, February 26, 2009  5:01 PM
+
+> If that's the case, why the heck don't we say that! Ada has needed
+> conditional expressions since the beginning of time; I find myself
+> using Boolean'Pos(<some-expr>)*<some-other-expr>+Boolean'Pos(not
+> <some-expr>)*<some-third-expr> periodically and it is impossible to
+> read and potentially buggy to boot.
+
+I strongly agree that the Boolean'Pos trick is a horrible hack, though I do it
+when necessary.  Or declare a local function. Or misc other workarounds.
+
+Conditional expressions would be a "nice to have".  Note that they were proposed
+for Ada 9X, and soundly rejected by the reviewers.
+
+> (if A then B else False) makes more sense for readability than "A implies B"
+> because there cannot be a programmer who doesn't know what the first
+> means, while the second seems to require a college course in Boolean
+> algebra [and actually remembering what was taught there :-)]. (I took
+> Probability instead, it sounded more interesting.)
+
+Well, I did take college courses in mathematical logic and modern algebra and so
+forth, and many of the students were puzzled by "implies", so you are probably
+right that many Ada programmers don't understand it.  I am puzzled by their (and
+your) puzzlement -- it means exactly what it means in English.  If I say,
+"swimming in the ocean implies you will get wet", I'm not saying anything about
+what happens if you do not swim in the ocean -- you might get wet or might not
+(maybe it's raining).  Just remember, "falsehood implies anything"; that is,
+"False implies X" is True for all X.
+
+If it makes you feel any better, I was puzzled by Probability and Statistics, a
+grueling (to me) two-semester course.  ;-)
+
+We certainly don't _need_ an implies operator.  As noted before, we already have
+"<= -- implies".  Also, "X implies Y" is equivalent to "(not X) or Y". Use "(not
+X) or else Y" in cases where short-circuit is wanted (some of us think it's
+_always_ wanted).
+
+So:
+
+    pragma Assert (X /= null implies X.all > 0);
+
+is equivalent to:
+
+    pragma Assert (X = null or[else] X.all > 0);
+
+And I guess I find both equally understandable.
+The conditional-expression forms, somewhat less so:
+
+    pragma Assert (if X /= null then X.all > 0 else True);
+    pragma Assert (if X = null then True else X.all > 0);
+
+But it might be nice to say:
+
+    Put_Line (Error_Count'Image(Num_Errors) &
+              (if Num_Errors = 1 then "error" else "errors")
+              & " detected.");
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, February 26, 2009  5:37 PM
+
+...
+> Conditional expressions would be a "nice to have".  Note that they
+> were proposed for Ada 9X, and soundly rejected by the reviewers.
+
+My hazy recollection was that they were dropped from Ada 9x because *all* "nice
+to have" features were dropped from Ada 9x simply because it was getting to be
+too much of a change. That's not the same as "soundly rejected". (Admittedly,
+Tucker snuck several of those "nice to haves" back in, like library-level
+renaming.)
+
+> I am puzzled by their (and your) puzzlement -- it means exactly what
+> it means in English.  If I say, "swimming in the ocean implies you
+> will get wet", I'm not saying anything about what happens if you do
+> not swim in the ocean -- you might get wet or might not (maybe it's
+> raining).  Just remember, "falsehood implies anything"; that is,
+> "False implies X" is True for all X.
+
+The last part is the obvious cause of the problem. It surely *does not* mean
+precisely what it does in English, which you correctly described as "not saying
+anything", that is, *we don't care about this statement* if "swimming in this
+ocean" (call it S) is False (as it was at this meeting :-). That is essentially
+"(if S then W else null)".
+
+But of course a Boolean expression can't represent "don't care", so we
+*arbitrarily* decide that it is "(if S then W else True)". And here we've
+diverged from the English meaning, and that's the part that I (and apparently
+many students) can't remember. It's very much like "or" (and "xor"), which don't
+quite mean the same as in English. So it is best to not make any assumptions at
+all about the English meaning. Thus the difficulties.
+
+> If it makes you feel any better, I was puzzled by Probability and
+Statistics, a grueling (to me) two-semester course.  ;-)
+
+Those were separate one semester classes for me (took them both, in the latter
+was lucky to get the only TA who actually could speak English clearly!).
+Probability is easy: the Firesign Theater approach is best: "Everything you know
+is wrong!!". That is, you can't do math on probabilities in the normal way -- it
+has its own set of rules. The hardest thing is forgetting everything else when
+doing it. (For instance, Bayesian spam filters are likely abusing the name, as
+they violate all of the assumptions of probability theory [there is no way that
+the contents of an e-mail message are independent variables], meaning that you
+can't apply the theory at all. There is no such thing as almost independent!
+Bayesian spam filters undoubtedly do work, but to claim it is because of
+mathematics is completely bogus -- it's just luck and lots of algorithm tuning.)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, February 27, 2009 10:57 AM
+
+> Conditional expressions are far more generally useful (since they can
+> return a type other than Boolean), and they will be readable to every
+> Ada programmer (I can't imagine anyone being confused by the meaning of "if").
+
+Yes, well of course all languages should have conditional expressions, though
+you do have to worry about coercions and typing, and that's not always obvious,
+if the expression is used in other than what Algol-68 would call a strong
+position.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, February 27, 2009  11:02 AM
+
+> Conditional expressions would be a "nice to have".  Note that they
+> were proposed for Ada 9X, and soundly rejected by the reviewers.
+
+But at least part of that rejection was the general attempt to cut down Ada 95
+from what was seen as entirely excessive scope, so good things got thrown out.
+Tuck always said "show me what is bad about XXX and I will remove it." Well the
+problem was not bad XXX's it was too many XXX's. So the fact that something was
+rejected in the Ada 9X process is not a technical argument
+
+> Well, I did take college courses in mathematical logic and modern
+> algebra and so forth, and many of the students were puzzled by
+> "implies", so you are probably right that many Ada programmers don't
+> understand it.  I am puzzled by their (and your) puzzlement -- it
+> means exactly what it means in English.  If I say, "swimming in the
+> ocean implies you will get wet", I'm not saying anything about what
+> happens if you do not swim in the ocean -- you might get wet or might
+> not (maybe it's raining).  Just remember, "falsehood implies anything"; that is,  "False implies X" is True for all X.
+
+And not saying anything about the else means that giving it a meaning is
+artificial.
+
+>     pragma Assert (X /= null implies X.all > 0);
+>
+> is equivalent to:
+>
+>     pragma Assert (X = null or[else] X.all > 0);
+>
+> And I guess I find both equally understandable.
+
+I find the second far superior, I would regard the form using imples as obscure
+programming, because I think most programmers would NOT intuitively understand
+it.
+
+Next you will be wanting NOR and NAND :-)
+
+> But it might be nice to say:
+>
+>     Put_Line (Error_Count'Image(Num_Errors) &
+>               (if Num_Errors = 1 then "error" else "errors")
+>               & " detected.");
+
+Yes, well languages without a conditional expression form are indeed a pain in
+the neck in situations like this :-)
+
 ****************************************************************
 
+From: Jean-Pierre Rosen
+Sent: Friday, February 27, 2009  1:06 AM
+
+>     Put_Line (Error_Count'Image(Num_Errors) &
+>               (if Num_Errors = 1 then "error" else "errors")
+>               & " detected.");
+
+Nice to have - not more.
+My own little utilities libraries has:
+   function Choose
+     (condition: boolean;
+      If_True  : string;
+      If_False : string) return string;
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, February 27, 2009  6:58 PM
+
+Very different, since it forces evaluation, I suggest not calling
+
+    X := Choose (N = 0, 0, 10 / N);
+
+:-)
+
+Now if Ada had special forms like LISP, or proceduring like the original
+Algol-68, before Algol-68 revised, then you could write choose properly (if you
+were LISPY, you would call it cond :-))
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, February 27, 2009  6:01 PM
+
+> Yes, well of course all languages should have conditional expressions,
+> though you do have to worry about coercions and typing, and that's not
+> always obvious, if the expression is used in other than what Algol-68
+> would call a strong position.
+
+I don't know Algol-68 very well, so I don't know what "strong position" means.
+But I don't see a big problem with the types:
+
+    conditional_expression ::= "(" "if" expression "then" expression "else" expression ")"
+
+    The expected type of the first expression is Boolean.  Or some boolean
+    type.
+
+    The expected type of the other two expressions is the expected type of the
+    conditional_expression.
+
+And then all the normal Ada rules about expected type apply.
+Is there a problem?
+
+So in my example:
+
+>     Put_Line (Error_Count'Image(Num_Errors) &
+>               (if Num_Errors = 1 then "error" else "errors")
+>               & " detected.");
+
+Put_Line expects String.  So "&" expects String.  So the expected type for the
+literal "error", is String, so it resolves just fine.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, February 27, 2009  7:07 PM
+
+> Put_Line expects String.  So "&" expects String.  So the expected type
+> for the literal "error", is String, so it resolves just fine.
+
+(if X then 1 else 2.5) + (if Y then 2 else 3.7);
+
+what rule makes this illegal? It needs to be illegal I would think in Ada
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, February 27, 2009  7:27 PM
+
+The above is not a complete context.  In Ada, you need a complete context for
+overload resolution.  Something like:
+
+  Blah : T := (if X then 1 else 2.5) + (if Y then 2 else 3.7);
+
+or:
+
+  Proc((if X then 1 else 2.5) + (if Y then 2 else 3.7));
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, February 27, 2009  8:20 PM
+
+Well if you think there is no problem, fine, but it is clear to me that there is
+a problem here :-) But let's wait and see if conditional expressions attract
+enough support to be worth discussing details.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, February 27, 2009  7:16 PM
+
+> Next you will be wanting NOR and NAND :-)
+
+Not.
+
+;-)
+
+Lisp has all 16 of them, I think.  Or at least all the 10 non-trivial ones.
+
+I asked Bill (15 years old) about "implies" yesterday, and he answered
+correctly.  Maybe it's genetic.  I'm not some sort of math whiz, but Bill and I
+"get" implies.  Strange.
+
+Anyway, I'm not asking for nor, nor nand!
+
+Let's forget about "implies".  That nicely solves the problem of whether it
+should be short-ciruit or not or both.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, February 27, 2009  8:25 PM
+
+> But let's wait and see
+> if conditional expressions attract enough support to be worth
+> discussing details.
+>
+
+Oh let's not.
+Presumably
+      (if False then Some_Function_Call / 0 else 123) would be static.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, February 27, 2009  8:35 PM
+
+> Presumably
+>       (if False then Some_Function_Call / 0 else 123) would be static.
+
+Sigh. We can always count on Steve to think of something to make the AI author's
+job harder. ;-) (I hadn't thought about staticness, but I suspect it should work
+like other short-circuit operations, so I would agree that the above should be
+static.)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, February 27, 2009  8:26 PM
+
+...
+>     The expected type of the other two expressions is the expected
+> type of the
+>     conditional_expression.
+>
+> And then all the normal Ada rules about expected type apply.
+> Is there a problem?
+
+I don't think there is a problem, per se, but I think I'd have to be convinced
+that the complexity is worth it. We've been tending toward not trying to use too
+much information in resolution, because only a compiler could figure out what
+was going on.
+
+Do we really want this to resolve:
+
+     Put ((if Cond then F1 else F2));
+
+with Put overloaded on String and Integer; F1 overloaded on Integer and Float;
+and F2 overloaded on Integer and Boolean? That would work, but do we really want
+people to write code like that?? (Yes, you can do that with "+", but that too
+appears to be a mistake. Why compound it?)
+
+I was thinking that it would resolve like an aggregate (it even looks somewhat
+like one), so that it would have to be qualified unless there was a "single
+type" identified by the context. In this example, that would mean that the
+conditional would have to be qualified:
+
+     Put (Integer'(if Cond then F1 else F2));
+
+It's pretty rare that you have to qualify aggregates, and I would think that the
+same would be true here.
+
+In any case, if we adopt a more restrictive resolution rule now, we could change
+to the less restrictive one later. Going the other way is incompatible.
+
+> So in my example:
+>
+> >     Put_Line (Error_Count'Image(Num_Errors) &
+> >               (if Num_Errors = 1 then "error" else "errors")
+> >               & " detected.");
+>
+> Put_Line expects String.  So "&" expects String.  So the expected type
+> for the literal "error", is String, so it resolves just fine.
+
+Yes, this would work with the rule I suggested as well (at least as long as you
+don't "use Wide_Text_IO" as well).
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, February 27, 2009  9:05 PM
+
+> Sigh. We can always count on Steve to think of something to make the
+> AI author's job harder. ;-)
+
+I think we'd also need wording to define the nominal subtype of one of these
+guys (not that this would be hard).
+
+I'd say keep it simple. You could imagine special rules for the case where, for
+example, the two operands have the same nominal subtype. Let's not.
+
+     Flag : Boolean := ... ;
+     X, Y : Positive:= ... ;
+   begin
+     case (if Flag then X else Y) is
+        when 0 => -- should be legal
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, February 27, 2009  9:34 PM
+
+Never mind.
+This is a case where I'd like the unsend command. A conditional expression is
+not a name, so nominal subtype definition is not an issue.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, February 27, 2009  8:56 PM
+
+> I was thinking that it would resolve like an aggregate...
+
+Yes, that's an even better idea.  Either way, I don't see any "problem".
+
+> > So in my example:
+> >
+> > >     Put_Line (Error_Count'Image(Num_Errors) &
+> > >               (if Num_Errors = 1 then "error" else "errors")
+> > >               & " detected.");
+> >
+> > Put_Line expects String.  So "&" expects String.  So the expected
+> > type for the literal "error", is String, so it resolves just fine.
+>
+> Yes, this would work with the rule I suggested as well (at least as
+> long as you don't "use Wide_Text_IO" as well).
+
+Right.  If you have multiple Put_Line's involved, then it's ambiguous, whichever
+rule we choose.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, February 28, 2009  8:14 AM
+
+Actually, "A implies B" means "if A then B else *True*" while "A and then B"
+means "if A then B else *False*", and "A or else B" means "if A then True else
+B".
+
+I agree that conditional expressions would be valuable, but "implies" has a long
+history in logic, and is well understood by many people who would want to write
+preconditions and postconditions.  The thing that is *not* intuitive is that "A
+implies B" <-> "not A or else B", and forcing people to write the latter is
+unacceptable in my view.  I also feel that "A <= B" is unacceptable if we are
+going to the trouble of adding syntax for pre/postconditions.  Adding "implies"
+as a third kind of short-circuit operation with semantics of "if A then B else
+True" is pretty trivial for the compiler, and will bring us in line with the one
+language that has had "contracts" since its very inception, namely Eiffel.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, February 28, 2009  11:41 AM
+
+I still don't like it, and I don't see what can be possibly hard to understand
+about "not A or else B". It seems *so* must clearer to me than using implies,
+and I don't care what context that is in. All programmers will want to write and
+read preconditions and postconditions, I do not buy the argument that there is
+some trained mathematical subset who will want to write these PPC's, and for
+sure all programmers will have to read them.
+
+To me, this is something that Eiffel got wrong!
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, February 28, 2009  2:35 PM
+
+> Actually, "A implies B" means "if A then B else *True*" while "A and
+> then B" means "if A then B else *False*", and "A or else B" means "if
+> A then True else B".
+
+Right.
+
+> I agree that conditional expressions would be valuable, but "implies"
+> has a long history in logic, and is well understood by many people who
+> would want to write preconditions and postconditions.
+
+True, but we have empirical proof that some folks are confused by "implies".
+
+>...The thing that is *not*
+> intuitive is that "A implies B" <-> "not A or else B",
+
+Strange.  I find that perfectly obvious.  (Except that "logic" has no "or else"
+-- there's no short-circuits involved.  ;-))
+
+Note that the "not" in "not A" often gets folded up into a comparison.
+"not X /= null" is usually written as "X = null".
+And "not X < Y" is "X >= Y".
+
+This discussion has convinced me to use the "or[else]" form in my assertions, to
+better communicate with others, even though I don't really understand why others
+like it better.
+
+> and forcing people to write the latter is unacceptable in my view.  I
+> also feel that "A <= B" is unacceptable if we are going to the trouble
+> of adding syntax for pre/postconditions.
+
+I think both "unacceptable"'s above are hyperbole. Surely "implies", whether s-c
+or not, is a "nice to have" at best.  I've written approx. one zillion pragmas
+Assert in my life, but I guess about 5 of those involve implications.
+
+>...Adding "implies" as a third
+> kind of short-circuit operation with semantics of  "if A then B else
+>True" is pretty trivial for the  compiler,
+
+Yes, trivial to implement.  I don't think anybody disputes that.
+
+>... and will bring us in line with the one  language that has had
+>"contracts" since its very  inception, namely Eiffel.
+
+Shrug.  It's good get ideas from Eiffel, but Eiffel is pretty-much a dead
+language.  Ada is alive (as a niche language, unfortunately).
+
+I used to read comp.lang.eiffel regularly, and my impression is that it was
+killed by compiler vendors being unwilling to support standards and portable
+Eiffel code.  Let that be a lesson to us.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, February 28, 2009  3:03 PM
+
+OK, maybe more than 5.  ;-)  I just did a search in the SofCheck Inspector
+sources, and I see 12.  I'd guess all of them were originally written by me. I
+shall mend my evil ways!
+
+% find . -name '*.ad?' | xargs grep -i '<=.*implies'
+./be/be-pvp-pvp_pass-prop.adb:          pragma Assert(Is_Based_On_Presumptions(VN_Id) <= -- implies
+./be/be-pvp.adb:                        Assert(Is_Precondition(VN_Id) <= -- implies
+./be/be-pvp.adb:                    -- Assert(Is_Precondition(VN_Id) <= -- implies
+./be/be-pvp-scil_extension.adb:            Assert(Is_Present(PV1, VN) <= -- implies
+./be/be-pvp-pvp_pass.adb:                Assert(VN_In_Current_Pass(Cur_Proc, VN) <= -- implies
+./utils/utils-short_int_sets.adb:        pragma Assert(Result <= -- implies
+./utils/utils-command_line.adb:            -- Note that "<=" on Boolean means "implies".
+./utils/utils-storage_management-subpools.adb:    pragma Assert(Protection_Enabled <= -- "<=" means "implies"
+./utils/utils-storage_management-subpools.adb:        pragma Assert(Protection_Enabled <= -- "<=" means "implies"
+./utils/utils-storage_management-subpools.adb:        pragma Assert(Protection_Enabled <= -- "<=" means "implies"
+./utils/utils-storage_management-subpools.adb:        -- Note that "<=" on Boolean means "implies".
+./utils/utils-storage_management-subpools.adb:        -- Note that "<=" on Boolean means "implies".
+
+I'm grepping 1.5 million lines of code here, which includes Inspector plus a lot
+of test code.  12 cases.
+
+Randy and Robert, do you really find the following confusing?
+
+        pragma Assert(Protection_Enabled <= -- "<=" means "implies"
+          (Block.all'Address mod OS_Dep.Page_Size_In_Storage_Elements = 0));
+        pragma Assert(Protection_Enabled <= -- "<=" means "implies"
+                        (Block.all'Size = Page_Size_In_Bits)); null;
+    ...
+    procedure Allocate_Fixed_Block(Pool: in out Subpool'Class) is
+        pragma Assert(Always_Collect <= Collection_Enabled);
+        -- Note that "<=" on Boolean means "implies".
+
+So if protection is enabled, that implies that pages need to be aligned and have
+a certain size.  And if we always collect, that implies that collection is
+currently enabled.  What's so confusing about that?
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, February 28, 2009  8:40 PM
+
+> OK, maybe more than 5.  ;-)  I just did a search in the SofCheck
+> Inspector sources, and I see 12.  I'd guess all of them were
+> originally written by me.
+> I shall mend my evil ways!
+
+We're supposed to change the language for something that occurs once per 100,000
+lines of Ada code?? I surely hope that nothing I've proposed would be used that
+rarely...
+
+...
+> I'm grepping 1.5 million lines of code here, which includes Inspector
+> plus a lot of test code.  12 cases.
+>
+> Randy and Robert, do you really find the following confusing?
+>
+>         pragma Assert(Protection_Enabled <= -- "<=" means "implies"
+>           (Block.all'Address mod OS_Dep.Page_Size_In_Storage_Elements = 0));
+>         pragma Assert(Protection_Enabled <= -- "<=" means "implies"
+>                         (Block.all'Size = Page_Size_In_Bits)); null;
+>     ...
+>     procedure Allocate_Fixed_Block(Pool: in out Subpool'Class) is
+>         pragma Assert(Always_Collect <= Collection_Enabled);
+>         -- Note that "<=" on Boolean means "implies".
+
+I wouldn't say it was "confusing", I would have said "meaningless". If I
+encountered a comment that said "<=" means "implies" before we had this
+discussion, my reaction would have been "WTF??". And then I would have tried to
+figure out the meaning of the expression ignoring the comment.
+
+I may have written something like this once or twice, but I would not have known
+that it actually had a name. (I tend to work from first principles anyway;
+reinventing the wheel is usually faster than figuring out what it is called...)
+
+> So if protection is enabled, that implies that pages need to be
+> aligned and have a certain size.  And if we always collect, that
+> implies that collection is currently enabled.
+> What's so confusing about that?
+
+If you wrote the above in a comment, it would have made sense. But "implies" is
+not something that I would have thought of as a Boolean operator; I have no
+intuition as to what it means exactly. And when reading code, you need to know
+what it means *exactly*, assuming you know is the leading source of undetected
+bugs. (After all, we know what "assume" means: making an ASS out of yoU and ME.
+:-)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, February 28, 2009  9:19 PM
+
+That's not quite realistic.  We aren't writing pre- and post-conditions on every
+subprogram we write yet.  If we were, I suspect "implies" would show up on a
+good proportion of the preconditions or postconditions.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, February 28, 2009  9:50 PM
+
+Why? Just to make the code hard to understand for a majority of readers? It
+surely isn't to save any typing:
+
+   (not A) or else B
+   A implies B
+
+That saves all of 6 characters of typing (and only 4 if you leave out the
+parens, which while not necessary, need to be given for readability -- I cannot
+count the number of times that I thought that "not" covered an entire expression
+rather than a single element). And as Bob notes, most of the time, "not" can be
+folded into the expression A. (That's true in all cases, not just this one --
+explicit "not"s are quite rare in my code.)
+
+But the former expression can be understood by any remotely competent
+programmer. That latter one is meaningless to a significant contingent of
+programmers, and will send then scrambling for a manual or piece of scratch
+paper if they actually have to figure out the result for particular values of A
+and B. So it's primary purpose would be to obfuscate the code - not usually a
+property of Ada code.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, February 28, 2009  10:07 PM
+
+I said:
+> Why? Just to make the code hard to understand for a majority of
+> readers?
+
+As an aside, I should note that complex Boolean expressions are a complete pain
+to write and debug. Any expression containing anything beyond a simple sequence
+of "and then"s or "or else"s is likely to be impossible to understand,
+especially if it needs to be corrected/expanded. (Just trying to remember to
+apply DeMorgans Law makes me break out in hives :-).
+
+Adding "implies" would do absolutely nothing to help this; it would have to be
+combined with some other operator so it would be making Boolean expressions more
+complex without adding anything in expressive power (other than perhaps for the
+chosen few that think in terms of Boolean algebra in their sleep :-).
+
+One thing that I dislike about the
+precondition/postcondition/invariant/user-defined-constraints proposals is that
+we'd have to write a lot more complex Boolean expressions. I can't think of any
+alternative to doing that, so I'm letting that go. But I surely would like to
+see something that would make Boolean expressions more understandable.
+
+I would hope that a conditional expression could have that effect, as you could
+then write an "if" when you meant an "if" rather than having to convert it into
+some bizarre sequence of Boolean operators that don't quite mean the same thing.
+
+P.S. I realized this morning that there is a reasonable way to use the existing
+Janus/Ada intermediate code to generate a conditional expression. Indeed, we do
+that to figure out array lengths in some cases, so I'm pretty confident that the
+optimizer and code generator would not fall over if that technique was used more
+generally. Thus, I suspect the toughest job (based on the 'virtual proposal')
+would be to add the syntax to the grammar generator and remove the inevitable
+conflicts. Probably could have them done tomorrow if the proposal was approved
+tonight.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Sunday, March  1, 2009  2:47 AM
+
+> I used to read comp.lang.eiffel regularly, and my impression is that
+> it was killed by compiler vendors being unwilling to support standards
+> and portable Eiffel code.  Let that be a lesson to us.
+
+I think that's an entirely incorrect analysis, languages do not live or die
+based on such things, the dynamics was that Eiffel never had a significant
+important constituency.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Sunday, March  1, 2009  2:56 AM
+
+> Randy and Robert, do you really find the following confusing?
+>
+>         pragma Assert(Protection_Enabled <= -- "<=" means "implies"
+>           (Block.all'Address mod OS_Dep.Page_Size_In_Storage_Elements = 0));
+>         pragma Assert(Protection_Enabled <= -- "<=" means "implies"
+>                         (Block.all'Size = Page_Size_In_Bits)); null;
+
+Actually it is true indeed that these uses in assertions seem acceptable *if* we
+had an implies keyword (I would NEVER have used the "<=" I agree totally with
+Randy's WTF comment on that :-))
+
+It is in if statements that such things would be confusing
+
+  I would not like to see
+
+      if Protection_Enabled implies ..... then
+
+  I just find that confusing because of the implication of causality
+  in implies. In the assert, it really does read to me as
+
+     if Protection_Enabled then bla bla
+
+  and in the assert context that seems fine, since the else false
+  really is not an issue, but it is in the IF.
+
+  Unfortunately,
+
+     pragma Postcondition (Protection_Enabled implies ...)
+
+  reads more like the IF than the ASSERT to me. I can't explain
+  why this is.
+
+    But the use of (not Protection_Enabled) or else bla bla
+
+  reads perfectly fine in all cases, and even in the Assert it
+  reads probably a bit clearer than the IMPLIES to me.
+
+  If the switch were the other way, then the choice is between
+
+     Protection_Disabled or else blabla
+
+       and
+
+     (not Protection_Disabled) implies bla bla
+
+  Here there is no question that I prefer the first form in
+  all cases by a big margin.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Sunday, March  1, 2009  3:02 AM
+
+> One thing that I dislike about the
+> precondition/postcondition/invariant/user-defined-constraints
+> proposals is that we'd have to write a lot more complex Boolean
+> expressions. I can't think of any alternative to doing that, so I'm
+> letting that go. But I surely would like to see something that would
+> make Boolean expressions more understandable.
+
+> I would hope that a conditional expression could have that effect, as
+> you could then write an "if" when you meant an "if" rather than having
+> to convert it into some bizarre sequence of Boolean operators that
+> don't quite mean the same thing.
+
+Yes I agree, conditional expressions would help
+
+Note that you can still abstract with functions though ...
+
+     function X (A : Integer; B : Float);
+     pragma Precondition (Check_X (A, B));
+
+and later (remember, forward references are allowed)
+
+     function Check_X (A : Integer; B : Float) return Boolean is
+     begin
+        if A > 23 then
+           return False;
+        elsif A > B then
+           return True;
+        ...
+     end Check_X;
+
+It's interesting to note that in the context of MCDC and the Couverture project,
+we discussed the impact of requiring people to abstract complex conditions in
+this way, but there are two objections:
+
+    a) you require more tests, since each test in the Check_X function
+       has to go both ways, and that's more tests than the independence
+       rules of MCDC in a complex expression.
+
+    b) people love complex boolean expressions and insist on filling
+       their code with them, the more complex the better :-(
+
+You can ameliorate the negative impact by putting lots of comments WITHIN the
+complex expression, but people don't seem to like to do this either.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Sunday, March  1, 2009  3:05 AM
+
+Just as a note, the discussion of abstracting complex PPC conditions into
+functions shows why the forward reference allowed for PPC is highly desirable.
+
+Languages like Pascal and Ada with their normal disallowance of forward
+references (in contrast to languages like Algol, COBOL, and PL/1) make it much
+more unpleasant to abstract in this way, since it is unnatural to write local
+abstractions BEFORE the use .. you get top down structure written bottom-side
+up, which has to be read backwards.
+
+At least we alleviate this for PPC's and that's very helpful.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, March  5, 2009  11:26 AM
+
+I would like to make another pitch for the importance of providing an operation
+that corresponds to what is typically labeled "implies," particularly in the
+context of adding support for explicit pre- and postconditions.  The discussion
+seems to have gotten a bit sidetracked... ;-)
+
+One thing that arises from previous responses is that the word "implies" does
+not always convey the right idea, so I have a suggestion for an alternative,
+which happens to dovetail with the interest in more general conditional
+expressions.
+
+The real need for this comes about in assertions, constraints, preconditions,
+postconditions, etc., which are in some sense "conditional."  The typical
+situation is something like this:
+
+    procedure Add_To_Fruit_Salad(
+      Fruit : in out Fruit_Type; Bowl : in out Bowl_Type) is
+    begin
+        -- Check if ready to add to fruit salad
+        case Fruit.Kind is
+          when Apple =>
+            pragma Assert(Fruit.Is_Crisp);
+            null;
+          when Banana =>
+            pragma Assert(Fruit.Is_Peeled);
+            null;
+          when Pineapple =>
+            pragma Assert(Fruit.Is_Cored);
+            null;
+          when others => null;
+        end case;
+        Cut_Up(Fruit);
+        Add_To_Bowl(Fruit, Bowl);
+    end Add_To_Fruit_Salad;
+
+How do we "hoist" these assertions up to the beginning of the subprogram, so
+they can become preconditions? What we would like to write is something like:
+
+    procedure Add_To_Fruit_Salad(
+      Fruit : in out Fruit_Type; Bowl : in out Bowl_Type)
+      with
+        Pre =>
+            Fruit.Kind = Apple then Fruit.Is_Crisp
+          elsif
+            Fruit.Kind = Banana then Fruit.Is_Peeled
+          elsif
+            Fruit.Kind = Pineapple then Fruit.Is_Cored,
+
+        Post =>
+           Is_In_Bowl(Fruit, Bowl);
+
+The general problem is that to write a precondition, you need to express the
+requirements for a subprogram at the point of call, rather than at some
+intermediate point in the subprogram's control flow.  Similarly, for a
+postcondition, you need to express the guaranteed results after the call, not
+just what is true at one particular "return" statement in a subprogram with
+multiple return statements.
+
+In other words, you would like to hoist what were assertions at intermediate
+points in the subprogram into being either "preconditions" or "postconditions,"
+as appropriate.   In our static analysis tool, one of the things it does is
+automatically "extract" pre- and postconditions from the code itself.  This is
+of course a bit of a "cheat" as far as the appropriate order of doing things,
+but it serves two purposes. One it helps document what the code *really* does,
+and it can provide a starting point for human-written pre- and postconditions.
+This tool is very frequently trying to hoist run-time checks into being
+preconditions. Checks like "X /= null" or "I in 1..10" can naturally become
+preconditions. But unfortunately, it is quite common if these requirements only
+exist on some, but not all of the paths through the subprogram.
+
+As in the example, imagine a subprogram that begins with a case statement on the
+kind of an object, and then performs actions appropriate to the kind. In an
+object-oriented worlds, one might call a dispatching operation, but that is the
+moral equivalent of a case statement at run-time, based on the tag.  The fact is
+there may be requirements on the caller that depend on the kind of object.  Our
+tool ends up hoisting these kinds of requirements into preconditions anyway, but
+we mark them as "(soft)" to indicate that they don't really apply to all paths
+through the subprogram.  Of course in some cases one could go ahead and always
+impose the requirement on the caller, presuming that they shouldn't be worried
+about the details of the object. On the other hand, there are cases where,
+typically for a variant record or a tagged-type hierarchy, the component of the
+object participating in the reqiurement exists only for some, but not all kinds
+of objects. In these cases, we can't real impose the requirement as a "hard"
+precondition on all callers.  What we really want to do is change our "soft"
+preconditions into "hard" preconditions using an equivalent of an "if
+<condition> then <precondition>."  In the above example syntax, we have dropped
+the "if" as that seems to be very tightly linked to the notion of a "statement"
+in Ada, but we retain the "then" as that seems to convey nicely the conditional
+aspect of the precondition.
+
+As perhaps can be guessed at this point, what this leads me to suggest is that
+we adopt a syntax for conditional_expression according to:
+
+   conditional_expression ::=
+        <condition> THEN <expression>
+          {ELSIF <condition> THEN <expression>}
+          [ELSE <expression>]
+
+In general, conditional_expression would only be permitted in a limited number
+of contexts.  In particular, inside parentheses, after a "=> in the proposed
+aspect specification syntax, and more generally as an operand inside a construct
+using parentheses, such as an aggregate, function call, pragma, discriminant
+constraint, etc.  The "ELSE <expression>" would be optional only for a boolean
+conditional expression, as used in an assertion, constraint, precondition,
+postcondition, etc., with the implied semantics being "ELSE True."  This special
+case provides the conditional assertion capability that is quite important in
+some cases for expressing preconditions and postconditions.
+
+Here are uses of the proposed conditional_expression:
+
+
+    Text_Length : constant Natural :=
+      (Text /= null then Text'Length else 0);
+
+    Hash_Is_Ok : constant Boolean :=
+      (Key(X) = Key(Y) then Hash(X) = Hash(Y));
+
+    ...
+
+    Ada.Assertions.Assert(
+     Obj.Name /= null then Is_Alphabetic(Obj.Name.all),
+      "Name, if any, must be alphabetic");
+
+    Put(Console, Str => Prompt /= null then Prompt.all else ">");
+
+    return (Size(X) >= Size(Y) then X else Y);
+
+
+Note that even without allowing a conditional_expression in normal code, you
+would probably often need one to express useful postconditions:
+
+    function Max(X, Y : T) return T
+      with
+        Post =>
+          Max'Result = (Size(X) >= Size(Y) then X else Y);
+
+If one is going to be seeing such things in postconditions, it would be
+frustrating to disallow them in normal code.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, March  5, 2009  1:56 PM
+
+>    conditional_expression ::=
+>         <condition> THEN <expression>
+>           {ELSIF <condition> THEN <expression>}
+>           [ELSE <expression>]
+
+OK, but I essentially proposed that a week ago. Where the heck have you been?
+The only difference here is "elsif" clause, and I had already put that into the
+proposal I'm writing. I realized the need for the "Elsif" the first time I tried
+to use one of these in an example.
+
+The main difference here is that you left out the parens. And the optional Else.
+
+> In general, conditional_expression would only be permitted in a
+> limited number of contexts.
+
+I don't see why. Just *always* parenthesize it, resolve it like an aggregate,
+and there is no conflict with other syntax. Trying to  allow the saving of the
+typing of *two* characters is silly to me, it makes the resolution and parsing
+much harder. (Expression parsing would have to be context-sensitive, which is a
+non-starter with me.)
+
+It would be more important to avoid the parens if we were only going to use
+pragmas for preconditions, but since we're going with syntax, there is no
+advantage at all - IMHO.
+
+> The "ELSE
+> <expression>" would be optional only for a boolean conditional
+> expression, as used in an assertion, constraint, precondition,
+> postcondition, etc., with the implied semantics being "ELSE True."
+> This special case provides the conditional assertion capability that
+> is quite important in some cases for expressing preconditions and
+> postconditions.
+
+I could live with this idea, although it seems unnecessary to me. If you want
+"Else True", you really ought to say so.
+
+...
+> Note that even without allowing a conditional_expression in normal
+> code, you would probably often need one to express useful
+> postconditions:
+>
+>     function Max(X, Y : T) return T
+>       with
+>         Post =>
+>           Max'Result = (Size(X) >= Size(Y) then X else Y);
+>
+> If one is going to be seeing such things in postconditions, it would
+> be frustrating to disallow them in normal code.
+
+Surely. I don't see any reason for these things to be special. But no one has
+ever proposed that. Why the straw man??
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Thursday, March  5, 2009  2:44 PM
+
+> I don't see why. Just *always* parenthesize it, resolve it like an
+> aggregate, and there is no conflict with other syntax. Trying to
+> allow the saving of the typing of *two* characters is silly to me, it
+> makes the resolution and parsing much harder. (Expression parsing
+> would have to be context-sensitive, which is a non-starter with me.)
+
+I agree the parens should always be there (I suppose it would be too radical to allow the nice Algol-68 short syntax
+
+(condition | expression | expression) :-)
+>
+> It would be more important to avoid the parens if we were only going
+> to use pragmas for preconditions, but since we're going with syntax,
+> there is no advantage at all - IMHO.
+
+resolve like an aggregate seems dubious to me
+
+doesn't that mean that if you write
+
+   (if X > 3 then 2 else 4) + (if X > 12 then 13 else 14)
+
+is ambiguous?
+
+> I could live with this idea, although it seems unnecessary to me. If
+> you want "Else True", you really ought to say so.
+
+I agree
+
+> Surely. I don't see any reason for these things to be special. But no
+> one has ever proposed that. Why the straw man??
+
+because there was a suggestion of implies being allowed only in PPC's.
+Note that this kind of thing happens in SPARK annotations, where there e.g. you
+can write quantifiers.
+
+And while we are at it, if we are talking useful stuff in PPC's, how about
+adding quantifiers while we are at it
+
+    (for all X in Sint => Sqrt (X) < 23)
+
+or something like that ...
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Thursday, March  5, 2009  2:51 PM
+
+>> It would be more important to avoid the parens if we were only going
+>> to use pragmas for preconditions, but since we're going with syntax,
+>> there is no advantage at all - IMHO.
+>
+> resolve like an aggregate seems dubious to me
+>
+> doesn't that mean that if you write
+>
+>  (if X > 3 then 2 else 4) + (if X > 12 then 13 else 14)
+>
+> is ambiguous?
+
+No, this is not a complete context, there is some expected type that both of
+these have to have
+
+> And while we are at it, if we are talking useful stuff in PPC's, how
+> about adding quantifiers while we are at it
+>
+>   (for all X in Sint => Sqrt (X) < 23)
+>
+> or something like that ...
+
+
+Would mesh nicely with  some new iterator forms, of course...  There
+is no concern here that the iteration might not finish.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Thursday, March  5, 2009  2:58 PM
+
+...
+> No, this is not a complete context, there is some expected type that
+> both of these have to have
+
+sorry not quite the right example, here is a more complete example
+
+    procedure q (a, b : Integer);
+    procedure q (a, b : float);
+
+    q ((if X > 3 then 2 else 4), (if X > 12 then 13 else 14))
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, March  5, 2009  3:17 PM
+
+...
+> sorry not quite the right example, here is a more complete example
+>
+>     procedure q (a, b : Integer);
+>     procedure q (a, b : float);
+>
+>     q ((if X > 3 then 2 else 4), (if X > 12 then 13 else 14))
+
+My thinking was that you don't want this to resolve without some qualification,
+anymore than you want an aggregate to do so. The problem is that there is an
+potentially infinite number of expressions that could control the resolution,
+and at some point that gets more confusing than helpful. Qualifying one of the
+conditionals doesn't seem that bad:
+
+     q (Integer'(if X > 3 then 2 else 4), (if X > 12 then 13 else 14))
+
+To see the problem, imagine that you have the following declarations:
+
+     function F return Integer;
+     function F return Boolean;
+
+     function G (N : Natural) return Integer;
+     function G (N : Natural) return Float;
+
+     Q (if X > 3 then F else G(1)), (if X > 12 then G(2) else G(3)));
+
+This resolves to Integer because there is no F for Float. Do we really want
+something this confusing to work? (BTW, I really think this sort of rule should
+be applicable to *all* Ada subexpressions, because it requires qualification on
+the confusing ones and allows the obvious ones to resolve. It is a much better
+rule than the one that allows unlimited overloading on results that we currently
+use -- but sadly, too incompatible. Of course, you can't qualify functions that
+return anonymous access types, another reason to avoid them... :-)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Thursday, March  5, 2009  3:24 PM
+
+OK, well you really state yourself the reason I don't like having to qualify in
+this situation, it's not Ada! You wish it were, but it isn't!
+
+Algol-68 has this all worked out very clearly and consistently, but retrofitting
+it into Ada may require some kludges (like the qualification in Randy's example,
+which to me is an obvious kludge).
+
+other things to worry about are staticness, etc
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, March  5, 2009  5:44 PM
+
+> My thinking was that you don't want this to resolve without some
+> qualification, anymore than you want an aggregate to do so.
+
+I agree with Randy.  Allowing this to resolve adds implementation work, for
+negative user benefit.  The analogy with aggregates is apt -- you have to know
+the type before looking inside.
+
+If you erase the second q, then the expected type is Integer for both of those,
+and it resolves just fine.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Thursday, March  5, 2009  7:12 PM
+
+I find it really ugly that you cannot replace 1 by (True|1|1) in any context,
+most certainly we regarded that as essential in the A68 design.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, March  5, 2009  5:44 PM
+
+> I agree the parens should always be there (I suppose it would be too
+> radical to allow the nice Algol-68 short syntax
+>
+> (condition | expression | expression) :-)
+
+Yes, too radical.  ;-)
+
+Anyway, how would you extend that to allow "elsif"?
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Thursday, March  5, 2009  7:14 PM
+
+> Yes, too radical.  ;-)
+>
+> Anyway, how would you extend that to allow "elsif"?
+
+A68 uses
+
+   (condition | expr | expr |: expr | expr ....)
+
+if I remember right, it's a long time ago ...
+
+of course what I call here expr in A68 is actually a serial clause, so you can
+write
+
+   (X > 3 | int a; a := 4*b*c; a*a | 0)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, March  5, 2009  5:55 PM
+
+> What we would like to write is something like:
+>
+>     procedure Add_To_Fruit_Salad(
+>       Fruit : in out Fruit_Type; Bowl : in out Bowl_Type)
+>       with
+>         Pre =>
+>             Fruit.Kind = Apple then Fruit.Is_Crisp
+>           elsif
+>             Fruit.Kind = Banana then Fruit.Is_Peeled
+>           elsif
+>             Fruit.Kind = Pineapple then Fruit.Is_Cored,
+>
+>         Post =>
+>            Is_In_Bowl(Fruit, Bowl);
+
+I like this, except I really dislike leaving off the "if".
+That really harms readability, to me.
+
+I like the fact that you can leave off the parens in certain places where they
+are not needed.
+
+I like the fact that "else True" is optional, but I can live without that if
+others find it confusing.
+
+One thing you lose in the above transformation is the full coverage checking of
+case statements, which is one of my favorite features of Ada.  (Get rid of the
+naughty "when others => null;" above.)  Can I have some form of conditional
+expression that starts with "case", and has full coverage rules?  When
+applicable, it's much safer than elsif chains.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Sunday, March  8, 2009  1:21 AM
+
+> OK, but I essentially proposed that a week ago. Where the heck have
+> you been? The only difference here is "elsif" clause, and I had
+> already put that into the proposal I'm writing. I realized the need
+> for the "Elsif" the first time I tried to use one of these in an example.
+
+I'd rather have:
+    when <condition> => <expression>
+
+(I proposed something like that for the pragma version, but my message seems to
+have vanished in the haze)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Sunday, March  8, 2009  4:19 AM
+
+I find it peculiar (given expectations from other languages) to have such a
+variation between the syntax for conditional statements and conditional
+expressions. For my taste I would prefer they be totally unified as in any
+reasonable expression language, but given we have inherited the Pascal tradition
+of making a big difference between statements and expressins, let's at least
+keep the syntax parallel (as we do in the case of function vs procedure calls
+for example).
+
+It would be reasnable to have a case expression as well, something like
+
+   (case x is when bla => expr, bla => expr, bla => expr)
+
+but reusing when in this odd way which is at odds with the syntax of case, for
+an if expression seems odd to me.
+
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, March  9, 2009  2:0 PM
+
+...
+> I'd rather have:
+>     when <condition> => <expression>
+>
+> (I proposed something like that for the pragma version, but my message
+> seems to have vanished in the haze)
+
+I can't tell whether you mean for the conditions to be evaluated independently
+when there are many or sequentially. (Or even if you are allowing many.
+
+If sequentially, the syntax implies an independence between the conditions that
+does not exist. (Case statement conditions use "when" and they are independent;
+exits use "when" and they are independent.) "elsif" makes it clear that it
+*follows* the previous condition.
+
+If independent, then there is no way to handle "else" without repeating the
+inverse of the condition, which is obviously error-prone.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Monday, March  9, 2009  6:04 AM
+
+> I find it peculiar (given expectations from other languages) to have
+> such a variation between the syntax for conditional statements and
+> conditional expressions. For my taste I would prefer they be totally
+> unified as in any reasonable expression language, but given we have
+> inherited the Pascal tradition of making a big difference between
+> statements and expressins, let's at least keep the syntax parallel (as
+> we do in the case of function vs procedure calls for example).
+
+This is not intended as a replacement for general "if expression", rather as a
+replacement for "implies". I was specifically addressing Tuck's proposal for
+Pre/Post conditions.
+
+> I can't tell whether you mean for the conditions to be evaluated
+> independently when there are many or sequentially. (Or even if you are
+> allowing many.)
+
+Let's make it clearer. Here is what I suggest:
+From Tuck:
+<declaration>
+    WITH
+      <aspect_name> [=> <aspect_value>],
+      <aspect_name> [=> <aspect_value>],
+      ... ;
+
+My suggestion:
+<aspect_value> ::= pre | post | invariant {<assertion>}
+
+<assertion> ::= {[<guard>] <boolean expression>}
+<guard> ::= when <condition> =>
+
+All, and only, <boolean expression> corresponding to True <guard>s are evaluated
+and should return true. No guard is the same as "when True".
+
+This is more like guards in select or protected entries than case statements. I
+think the intent would be clearer than conditional expressions (and certainly
+clearer than "implies").
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, March  9, 2009  10:27 AM
+
+I am unclear what your BNF means.  "pre", "post", etc were intended to be aspect
+*names*, not aspect values. Also, the aspect value for "pre" might be several
+boolean expressions connected by "and", and each boolean expression might need a
+different "guard."  Also, we would like these to be usable in other contexts
+where boolean expressions are used, such as in calling the "Assert" procedure
+declared in Ada.Assertions, or in the pragma Assert, or in declaring a boolean
+constant such as "Is_Ok", etc. So I don't think we want a syntax that only works
+in the context of the "aspect_name => aspect_clause" syntax.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Monday, March  9, 2009  11:08 AM
+
+> I am unclear what your BNF means.  "pre", "post", etc were intended to
+> be aspect *names*, not aspect values.
+
+Sorry, my confusion. Should have been:
+<aspect_value> ::= {<assertion>}
+<assertion> ::= [<guard>] <boolean expression>
+<guard> ::= when <condition> =>
+
+> Also, the aspect value for "pre" might be several boolean expressions
+> connected by "and", and each boolean expression might need a different
+> "guard."
+
+The (corrected) proposed syntax allow several <assertion>, with possibly
+different guards. I think it is much clearer than packing everything in a single
+expression: f.e: X is null iff Y = 0
+
+pre =>
+   when X = null => Y = 0;
+   when Y = 0    => X = null;
+
+compared to:
+pre =>
+   (if x = null then y = 0 else y /= 0)
+
+> Also, we would like these
+> to be usable in other contexts where boolean expressions are used,
+> such as in calling the "Assert" procedure declared in Ada.Assertions,
+> or in the pragma Assert,
+
+We could also have:
+   pragma Assert(
+     [Check =>] boolean_expression
+     [, When => boolean_expression]
+     , [Message =>] string_expression);
+
+> or in declaring a boolean constant such as "Is_Ok", etc.
+> So I don't think we want a syntax that only works in the context of
+> the "aspect_name => aspect_clause" syntax.
+
+It would not preclude the "if expression" in the general case, but I think it
+would read nicely for assertions. And it's only syntax, I don't think it would
+be a big deal for the compiler. So it's mainly a matter of taste.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, March  9, 2009  11:20 AM
+
+> I am unclear what your BNF means.  "pre", "post", etc were intended to
+> be aspect *names*, not aspect values.
+> Also, the aspect value for "pre" might be several boolean expressions
+> connected by "and", and each boolean expression might need a different
+> "guard."  Also, we would like these to be usable in other contexts
+> where boolean expressions are used, such as in calling the "Assert"
+> procedure declared in Ada.Assertions, or in the pragma Assert, or in
+> declaring a boolean constant such as "Is_Ok", etc.
+> So I don't think we want a syntax that only works in the context of
+> the "aspect_name => aspect_clause" syntax.
+
+I agree with Tucker.  And if we're going to have a general-purpose conditional
+expression, I don't see any need for the proposed "when" syntax.  Nothing wrong
+with it, I suppose, but we just don't need gratuitous extra syntax.
+
+Let's restrict Ada 2012 features to what's really needed/useful.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March  9, 2009  3:09 PM
+
+...
+> The (corrected) proposed syntax allow several <assertion>, with
+> possibly different guards. I think it is much clearer than packing
+> everything in a single expression:
+> f.e: X is null iff Y = 0
+>
+> pre =>
+>    when X = null => Y = 0;
+>    when Y = 0    => X = null;
+>
+> compared to:
+> pre =>
+>    (if x = null then y = 0 else y /= 0)
+
+Perhaps it's this flu bug that I have, but I don't have the foggiest idea what
+the first expression is supposed to mean -- it surely does not appear equivalent
+to the second. The second one is crystal clear.
+
+Moral: If you don't understand the logical "implies", that confusion is not
+going to go away by dressing it up in some other syntax. If you don't understand
+"if", you aren't a programmer, so let's stick to the universal.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Tuesday, March  9, 2009  5:18 AM
+
+> Perhaps it's this flu bug that I have, but I don't have the foggiest
+> idea what the first expression is supposed to mean -- it surely does
+> not appear equivalent to the second. The second one is crystal clear.
+
+Well, it means that when X is null, Y should be equal to 0, and
+(conversely) when Y is equal to 0, X should be null.
+
+I found that notation nice-looking, and in line with the notion of assertions
+that are applicable only under some conditions; but if others don't support the
+idea, I won't insist on that (it's only syntactic sugar after all).
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, March 14, 2009  9:48 PM
+
+In the interests of making myself more work that I may never get paid for,
+below find a *complete* write-up for conditional expressions. This includes
+wording for everything that has previously been discussed. (This is version /02
+since I made extensive changes today while filing the mail, including
+borrowing several nice examples.)
+
+I included Tucker's optional else part, as I figured it was easier to delete
+the wording if we decide to remove that option than to add it at a meeting.
+
+I stuck with the model that these are much like a aggregate, thus I inserted
+them into the syntax in the same places.
+
+I've left "case expressions" and "loop expressions" (or "quantifiers", whatever
+the heck that is) for someone else to write up. I'd suggest using a similar
+model for them, at least syntactically.
+
+All comments welcome.
+
+****************************************************************

Questions? Ask the ACAA Technical Agent