Version 1.3 of ai05s/ai05-0147-1.txt

Unformatted version of ai05s/ai05-0147-1.txt version 1.3
Other versions for file ai05s/ai05-0147-1.txt

!standard 4.4 (07)          09-06-27 AI05-0147-1/03
!standard 4.5.7 (0)
!standard 4.7(2)
!standard 4.7(3)
!standard 4.7(5)
!standard 4.9(12)
!standard 4.9(33)
!class amendment 09-03-13
!status work item 09-03-13
!priority Medium
!difficulty Medium
!subject Conditional expressions
!summary
!problem
It is not unusual that an expression value needs to be calculated in a way that avoids an exception or other boundary. For instance, consider declaring a range based on a parameter:
procedure P (N : in Natural) is subtype Calculation_Range is Natural range 0 .. (10_000 / N) + 1; begin
This obviously doesn't work if N is 0. One might want to use the maximum value in this case, but such an expression is hard to write in Ada.
One common workaround for the lack of conditional expressions in Ada is to multiply by Boolean'Pos:
procedure P (N : in Natural) is subtype Calculation_Range is Natural range 0 .. (Boolean'Pos(N=0) * 10_000 + Boolean'Pos(N/=0)*(10_000 / N)) + 1; begin
But this doesn't work because the entire expression will be evaluated even when N is 0, including the divide-by-zero.
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 .. (if N=0 then 10_000 else 10_000 / N) + 1;
The pending addition of preconditions to Ada will greatly increase this need. It is not at all unusual to have the value of one parameter depend on another. It is possible to write a Boolean expression like
Precondition => (not Param_1 >= 0) or Param_2 /= ""
but this sacrifices a lot of readability, when what is actually meant is
Precondition => (if Param_1 >= 0 then Param_2 /= "" else True)
Another situation is renaming an object determined at runtime:
procedure S (A, B : Some_Type) is Working_Object : Some_Type renames (if Some_Func(A) then A else B); begin -- Use Working_Object in a large chunk of code. end S;
In Ada currently, you would have to either duplicate the working code (a bad idea if it is large) or make the working code into a subprogram (which adds overhead, and would complicate the use of exit and return control structures).
for all of these reasons, we are proposing to add conditional expressions to Ada.
!proposal
(See wording.)
!wording
primary ::= numeric_literal | null | string_literal | aggregate | name | allocator | (expression) | conditional_expression
4.5.7 Conditional expressions
Syntax
conditional_expression ::= (if condition then *dependent*_expression {elsif condition then *dependent*_expression} [else *dependent*_expression])
Name Resolution Rules
The expected type for a conditional_expression shall be a single type. The expected type for each dependent_expression of a conditional_expression shall be the type of the conditional_expression. Redundant[The expected type for each condition is expected to be of any boolean type (see 5.3).]
[Editor's Note: "condition" is defined in 5.3. Should it (both syntax and semantics - 2 lines) be moved here to avoid the forward reference??]
Legality Rules
If there is no "else" dependent_expression, the type of conditional_expression shall be of a boolean type.
Dynamic Semantics
For the execution of a conditional expression, the condition specified after if, and any conditions specified after elsif, are evaluated in succession (treating a final else as elsif True then), until one evaluates to True or all conditions are evaluated and yield False. If a condition evaluates to True, the associated dependent_expression is evaluated and its value is the value of the expression. Otherwise, the value of the expression is True.
[Editor's note: This is nearly a copy of 5.3(5). I left the clunkyness intact. Note that the last otherwise can be true only for a boolean conditional expression, as an "else" is required in all other cases.]
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...
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.
* A conditional_expression all of whose conditions and dependent_expressions are
static expressions;
Split 4.9(33), replacing it by the following:
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 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:
[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.]
** TBD: We need wording to deal with built-in-place issues. In particular, a conditional expression ought to work like a set of parens rather than an aggregate with one component: no temporary object would be created (even logically).
** TBD: We also need to deal with the case that the various results have mixed tagged states: if one result is statically tagged and another is dynamically tagged, and the whole is used as the argument of a non-dispatching call, probably we need something to be illegal (we wouldn't want this to be a way to avoid 3.9.2(8-9)). [Well, I might, but that's a different issue. ;-)]
!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:
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 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:
procedure Q (A, B : Integer); procedure Q (A, B : Float);
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)));
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.
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" relationship of Boolean algebra. That is,
A implies B
could be written as
(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 get this right because it requires duplicating the entire call.
For instance, we have to write:
if Num_Errors = 1 then
Put_Line ("Compilation of " & Source_Name & "completed with" &
Error_Count'Image(Num_Errors) & "error detected.");
else
Put_Line ("Compilation of " & Source_Name & "completed with" & Error_Count'Image(Num_Errors) & "errors detected.");
end if;
The duplication of course brings the hazard of not making the same changes to each message during maintenance.
Using a conditional expression, we can eliminate this duplication:
Put_Line ("Compilation of " & Source_Name & "completed with" &
Error_Count'Image(Num_Errors) & (if Num_Errors = 1 then "error" else "errors") & " detected.");
!ACATS test
ACATS B and C tests are needed.
!appendix
```
From: Tucker Taft
Sent: Sunday, February 22, 2009  4:51 AM

[Find the rest of this message in AI05-0145-1.]

Somewhat independent suggestion:

Add "X implies Y" as a new short-circuit operation meaning
"not X or else Y".

By making it a short-circuit operation, we avoid the
burden of worrying about user-defined "implies" operators
(which then might no longer mean "not X or Y"),
boolean array "implies" operators, etc., and the compiler
can trivially transform them to something it already
knows how to compile.

I suspect "implies" will be used almost exclusively in Assert
and pre/post conditions.

****************************************************************

From: Bob Duff
Sent: Tuesday, February 24, 2009  10:25 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 "implies" and
"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".
"Implies" on arrays is not terribly useful, but the implementation is trivial,
so I'd go for uniformity.

Note that "<=" on Booleans means "implies" (not short circuit, of course).

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

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.

****************************************************************

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
> "implies" and "implies then"?  Seems more uniform.

This is uniformity run amok. 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 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
> 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
> left-hand side, and perhaps for efficiency in some cases.

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

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

> 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 definitely disagree strongly with this, and I really can't believe anyone
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",
> 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 cover up a case where the full evaluation
is required for correctness.

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

****************************************************************

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
> > "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
>insist on the non-short-circuited form can use that name.

I sometimes write:

pragma Assert (Is_Good (X) <= -- implies
Is_Gnarly (Y));

The comment is necessary.  ;-)

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",
> > any more 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.
>
> 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"
on non-binary modular types [*] would just be a feature nobody would use.

[*] 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
> > 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
> 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
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> 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
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").

> 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
>announcement after all.

Shrug.  If you say "multiply the number of unicorns in the world by the
cost of feeding a unicorn", I can stop listening at "by".
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",
> > 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
> 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
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.

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

I guess you and I will never agree on this issue.
I can live with that.  And I'll continue to put in the noise word "then" after
every "and" in AdaCore code.  ;-)

****************************************************************

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

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

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: 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: 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,
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: 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,
> 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: 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: 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: 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: 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: 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: 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: 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.

****************************************************************

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

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

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.

****************************************************************

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

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

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.

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

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

****************************************************************

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

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:

Fruit : in out Fruit_Type; Bowl : in out Bowl_Type) is
begin
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);

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:

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

...

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

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

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

Anyway, how would you extend that to allow "elsif"?

****************************************************************

From: Robert Dewar
Sent: Thursday, March  5, 2009  7:14 PM

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