Version 1.4 of ai12s/ai12-0341-1.txt

Unformatted version of ai12s/ai12-0341-1.txt version 1.4
Other versions for file ai12s/ai12-0341-1.txt

!standard 4.5.7(5/3)          19-09-04 AI12-0341-1/01
!standard 5.4(2/3)
!class Amendment 19-09-04
!status No Action (9-0-1) 19-10-05
!status work item 19-09-04
!status received 19-07-18
!priority Low
!difficulty Easy
!subject Syntax of conditional case expressions and statements
!summary
!problem
The syntax of Ada usually is designed so that it positively identifies the programmer's intent. For instance, one cannot just omit a statement, "null;" has to be used if nothing is needed.
However, the selected syntax for conditional case expressions and statements does not have a positive indication that a conditional case, rather than a traditional case, is intended. Instead, the omission of an expression changes the semantics significantly:
case X is -- traditional case statement
case is -- conditional case statement
!proposal
(See Summary.)
!wording
In 4.5.7(5/5) and 5.4(2/5), replace "case is" with "case select".
!discussion
A large number of ideas were suggested here. Following are some of them:
case of ... case separate ... separate ... protected case ... case <> is ... case <boolean-subtype> is ... case ...
There even was a proposal to use "orif" in an if statement. This latter suggests that the order of the choices is significant (it is not).
!example
The example in the Problem statement of AI12-0214-2 could be written:
(case select
when X > 5 => ... when X < 5 => ... when X = 6 => ...)
!corrigendum 4.5.7(5/3)
Replace the paragraph:
case_expression ::= 
   case selecting_expression is
   case_expression_alternative {,
   case_expression_alternative}
by:
case_expression ::= 
   case selecting_expression is
   case_expression_alternative {,
   case_expression_alternative}
 | case select
   conditional_case_expression_alternative {,
   conditional_case_expression_alternative}
!corrigendum 5.4(2/3)
Replace the paragraph:
case_statement ::= 
   case selecting_expression is
       case_statement_alternative
      {case_statement_alternative}
   end case;
by:
case_statement ::= 
   case selecting_expression is
       case_statement_alternative
      {case_statement_alternative}
   end case;
 | case select
       conditional_case_statement_alternative
      {conditional_case_statement_alternative}
   end case;
!ASIS
No change needed here (AI12-0214-2 should be sufficient.)
!ACATS test
No new tests are needed (we don't separately test syntax), but tests for AI12-0214-2 need to be modified to use the syntax given here.
!appendix

[Editor's note: The following is split off of a thread started in 
AI12-0214-2.]

From: Richard Wai
Sent: Thursday, July 18, 2019  11:02 PM

> > I can see both sides of this argument.  As I said, we should
> > *consider* simplifying the syntax.  I'd be curious what others think.
> 
> Same here.

It is bad enough that we are violating one of the greatest features of
regular case statements: static safety. I can't see the value in making
things any more inconsistent. If regular case statements accept multiple
conditions, so should case_expressions, IMO. 

I was a little late joining the party for this AI, but after reviewing the
discussion, I'm in the camp that this entire proposal is problematic since
it violates the familiar specializations of case statements - that the
compiler will be able to confirm the exclusivity of the choices. Ada's case
statements are powerful, elegant, and a huge boon to safety and
maintainability. I can't say any of that about case expressions.

I love SPARK, but it's not something you use on everything. So I oppose any
implicit suggestion that such statements are intended to be proven by an
external tool (pardon me if I misread this). Programmers will use these if
we give them the option. And without formal verification, it is way too easy
to have Arianne 5 syndrome where a Program_Error pops up in a corner case
that no one was prepared for, at the worst possible moment. It is too easy
to overlook complex case expressions, and I suspect that you'd have a lot of
those in the wild.

Honestly, why don't we just bring Contract_Cases into Ada and call it a day?
All of these fancy expressions are giving me nightmares where Ada 2030
becomes a superset of Erlang.


P.S. 

I know this opens a real can of worms, but I couldn't help thinking what if
we made this a "selective_expression" instead?

(select
   when X > 5 => True;
or
   when X < 5 => False;
or
  when X = 6 => False);

Obviously this is a bit of stretch since select statements are explicitly
tied to tasking, but they do seem to be more naturally (from the
programmer's view) representative of the problem, and allow us to
distinguish from case statements without introducing a new reserved word.
It's also not at all surprising to get an exception out of a select
statement - in fact a Program_Error is already prescribed if there are no
open alternatives. That's serendipitously close to what we are talking about
here! 

Ignoring the association with tasking, only a small change from the actual
behavior of select statements would be needed: The rule that exactly one
alternative must be selectable in a selective_expression, at the penalty of
a Program_Error. The existing select statement rules require a Program_Error
is raised if there are none of the alternatives are open, so this is already
built-in.

So it could be defined like this
I.e.

selective_expression ::= 
  select 
    guard expression
{ or
    guard expression }
[ else
    expression ]

I think this could quite useful in a variety of non contractual situations,
and is much more readable (IMO) than "case is".

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

From: Randy Brukardt
Sent: Friday, July 19, 2019  12:35 AM

...
> And without formal verification, it is way too easy to have Arianne 5 
> syndrome where a Program_Error pops up in a corner case that no one 
> was prepared for, at the worst possible moment. It is too easy to 
> overlook complex case expressions, and I suspect that you'd have a lot 
> of those in the wild.

I've worried about this some myself, but I've eventually concluded that the 
problem is assuming that any sort of verification really eliminates the 
corner case problem. The Arianne code was verified after all -- for the 
Arianne 4. And for that reason they thought they could get away without 
handling runtime errors. I don't buy the notion that you can truly prove them 
away -- especially with a tool separate from the compiler which necessarily is
going to have a slightly different interpretation of language rules (and has 
no chance of getting the right answer for compiler mistakes).
You can significantly reduce the possibility, but never to zero.

I would hope that good program management would keep the number of these 
things down to cases which are relatively easy to prove correct. And I also 
expect that compilers will spend a decent amount of effort on proving these 
things -- as the disjointness check is rather expensive, so eliminating that
cost is a good thing. (Janus/Ada is moving in the direction of (optionally) 
giving a warning on any check it can't eliminate, as those are both 
performance sapping and suggest potentially unsafe code.)

> Honestly, why don't we just bring Contract_Cases into Ada and call it 
> a day?

Contract_Cases in Ada also has dynamic checks of this sort, and on top of 
that, they destroy the readability of the precondition (which is much more
important than the postcondition, as it is the contract that clients HAVE 
to understand). SPARK avoids that by statically requiring that the contract
cases cover exactly the precondition, but of course Ada doesn't have the 
ability to make such a requirement outside of trivial cases and it's not 
even possible to detect the mistake dynamically (it looks the same as a 
precondition failure).

...
> P.S. 
> 
> I know this opens a real can of worms, but I couldn't help thinking 
> what if we made this a "selective_expression" instead?
> 
> (select
>    when X > 5 => True;
> or
>    when X < 5 => False;
> or
>   when X = 6 => False);

That was *exactly* my original idea. But that means we can't have 
selective_statements, and that seems bad. If this is worthwhile in 
expressions, it surely is worthwhile in larger contexts.

> Obviously this is a bit of stretch since select statements are 
> explicitly tied to tasking, but they do seem to be more naturally 
> (from the programmer's view) representative of the problem, and allow 
> us to distinguish from case statements without introducing a new 
> reserved word.
> It's also not at all surprising to get an exception out of a select 
> statement - in fact a Program_Error is already prescribed if there are 
> no open alternatives. That's serendipitously close to what we are 
> talking about here!
> 
> Ignoring the association with tasking, only a small change from the 
> actual behavior of select statements would be
> needed: The rule that exactly one alternative must be selectable in a 
> selective_expression, at the penalty of a Program_Error. The existing 
> select statement rules require a Program_Error is raised if there are 
> none of the alternatives are open, so this is already built-in.
> 
> So it could be defined like this
> I.e.
> 
> selective_expression ::=
>   select 
>     guard expression
> { or
>     guard expression }
> [ else
>     expression ]
> 
> I think this could quite useful in a variety of non contractual 
> situations, and is much more readable (IMO) than "case is".

I didn't worry about the supposed tasking implications. I think a statement 
version is required (I don't want a situation where I *have* to write a 
crazy complex expression just to get some structuring feature - statements 
are supposed to be providing structure). To use "select", you'd have to come 
up with a way to allow select_statements to be used this way -- but then you 
definitely would be running into a conflict with tasking.

The best solution clearly is a new reserved word (I had suggested 
"alternative"), since this construct is about halfway between an if and a 
case, having features of both. But I don't know if this problem is sufficient 
to introduce a new reserved word.

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

From: Jean-Pierre Rosen
Sent: Friday, July 19, 2019  2:06 AM

Thinking about it, this seems like a tempest in a teapot. After all, what is 
the difference between this new construct and a plain if..elsif?
The check that alternatives are mutually exclusive. So why not call this a 
special kind of if statement? Like:

<asbestos suit>
protected if <cond> then
   <stmt>
elsif ...
end protected if;
</asbestos suit>

(and similarly for the expression version)

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

From: Richard Wai
Sent: Friday, July 19, 2019  2:27 PM

> I didn't worry about the supposed tasking implications. I think a statement
> version is required (I don't want a situation where I *have* to write a crazy
> complex expression just to get some structuring feature - statements 
> are supposed to be providing structure). To use "select", you'd have to come
> up with a way to allow select_statements to be used this way -- but then 
> you definitely would be running into a conflict with tasking.

I was thinking about this as well! I was going to suggest adding another 
alternative to select_alternative, which would be called 
"expression_alternative", wich would allow a single guarded expression. Of 
course this was silly since a selective_accept statement is not an expression, 
and so to whither the value goes? I also thought about a "local_alternative" 
which would simply be a sequence of statements that must be guarded. I tried 
to think of something useful for that, but it seems else could do that job in
most cases, though theoretically it could allow a sort of "multiple else" 
condition which could be a lot cleaner..

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

From: Richard Wai
Sent: Friday, July 19, 2019  2:06 AM

> Thinking about it, this seems like a tempest in a teapot. After all, 
> what is the difference between this new construct and a plain if..elsif?
> The check that alternatives are mutually exclusive. So why not call 
> this a special kind of if statement? Like:

Well I guess the issue at hand is, we want to ensure  that only one outcome 
could ever be possible, regardless of the order of evaluation. The problem 
with else if being that the programmer has to be careful to enforce that 
order correctly.

> <asbestos suit>
> protected if <cond> then
>    <stmt>
> elsif ...
> end protected if;
> </asbestos suit>
> 
> (and similarly for the expression version)
> --

I kind of like "protected case" - it's way more distinguished than "case is". 
But then again, we'd have to worry about confusion over concurrency... 

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

From: Randy Brukardt
Sent: Friday, July 19, 2019  6:25 PM

I don't think "protected" has the right connotation; it doesn't mean 
"exclusive" to me.

I wonder if we could do something with "xor", which does have the right 
connotation. There'd have to be some care about the parsing (don't want to 
make this ambiguous with an expression). Perhaps "case xor is" or just 
"case xor"?

Another reserved word that is underused is "separate". That's roughly the 
right idea for this concept. "separate case"? "case separate"??

That's enough ideas thrown at the wall for one evening. :-)

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

From: Tucker Taft
Sent: Friday, July 19, 2019  6:42 PM

Case statement alternatives are already mutually exclusive, so I don't see the 
issue. The difference is that for these "boolean" case statements, the 
exclusivity is checked dynamically.  I don't see any inconsistency in using 
"case" here.  I agree that one of these uses static checks, and the other uses 
dynamic checks, but that doesn't change things fundamentally in my view,  The 
mutually exclusive property is the key point in my view.  

We know there are many cases in Ada where a very similar rule is enforce 
statically in one situation and dynamically in another (e.g. base range 
checks, accessibility checks, generic parameter matching rules, etc.).

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

From: Randy Brukardt
Sent: Friday, July 19, 2019  7:20 PM

True enough, but if we can get a bit more visibility into when the checks are 
static and when they are dynamic, that seems like a bonus. And at least some 
people feel that "case is" is ugly and feels like it is missing something. If
we can address these issues with a minor syntax change, that seems like a 
good thing (surely better than going back to the drawing board and inventing 
new constructs - or abandoning solving the problem).

I thought of proposing:

    separate
      when X > 5 => ...
      when X < 5 => ...
      when X = 6 => ...
    end separate;

but that seems unnecessarily different. But:

    case separate -- is??
      when X > 5 => ...
      when X < 5 => ...
      when X = 6 => ...
    end case;

doesn't feel as much like the header is missing something.

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

From: Tucker Taft
Sent: Saturday, July 20, 2019  7:24 AM

Or how about "case <boolean-subtype> is ..."?

Then you can get away from the somewhat ugly rule that it requires the 
predefined Boolean  type.  But of course 99% of them would be:

   case Boolean is
     when ...
     ...

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

From: Tullio Vardanega
Sent: Sunday, July 21, 2019  8:12 AM

That one proposal, I begin to like ...

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

From: Richard Wai
Sent: Sunday, July 21, 2019  10:39 PM

> Or how about "case <boolean-subtype> is ..."?

Or perhaps..

case <> is ...  ?

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

From: Yannick Moy
Sent: Sunday, July 21, 2019  8:40 AM

FWIW, having to write "case Boolean is" feels really clumsy to me, even if it
has some logic behind it.
The alternative "case is" also has some logic, and one fewer word.

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

From: Tucker Taft
Sent: Wednesday, July 24, 2019  1:46 PM

We could also consider "case of ..." which is distinct enough that it should 
be obvious we are talking about something different from the "usual" case 
statement.

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

From: Bob Duff
Sent: Wednesday, July 24, 2019  2:08 PM

> We could also consider "case of ..." which is distinct enough that it 
> should be obvious we are talking about something different from the 
> "usual" case statement.

I always liked the Pascal syntax, using "of".
I've always thought "is" is weird in a case stm.

> > FWIW, having to write "case Boolean is" feels really clumsy to me, 
> > even if it has some logic behind it.  The alternative "case is" also 
> > has some logic, and one fewer word.

I also find "case Boolean is" to be kind of odd.
It would make more sense to say "case True is".

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

From: Tucker Taft
Sent: Wednesday, July 24, 2019  3:19 PM

> I also find "case Boolean is" to be kind of odd.
> It would make more sense to say "case True is".

But "case True is ..." would be a legal "normal" case statement, which would 
allow at most two choices, one statically True, and one statically False.  It
would be roughly equivalent to "if True then ... else ... end if;"

In any "case," any more comments on "case of ..."?

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

From: Jean-Pierre Rosen
Sent: Wednesday, July 24, 2019  3:34 PM

> In any "case," any more comments on "case of ..."?
I think that "case of when..." reads very strange

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

From: Tucker Taft
Sent: Wednesday, July 24, 2019  3:59 PM

When written all on one line I would agree.  Does it read better as:

   case of
      when X < 5 => Abc;
      when X = 5 => Def;
      when X > 5 => Ghi;
  end case;

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

From: Randy Brukardt
Sent: Wednesday, July 24, 2019  4:15 PM

It's OK, but doesn't excite me.

I'm still lobbying for a different keyword, with my suggestion being 
separate. Either:

    case separate
       when X < 5 => Abc;
       when X = 5 => Def;
       when X > 5 => Ghi;
    end case;

or more radically:

    separate
       when X < 5 => Abc;
       when X = 5 => Def;
       when X > 5 => Ghi;
    end separate;

[This latter being essentially my original idea that started the discussion 
on this one.]

Of course, this seems to have excited exactly no one as well. Probably will 
have to discuss this in a meeting to get any sort of consensus. And I'm trying 
to not say too much here so I'm not dominating the conversation.

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

From: Richard Wai
Sent: Wednesday, July 24, 2019  4:20 PM

> In any "case," any more comments on "case of ..."?

I also feel "case of when" reads a bit strange. 

I think we are all in some agreement that this form of a case expression is 
problematic in that it really doesn't act anything like a normal case 
statement, and this is confusing (and potentially unsafe).

Considering that case statements are really there to allow for two nice
features:
1. Implementing jump tables (most languages) 
2. Static assurance that all cases are accounted for (Ada)

This monster of a case expression we are talking about does none of those, 
as we've talked about. I also note that some have mentioned the similarities 
to an if statement, except that the evaluation of the conditions for each 
alternative happens in all cases.

So here is a totally outside the box idea. --

How about we just modify if statements (and expressions) by adding a new 
reserved word that is a sibling to elsif - "orif". "orif" would be mutually 
exclusive to "elsif" in a given if statement/expression. So we could mofidy
5.3/2 as follows:

If_statement ::=
	If condition then
		Sequence_of_statmenets
	{elsif condition then
		Sequence_of_statements} |
	{orif condition then
		Sequence_of_statements}
	[else
		Sequence_of_statements]
end if;


For if statements/expressions with orif, the following rules apply:
All conditions for all "orif" as well as the initial "if" are always evaluated.
If more than one (including the opening if) evaluates True, program_error is 
raised. If none evaluate True, else is executed (if it exists).

Honestly I think this could end up being much more broadly useful than a 
"case expression without selecting_expressions".

I know that there is a general discomfort with adding new reserved words, but I 
think "orif" is palatable since it is pretty unlikely to be used in an 
existing program (I'd think).

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

From: Tucker Taft
Sent: Wednesday, July 24, 2019  4:33 PM

> I also feel "case of when" reads a bit strange. 

Did you see my follow-up question, showing it properly indented?

...
> we could mofidy
> 5.3/2 as follows:
> 
> If_statement ::=
> 	If condition then
> 		Sequence_of_statmenets
> 	{elsif condition then
> 		Sequence_of_statements} |
> 	{orif condition then
> 		Sequence_of_statements}
> 	[else
> 		Sequence_of_statements]
> end if;
> 

This leaves the visibility of the mutually exclusive property to a two-letter 
difference potentially buried.  

I think we want this to be highly visible, and I believe "case" has the right 
"mutual exclusion" semantics.  I could also get behind "select" (or "select 
case ..." or "case select ...") as another possibility, if "case" by itself 
creates heartburn.  But having a special connector buried in an "if" statement 
is definitely going in the wrong direction in my view.

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

From: Richard Wai
Sent: Wednesday, July 24, 2019  4:45 PM

> This leaves the visibility of the mutually exclusive property to a two-letter
> difference potentially buried.

I don't really see that since you couldn't have an if statement with both 
elsif and orif, and orif looks pretty different from elsif.

OTOH, I can see the argument where one could say that we are so use to seeing 
if .. elsif .. elsif .. else that the casual reader might gloss-over the 
difference and mis-perceive "orif" as "elsif"

But at least if statements don't come with the expectation that the compiler 
is going to make sure you didn't miss a condition. So at a high level I'd 
still think it would be safer in practice.

> I think we want this to be highly visible, and I believe "case" has the right
> "mutual exclusion" semantics.  I could also get behind "select" (or "select
> case ..." or "case select ...") as another possibility, if "case" by itself 
> creates heartburn.  But having a special connector buried in an "if" 
> statement is definitely going in the wrong direction in my view.

I don't think it's any more "buried" than elsif.. But I suppose in a 
"pyramid of doom" this could be a problem for the same reasons I've conceded 
above.

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

From: Richard Wai
Sent: Wednesday, July 24, 2019  4:48 PM

>     separate
>        when X < 5 => Abc;
>        when X = 5 => Def;
>        when X > 5 => Ghi;
>     end separate;

You've got my vote here, aside from my usual crazy ideas!

I really like the idea of dropping the word "case" altogether. I really can't 
stomach any kind of case statement that is not statically verified by the 
compiler.

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

From: Steve Baird
Sent: Wednesday, July 24, 2019  5:38 PM

>  I could also get behind "select" (or "select case ..." or 
> "case select ...") as another possibility, if "case" by itself creates 
> heartburn.  But having a special connector buried in an "if" statement 
> is definitely going in the wrong direction in my view.

Sounds right to me.

To me, either of those options reads better than "separate". Unlike Richard, 
I want to see the word "case" in there somewhere because we are choosing to 
execute exactly one of a set of alternatives and the order in which those 
alternatives are listed is pretty much irrelevant.

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

From: Edmond Schonberg
Sent: Wednesday, July 24, 2019  8:02 PM

I also like  “case select”,  given the obvious resemblance with a select 
statement all of whose alternatives have guards.

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

From: Jean-Pierre Rosen
Sent: Thursday, July 25, 2019  12:41 AM

> When written all on one line I would agree.  Does it read better as:
> 
>    case of
>       when X < 5 => Abc;
>       when X = 5 => Def;
>       when X > 5 => Ghi;
>   end case;

I don't think so. I wrote it on one line to show that it doesnt' read 
normally, but I didn't expect it to be written that way.

I like it when a program reads like natural language...

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

From: Jeff Cousins
Sent: Thursday, July 25, 2019  3:37 AM

Joining in ...

I too like the idea of the reserved word “select” appearing somewhere.

“case of” read better than “case is”, in English English at least, though 
that comment would be equally applicable to the original case statement too.

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

From: Tucker Taft
Sent: Thursday, July 25, 2019  10:56 AM

Let me then make an "official" proposal:


    Change "case is <nl> when .. => ...." to 
    "case select <nl> when ... => ..." and make essentially no other change 
    to the AI.  ("<nl>" here means "new line".)

This has the advantage of keeping this as a "case" expression/statement rather
than having to invent a new kind of expression/statement (and yet another 
subclause ;-), and the "select <nl> when ..." combination already exists in 
the Ada lexicon.  It also avoids making it into another kind of "select" 
statement, all of which currently reside in the Tasks and Synchronization part 
of the manual, which is clearly wrong for this one.

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

From: Steve Baird
Sent: Thursday, July 25, 2019  11:56 AM

> case select

Among the alternatives we have discussed, I like this one the best.

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

From: Gary Dismukes
Sent: Thursday, July 25, 2019  12:01 PM

I second that.

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

From: Jeff Cousins
Sent: Thursday, July 25, 2019  1:06 PM

I third it.

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

From: Yannick Moy
Sent: Thursday, July 25, 2019  3:30 AM

> For if statements/expressions with orif, the following rules apply:
> All conditions for all "orif" as well as the initial "if" are always
> evaluated. If more than one (including the opening if) evaluates True,
> program_error is raised. If none evaluate True, else is executed (if it
> exists).

This proposal is my favorite so far. It reads naturally for the user, and 
shows the strong connection of the usual if-statement or if-expression to 
this new construct. As a user, I would be more inclined to replace previous
if-statement/expression with this version that simply spells out the 
distinction of cases.

I don't think that "elsif" and "orif" look the same, not more than "or" and 
"xor" look the same.

> Honestly I think this could end up being much more broadly useful than a
> "case expression without selecting_expressions".

I agree. 

This AI originates in the Contract_Cases aspect in SPARK, which is a sometimes 
useful but in fact rarely used feature in practice. What is more, it's unlikely
that this new feature is going to replace all uses of Contract_Cases, because 
Contract_Cases has the nice additional benefit that guards are evaluated on 
subprogram entry, so in the general case you'd have to sprinkle 'Old all over
your guards, which is unwise (it makes the contract less readable and more 
likely to be incorrect if you miss a 'Old somewhere).

So the utility of this new feature completely rests on replacing existing 
if-statements/expressions. It's more likely to happen with the syntax 
proposed here.

> I know that there is a general discomfort with adding new reserved words,
> but I think "orif" is palatable since it is pretty unlikely to be used in an
> existing program (I'd think).

I agree.

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

From: Erhard Ploedereder
Sent: Thursday, July 25, 2019  3:59 PM

>    case of
>       when X < 5 => Abc;
>       when X = 5 => Def;
>       when X > 5 => Ghi;
>   end case;

Why isn't this simply

   case
       when X < 5 => Abc;
       when X = 5 => Def;
       when X > 5 => Ghi;
   end case;

Ignore me if this has already been rejected.

(My credo: keywords ought to be there for a reason.
 The "of" hardly serves any reason in the absence of a selecting expression 
 (in the "normal" case it acts as a mnemonic separator for the expression).

Incidentally, Dijkstra's case statement
  - allowed overlapping choices
  - left the choice among open guards non-deterministic on purpose
  - failed if none of the guards were true.

This is certainly a more efficient and, arguably, better choice.
Dijstra thought so and argued that making something deterministic where you 
do not really care which arm is executed ("all roads lead to Rome"), is a 
hindrance to robust programming.
It checks for completeness by making the fall-through illegal.

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

From: Steve Baird
Sent: Thursday, July 25, 2019  4:47 PM

> Why isn't this simply
> 
>     case
>         when X < 5 => Abc;
>         when X = 5 => Def;
>         when X > 5 => Ghi;
>     end case;

One argument for adding some new reserved word for this new construct has to
do with IDEs which (perhaps using only syntactic information) support entering
a fragment of a construct and then requesting the IDE to intelligently supply 
whatever is missing.

The Rational Apex "format" command, for example, might replace the above text 
with

     case [expression] of
        when X < 5 => Abc;
        when X = 5 => Def;
        when X > 5 => Ghi;
     end case;

with "[expression]" displayed as a prompt (i.e., if you type on top of it, it 
will disappear).

Your proposal would, as far as I can see, require changing this desirable 
behavior for users of the next version of Ada.

If we are going to add a new form of case statement and case expression, I 
think we want it to differ syntactically from the existing forms by more than 
just the absence of some portions of the older constructs.

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

From: Randy Brukardt
Sent: Thursday, July 25, 2019  10:11 PM

>This AI originates in the Contract_Cases aspect in SPARK, which is a 
>sometimes useful but in fact rarely used feature in practice.
>What is more, it's unlikely that this new feature is going to replace 
>all uses of Contract_Cases, because Contract_Cases has the nice 
>additional benefit that guards are evaluated on subprogram entry, so in 
>the general case you'd have to sprinkle 'Old all over your guards, 
>which is unwise (it makes the contract less readable and more likely to 
>be incorrect if you miss a 'Old somewhere).

It will at least keep them from appearing in Ada code, which is a big benefit.
The "guards" of Contract_Cases are evaluated on entry because they are 
logically part of the precondition. That only works if they are statically 
proven to be equivalent to the stated precondition, which is fine for SPARK
but impossible for Ada. Otherwise, they just make the precondition unreadable 
for clients (who usually will not care about the postcondition).

Since the "guards" ("choice_conditions" in this new form) are part of the 
precondition, they rarely will depend on "in out" parameters so 'Old will not 
be necessary on most items. Moreover, if 'Old is forgotten in a 
choice_condition where it is required, then it will not meet the requirements 
in AI12-0280-2 and most likely uses of 'Old in the dependent_expression(s) 
will be illegal. I think that should make the mistake pretty obvious. :-) The
explicit inclusion of 'Old also will make it clear when the values are 
evaluated - doing that implicitly is dangerous in its own way. (Remember, I 
don't use "use clauses" much either - I find a lot of value in saying a bit 
more to keep things explicit.)

The only reason for even considering this feature is to provide the 
functionality of Contract_Cases in a way that is both friendly to Ada and 
still analyzable by SPARK. Any other uses are very secondary.

>So the utility of this new feature completely rests on replacing 
>existing if-statements/expressions. It's more likely to happen with the 
>syntax proposed here.

I don't think such usage is of enough utility to even consider for Ada. This 
is all about replacing Contract_Cases with something that is more readable to
those that understand Pre/Post but not necessarily every nuance of SPARK 
(that would be me, for one).

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

From: Randy Brukardt
Sent: Thursday, July 25, 2019  10:17 PM

> > Why isn't this simply
> > 
> >     case
> >         when X < 5 => Abc;
> >         when X = 5 => Def;
> >         when X > 5 => Ghi;
> >     end case;
> 
> One argument for adding some new reserved word for this new construct 
> has to do with IDEs which (perhaps using only syntactic information) 
> support entering a fragment of a construct and then requesting the IDE 
> to intelligently supply whatever is missing.

More generally, it is about positively identifying the programmer's intent.
Ada rarely uses omission to represent anything; in most cases we have some 
positive thing (such as "null;" rather than just omitting a statement). I 
tend to think that Ada does far too much assuming anyway [if I was "improving"
the syntax, I would make identifiers after "end" manditory, along with 
subprogram modes (saving three characters (" in") isn't worth the confusion 
as to whether to write it or not)].

As such, this sort of case statement needs a positive indication that it is 
intended, not just the absence of something (the current syntax also suffers
from this problem). The "case select" proposal is better in this way than 
either this proposal or the original one.

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

From: Yannick Moy
Sent: Friday, July 26, 2019  2:46 AM

> It will at least keep them from appearing in Ada code, which is a big
> benefit. 

I don't understand the above sentence. The new feature prevents 'Old in Ada 
code? What's the difference here with Contract_Cases?

> The "guards" of Contract_Cases are evaluated on entry because they
> are logically part of the precondition. That only works if they are
> statically proven to be equivalent to the stated precondition, which is fine
> for SPARK but impossible for Ada. Otherwise, they just make the precondition
> unreadable for clients (who usually will not care about the postcondition).

David Parnas would disagree with you, cf the Parnas Tables: 
https://cs.uwaterloo.ca/~jmatlee/talks/parnas01.pdf

Having used Contract_Cases, I don't agree as well.

> Since the "guards" ("choice_conditions" in this new form) are part of the
> precondition, they rarely will depend on "in out" parameters so 'Old will
> not be necessary on most items. 

>Precisely, it will be necessary on some not all, which is a recipe for 
>confusion.

>Moreover, if 'Old is forgotten in a
>choice_condition where it is required, then it will not meet the
>requirements in AI12-0280-2 

I don't follow your argument. You're talking about two different AI here, can 
you explain?

>and most likely uses of 'Old in the
>dependent_expression(s) will be illegal. I think that should make the
>mistake pretty obvious. :-) 

That's yet something else, the use of 'Old in the dependent_expression, which 
is not part of the AI and would be yet another complexity added on top.

>The explicit inclusion of 'Old also will make it
>clear when the values are evaluated - doing that implicitly is dangerous in
>its own way. (Remember, I don't use "use clauses" much either - I find a lot
>of value in saying a bit more to keep things explicit.)

Contract_Cases indeed have guards evaluated in the pre-state and consequences 
evaluated in the post-state. That's something to learn, but clearly less 
error-prone than the alternative you propose here.

>The only reason for even considering this feature is to provide the
>functionality of Contract_Cases in a way that is both friendly to Ada and
>still analyzable by SPARK. Any other uses are very secondary.

Then, I would not propose it. Given that not all uses of Contract_Cases can 
be replaced IMO, I'll keep one way of specifying such contracts, instead of 
having two ways. 

>So the utility of this new feature completely rests on replacing 
>existing if-statements/expressions. It's more likely to happen 
with the syntax proposed here.

>I don't think such usage is of enough utility to even consider for Ada. This
>is all about replacing Contract_Cases with something that is more readable
>to those that understand Pre/Post but not necessarily every nuance of SPARK
>(that would be me, for one).

If that's only for SPARK users, I see no benefit in keeping this feature.

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

From: Randy Brukardt
Sent: Friday, July 26, 2019  11:43 PM

>>It will at least keep them from appearing in Ada code, which is a big 
>>benefit.

>I don't understand the above sentence. The new feature prevents 'Old in 
>Ada code? What's the difference here with Contract_Cases?

"them" => Contract_Cases. This feature (and the fact that Contract_Cases will 
not be defined in Ada) will keep Contract_Cases out of Ada code. Which is a 
good thing, IMHO, give the damage Contract_Cases does to readability.

>>	The "guards" of Contract_Cases are evaluated on entry because they
>>	are logically part of the precondition. That only works if they are
>>	statically proven to be equivalent to the stated precondition, which
>>      is fine for SPARK but impossible for Ada. Otherwise, they just make the
>>      precondition unreadable for clients (who usually will not care about 
>>      the postcondition).
		
>David Parnas would disagree with you, cf the Parnas
>Tables: https://cs.uwaterloo.ca/~jmatlee/talks/parnas01.pdf
>
>Having used Contract_Cases, I don't agree as well.

Not sure which part you disagree with above. For Ada (again IMHO), readability 
is paramount. And mixing the precondition and postcondition clearly harms 
readability. Moreover, *all* clients of a subprogram need to know the 
precondition of a subprogram, whereas only some clients of a subprogram need 
to know the details of the postcondition. Contract_Cases, at least without 
static checking as was proposed for Ada, makes it very hard to know what the 
precondition actually is, since one has to "or" together all of the various 
"guards" to figure that out. As such, one would have to write a comment 
explaining the actual precondition, which defeats the entire purpose of 
preconditions (eliminating comments about preconditions).

You could have only used Contract_Cases in SPARK (because there is no dynamic 
version in Ada as it stands), which makes the needed static checks to 
eliminate that problem. That makes all the difference vis-a-vis the 
precondition, and presumably the readability as well.

(Another complaint raised against Contract_Cases is that it encourages a style 
where essentially the entire subprogram body is reproduced in the 
postcondition, which essentially eliminates the separation of specification 
and implementation. It's especially bad in Ada since the language in which the 
body and the postcondition is written is the same. While I agree with the 
basic complaint, I don't think it matters a lot because I don't see any 
language rules that could discourage such contracts. Such worries have to be 
left to style guides and code reviews and management.)

>>Since the "guards" ("choice_conditions" in this new form) are part of 
>>the precondition, they rarely will depend on "in out" parameters so 
>>'Old will not be necessary on most items.

>Precisely, it will be necessary on some not all, which is a recipe for
confusion.

Not having 'Old in the postcondition is also a recipe for confusion. Note 
that it is fine to put 'Old on all items, so there is no problem with doing 
that if it helps reduce your confusion.

>>Moreover, if 'Old is forgotten in a
>>choice_condition where it is required, then it will not meet the 
>>requirements in AI12-0280-2

>I don't follow your argument. You're talking about two different AI 
>here, can you explain?

When I'm discussing the replacement of Contract_Cases in Ada (or pretty much 
anything these days), I'm talking about the entire Ada 202x language, not just
some single feature. And in this case, one needs both AI12-0214-2 and
AI12-0280-2 to get the needed features.

AI12-0280-2 changes the rules that make 'Old prefixes illegal by using the 
parts of postconditions that are known at subprogram entry to determine which
'Old prefixes do not need to be evaluated at all, or do not need any 
restrictions enforced on them.

>>and most likely uses of 'Old in the
>>dependent_expression(s) will be illegal. I think that should make the 
>>mistake pretty obvious. :-)

>That's yet something else, the use of 'Old in the dependent_expression, 
>which is not part of the AI and would be yet another complexity added 
>on top.

This is also already done (except for final approval of the wording). Note 
that this "complexity" has a number of good effects for all postconditions 
regardless of the value for Contract_Cases or postconditions using "case
select":
  (1) Fewer illegal 'Old references;
  (2) Many 'Old prefixes that will not be used in the actual postcondition 
      are not evaluated at all (cutting costs of checking postconditions).

That's why this is a separate AI: it is a good idea even if Contract_Cases 
was never invented.

>>The only reason for even considering this feature is to provide the 
>>functionality of Contract_Cases in a way that is both friendly to Ada 
>>and still analyzable by SPARK. Any other uses are very secondary.

>Then, I would not propose it. Given that not all uses of Contract_Cases 
>can be replaced IMO, I'll keep one way of specifying such contracts, 
>instead of having two ways.

But all uses of Contract_Cases *can* be replaced (that is, written using 
"case select" and the other changes in Ada 202x) -- that's certainly the 
intent. Whether SPARK users do that is of course another question.

>If that's only for SPARK users, I see no benefit in keeping this feature. 

I'd love to be able to completely ignore SPARK and make new Ada features 
solely be about improving Ada. But that's not a practical reality. OTOH, 
it doesn't make any sense to import into Ada SPARK features that don't make 
sense in an Ada context. Especially features with only one specialized usage.
If there is another, more general way to give the same functionality, we 
have to explore those possibilities.

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

From: Erhard Ploedereder
Sent: Saturday, July 27, 2019  3:36 PM

Sounds reasonable at first what Steve wrote. On closer look, though, the 
argument applies to all proposals that start with "case". Adding an extra
reserved word will not change the situation a bit. The only remedy would 
be to not start with "case". Short analysis:

case is   -- discussed by some
case separate -- discussed by some
case when   -- my proposal

are all sequences distinct from the old

case <expression> is

and afflicted by the issue that you have to have a lookahead of 1 to decide 
how to syntactially complete.

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

From: Steve Baird
Sent: Saturday, July 27, 2019  4:40 PM

I disagree.

Suppose, for sake of discussion, we go with "case select" syntax.

Then the error-correcting parser in our hypothetical IDE can still have a 
preference rule to treat a "case" token that is not followed by a "select"
token the same as it was treated before.

There is also Randy's argument that we prefer to convey info by something 
more than just the absence of something. Ada doesn't always do that (e.g., a 
full constant declaration with the initial expression missing is a deferred 
constant declaration) but it still seems like a good principle.

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

From: Raphael Amaird
Sent: Saturday, July 27, 2019  9:38 AM

>>If that's only for SPARK users, I see no benefit in keeping this feature. 

>I'd love to be able to completely ignore SPARK and make new Ada features
>solely be about improving Ada. But that's not a practical reality. OTOH, it
>doesn't make any sense to import into Ada SPARK features that don't make
>sense in an Ada context. Especially features with only one specialized
>usage. If there is another, more general way to give the same functionality,
>we have to explore those possibilities.

I think Yannick's point is that if the feature is not of general interest 
outside of SPARK, there is little interest into porting it into Ada.

I also strongly agree with Yannick that the `case` based syntax is confusing, 
and that a syntax based on `if` makes more sense syntactically and 
semantically.

My first vote would be "no feature is needed". Let contract cases be a SPARK 
only feature, and leave Ada out of it.

My second vote would be for the syntax Yannick proposes. I think that:

1. The syntax based on case, given that you cannot statically test 
   exhaustiveness or exclusivity of case alternatives, is hugely confusing. 
   Furthermore, my experience with "for .. in"/"for .. of" is that it becomes 
   really easy to confuse one with the other, which is annoying.

2. The usefulness vs. complexity ratio is very low. 

I strongly encourage all interested parties to read Yannick's full proposal 
here: https://github.com/AdaCore/ada-spark-rfcs/pull/25

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

From: Randy Brukardt
Sent: Sunday, July 28, 2019  2:46 AM

...
>I think Yannick's point is that if the feature is not of general 
>interest outside of SPARK, there is little interest into porting it 
>into Ada.

We were asked to consider adding it to Ada - by Yannick himself, in fact. If 
we didn't have such a request, then we wouldn't be considering any of these 
ideas.

...
>I strongly encourage all interested parties to read Yannick's full 
>proposal here: https://github.com/AdaCore/ada-spark-rfcs/pull/25

It would be best to keep all of the ARG discussion together, so it can be 
referred to in the future. Splitting threads is nasty, as people lose track 
of the conversation. In this case, Richard's proposal seems pretty complete 
and my understanding was that Yannick was just copying it. (And since this is
just a syntax discussion, it doesn't take a lot to make a proposal
"complete".)

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

From: Tucker Taft
Sent: Monday, July 29, 2019  6:58 AM

...
>1. The syntax based on case, given that you cannot statically test 
>exhaustiveness or exclusivity of case alternatives, is hugely confusing. 
>Furthermore, my experience with "for .. in"/"for .. of" is that it becomes 
>really easy to confuse one with the other, which is annoying.

Note that in the ARG we seem to have moved onto "case select" from "case is" 
so the distinction is significantly more visible.  But I do understand your 
point.  From my perspective, it is more important that the mutual exclusivity
be visible from the beginning, rather than having it buried in the connector.
I also do not think it should somehow be an optional check.  And as I have 
mentioned in direct responses to Richard, whether a check is static or 
dynamic is already something that depends on context, so I don't see this as 
a big deal.  In fact, I suspect that in most cases, a decent optimizer will be
able to prove the conditions are mutually exclusive, so there will be no 
run-time overhead, and you will get good compile-time error messages.  I 
suppose you could even have an implementation-defined warning whenever it
couldn't be proved mutually exclusive, and by making that warning into an
error, you would get the compile-time checking you prefer.

>2. The usefulness vs. complexity ratio is very low. 

You might be right, though after we discussed it in the ARG, we felt the 
feature to address a periodic need, where you have a complex if/elsif/elsif/... 
and you can lose track of whether these are actually mutually exclusive 
conditions, or if there is some relevance to the ordering.  I know I have 
bumped into bugs where "elsif alternatives" have been moved thinking they were 
order independent, when in fact there was some subtle order dependence.  The 
nice thing about "case" is that it is order independent, and this feature 
would preserve that.  It also brings the selecting conditions out into a 
place where they are very visible.  In a long if/elsif sequence, I find things 
get pretty hard to read.

>I strongly encourage all interested parties to read Yannick's full proposal 
>here: https://github.com/AdaCore/ada-spark-rfcs/pull/25

I agree with Randy that it is not helpful to split the discussion at this 
point, especially since the interested parties are all on the ARG mailing 
list.  Also, this doesn't really involve some kind of AdaCore "business" 
issue, and just increasing the number of commentators will not necessarily 
increase the relative ratio of "heat" vs. "light" in such a 
syntax/aesthetics-oriented discussion. ;-)

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

From: Raphael Amiard
Sent: Wednesday, July 31, 2019  4:53 AM

>I agree with Randy that it is not helpful to split the discussion at this 
>point, especially since the interested parties are all on the ARG mailing 
>list.

What ? No, absolutely not. Also the thread above is a perfect counter example 
of what you are saying. A number of the commenters that gave useful feedback 
are:

Egilhh (A random Ada user & community member from Norway, from what I can 
gather)
Fabien Chouteau (An AdaCore engineer not involved in ARG)
Johannes Kannig and Claire Dross, two of the main SPARK engineers and 
designers, not on this ML.
Quentin Ochem, a marketing/sales manager and an Ada teacher, from AdaCore, not 
on the ARG ML.
Alejandro, a community member who made a presentation at Ada Europe last year, 
and is developing Alire, an Ada package manager that we hope will work out.

The platform is thus fulfilling its exact purpose, to my great satisfaction: 
Giving feedback about proposed features, that is never getting through here. 
So I suggest that if you insist on not splitting the discussion, you guys 
folks gather and discuss it there. This mailing list can be used to summarize 
the discussion/decide what to do in light of what has been said there.

The bottom line is that we need to take into account discussions that happen 
out there, as the ARG should stay connected with users.

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

From: Yannick Moy
Sent: Monday, July 29, 2019  12:41 AM

> "them" => Contract_Cases. This feature (and the fact that Contract_Cases
> will not be defined in Ada) will keep Contract_Cases out of Ada code. Which
> is a good thing, IMHO, give the damage Contract_Cases does to readability.

Funny, because I think the feature discussed on this TN is worse than 
Contract_Cases for expressing contracts by cases, and I explained why. So if 
your goal is to propose a replacement for Contract_Cases, as I said, better 
to leave it at that.

>Not sure which part you disagree with above. For Ada (again IMHO),
>readability is paramount. And mixing the precondition and postcondition
>clearly harms readability. 

your personal point of view. Having more experience on the proof side, I 
disagree that Contract_Cases harm readability, quite the opposite.

>Moreover, *all* clients of a subprogram need to
>know the precondition of a subprogram, whereas only some clients of a
>subprogram need to know the details of the postcondition. Contract_Cases, at
>least without static checking as was proposed for Ada, makes it very hard to
>know what the precondition actually is, since one has to "or" together all
>of the various "guards" to figure that out. As such, one would have to write
>a comment explaining the actual precondition, which defeats the entire
>purpose of preconditions (eliminating comments about preconditions).

In fact, you can still provide a precondition. 

>You could have only used Contract_Cases in SPARK (because there is no
>dynamic version in Ada as it stands), 

It has a dynamic version in the version of Ada supported in GNAT. 
Contract_Cases needs not be in the Ada standard, it's just an aspect.

>which makes the needed static checks
>to eliminate that problem. That makes all the difference vis-a-vis the
>precondition, and presumably the readability as well.

I don't agree. The dynamic checking benefits of Contract_Cases make it 
valuable even if you don't do proof.

>(Another complaint raised against Contract_Cases is that it encourages a
>style where essentially the entire subprogram body is reproduced in the
>postcondition, which essentially eliminates the separation of specification
>and implementation. It's especially bad in Ada since the language in which
>the body and the postcondition is written is the same. While I agree with
>the basic complaint, I don't think it matters a lot because I don't see any
>language rules that could discourage such contracts. Such worries have to be
>left to style guides and code reviews and management.)

I don't see where this POV comes from.
You can perfectly have weak "consequence expressions" for some or all of the 
cases, say "True". No difference with Post here.

>Not having 'Old in the postcondition is also a recipe for confusion. 

I think you're confused about the semantics of Contract_Cases. 'Old is only 
allowed in the "consequence expressions" on the right of the arrow symbol in
every case. Like it is allowed in a postcondition.

>Note
>that it is fine to put 'Old on all items, so there is no problem with doing
>that if it helps reduce your confusion.

'Old on pure inputs is confusing, and GNAT warns you about it.
Sprinkling 'Old makes conditions unreadable.

>Moreover, if 'Old is forgotten in a
>choice_condition where it is required, then it will not meet the
>requirements in AI12-0280-2 

I don't follow your argument. You're talking about two different AI here, 
can you explain?

>When I'm discussing the replacement of Contract_Cases in Ada (or pretty much
>anything these days), I'm talking about the entire Ada 202x language, not
>just some single feature. And in this case, one needs both AI12-0214-2 and
>AI12-0280-2 to get the needed features.
>
>AI12-0280-2 changes the rules that make 'Old prefixes illegal by using the
>parts of postconditions that are known at subprogram entry to determine
>which 'Old prefixes do not need to be evaluated at all, or do not need any
>restrictions enforced on them.

You're considering a quite restricted subset of cases still.
In SPARK, we're used for long a GNAT-specific pragma Unevaluated_Use_Of_Old 
that allows liberal use of Old and Loop_Entry. Mostly because proof ensures 
there are no bad consequences. So your argument won't do for SPARK where we 
need more complex expressions than what you're referring to (typically calls
to queries implemented as expression functions).

>and most likely uses of 'Old in the
>dependent_expression(s) will be illegal. I think that should make the
>mistake pretty obvious. :-) 

That's yet something else, the use of 'Old in the 
dependent_expression, which is not part of the AI and would 
be yet another complexity added on top.

>This is also already done (except for final approval of the wording). 

I'm lost. AI12-0214-2 on case without selecting_expression does not mention 
forbidding Old in dependent_expression. And doing so would kill the use of this 
feature as a replacement for Contract_Cases, as the dependent_expression is the 
equivalent of a postcondition (for a given case) so it typically has to refer 
to state on entry with Old.

>Note
>that this "complexity" has a number of good effects for all postconditions
>regardless of the value for Contract_Cases or postconditions using "case
>select":
> (1) Fewer illegal 'Old references;
> (2) Many 'Old prefixes that will not be used in the actual postcondition 
>     are not evaluated at all (cutting costs of checking postconditions).
>
>That's why this is a separate AI: it is a good idea even if Contract_Cases
>was never invented.

I think there are big problems with this AI at this stage.

>But all uses of Contract_Cases *can* be replaced (that is, written using
>"case select" and the other changes in Ada 202x) -- that's certainly the
>intent. Whether SPARK users do that is of course another question.

I suggest you refocus this AI on Ada and consult with SPARK developers and 
users for SPARK-related improvements.

>I'd love to be able to completely ignore SPARK and make new Ada features
>solely be about improving Ada. But that's not a practical reality. OTOH, it
>doesn't make any sense to import into Ada SPARK features that don't make
>sense in an Ada context. Especially features with only one specialized
>usage. If there is another, more general way to give the same functionality,
>we have to explore those possibilities.

I bear to disagree with your first sentence! SPARK is a great opportunity for 
Ada, and both strengthen the overall ecosystem.

I agree there is no reason to force SPARK features onto Ada. It certainly feels 
to me it's being done in this AI.

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

From: Randy Brukardt
Sent: Wednesday, July 31, 2019  12:02 AM

[Sorry about the delay in posting this, for some reasons all of your
(Yannick's) messages are requiring moderation, and I was away attending the 
funeral of a cousin. - RLB] 

...
>>Not sure which part you disagree with above. For Ada (again IMHO), 
>>readability is paramount. And mixing the precondition and 
>>postcondition clearly harms readability.

>your personal point of view. 

Of course. I've made that clear from the start, and I'm going to try to 
refrain from lengthening discussions that degenerate into "you're wrong", 
"no, you're wrong". And this is getting *way* off topic.

>Having more experience on the proof side, I disagree that 
>Contract_Cases harm readability, quite the opposite.

The Ada language has no proof capabilities, so the readability for proof 
should be a low priority. I'm concerned about readability for the clients
of an abstraction, whether it was proved by SPARK, or written solely by 
humans.

...
>In fact, you can still provide a precondition. 

Sure, but you can't trust it -- there is (and can be) no check that the 
precondition that is provided has any relationship to the "contract_cases".

...
>I don't agree. The dynamic checking benefits of Contract_Cases make it 
>valuable even if you don't do proof.

But that's the source of the problem. The dynamic checks do nothing to ensure 
that the precondition given has any relationship with the Contract_Cases. The 
net effect is that the *real* precondition is a combination of the 
precondition given, the inherited preconditions if any, and the Contract_Cases 
"guards". For someone doing maintenance on code with unknown coding rules 
(and especially in any debugging cases), this is a nightmare.

Now, if you can *assume* that the Contract_Cases was proven by SPARK or the 
like, then, and only then, does it work.

...
>I'm lost. AI12-0214-2 on case without selecting_expression does not 
>mention forbidding Old in dependent_expression.

That follows from the existing 'Old rules. There is nothing special about the 
dependent_expressions in "case select" or whatever syntax it gets.

AI12-0280-2 generalizes the rules to allow less restriction on the prefix of 
'Old.

...
>I think there are big problems with this AI at this stage.

Which AI are you talking about here???

...
>>I'd love to be able to completely ignore SPARK and make new Ada 
>>features solely be about improving Ada. ...

>I bear to disagree with your first sentence! SPARK is a great 
>opportunity for Ada, and both strengthen the overall ecosystem.

SPARK certainly has (ahem) sparked interest in the Ada ecosystem. But it is 
too hard to use SPARK on existing code, and it is especially hard to ease 
into SPARK in the way that one can ease into Ada.

I think that a better approach is possible using a much lighter touch. Ada
2012 provided the foundation for that, and Ada 202x provides a lot of the 
remainder. Codepeer demonstrates one way to do that; I do think even better 
approaches are possible.

>I agree there is no reason to force SPARK features onto Ada. It 
>certainly feels to me it's being done in this AI.

Because *YOU* asked us to do so!!!! If you hadn't asked, we surely would not 
have spent time in this area.

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

From: Yannick Moy
Sent: Wednesday, July 31, 2019  3:18 AM

>Because *YOU* asked us to do so!!!! If you hadn't asked, we surely would not
>have spent time in this area.

I'll just say it a last time: I did not ask for inclusion of this feature in 
Ada. So your *YOU* does not apply to me.

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

From: Yannick Moy
Sent: Wednesday, July 31, 2019  3:22 AM

>I agree with Randy that it is not helpful to split the discussion at this 
>point, especially since the interested parties are all on the ARG mailing 
>list.  

Sorry Tuck, I don't agree. I find the discussion on the RFC very interesting, 
to get broader feedback.

>Also, this doesn't really involve some kind of AdaCore "business" issue, and 
>just increasing the number of commentators will not necessarily increase the 
>relative ratio of "heat" vs. "light" in such a syntax/aesthetics-oriented 
>discussion. ;-)

The syntax is just the tip of the iceberg.
The underlying semantics and utility of this feature is still very debated, 
and I would find it curious that ARG presses on this AI given all the 
diverging opinions and the general low interest for that feature. As well 
as the inherent conflict visible in Randy's arguments about this feature being 
mostly targeted at replacing the SPARK feature of Contract_Cases, while it's 
clearly a poor replacement for it if you ask SPARK users/developers.

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

From: Randy Brukardt
Sent: Wednesday, July 31, 2019  12:26 PM

>I'll just say it a last time: I did not ask for inclusion of this 
>feature in Ada. So your *YOU* does not apply to me.

You wrote a proposal for Contract_Cases in Ada, which Tucker forwarded to the 
ARG list on April 11, 2018. See the first item in the !appendix of AI12-0280-1.

Contract_Cases did not look appropriate for Ada. Since the ARG solves 
problems, rather than blindly adding features suggested by people, we started 
looking for alternative ways of supporting the functionality. Which leads us 
to the current point. Had there been no request to solve this problem, we 
would probably never have looked in this area.

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

From: Tucker Taft
Sent: Wednesday, July 31, 2019  12:25 PM

Actually, Yannick, you did send the following message in 2017:

From: Yannick Moy
Subject: Ada 202X - add contract cases
Date: September 30, 2017 at 9:06:05 AM GMT+3

Raph, please find attached the AI that I'd like you to propose for inclusion
in Ada 202X at the next ARG meeting. For the structure of the AI, I copied 
the one that Vasiliy sent recently, feel free to modify.

You should be able to get support for this AI from members of the "SPARK 
Language Design Group" that are also ARG members: Tuck, Steve, Florian. I 
believe Steve did most of the wording for contract cases in SPARK RM.

------

So Randy is right in thinking this was something we wanted for SPARK.  Here is 
the original AI, AI12-0280-1:

  http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0280-1.txt?rev=1.1

Here are the first few paragraphs of this AI:

!summary

Add an aspect, called contract cases, which allows to specify a contract by 
cases. The cases should be disjoint and complete.

!problem

It is very common to have specifications for a functionality which are best 
expressed as a set of incompatible cases. Expressing these as preconditions 
and postconditions is both not as clear as it could, and in general ignores 
the property that cases partition the input space. Examples of better ways 
to express specifications by cases are the tabular notation by Parnas and the
behaviors of JML (Java Modeling Language) or ACSL (ANSI/ISO C Specification 
Language).

!proposal

We propose to add a new aspect, called Contract_Cases, which allows to 
specify subprogram contracts by disjoint and complete cases. Contract cases 
can be used either in place of a precondition and postcondition, or in 
addition to them. Each case consists in a Boolean guard expression, evaluated 
at the same point as preconditions, and a Boolean consequence expression, 
evaluated at the same point as postconditions. For any given call, one and 
only one guard should evaluate to True. The corresponding consequence should 
evaluate to True. Other consequence expressions should not be evaluated. 
Consequence expressions should respect the same rules as postconditions with 
respect to use of 'Old and 'Result attributes.

-------

In the !problem you indicated this was a common issue, and you identified some 
analogous capabilities in JML and ACSL.  It sounds like your thinking has 
evolved over the past two years, but you can perhaps at least understand why
Randy was confused. ;-)

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

From: Tucker Taft
Sent: Wednesday, July 31, 2019  12:32 PM

Fair enough.  But if you do decide to "split" the discussion, it would be 
great if you would inform the ARG of your plan before doing so, and include
whatever links are needed to make it easy for ARG members to read your RFC.
Also, it is important to try to reflect the state of the ARG discussion for
the RFC audience.  Ideally you will try to explain the ARG rationale for the 
current proposal in so far as possible, or highlight parts of the AI that 
provide that rationale.  

My biggest concern is that this process devolves into two "teams" rather 
than being a true collaborative, joint effort.

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

From: Richard Wai
Sent: Wednesday, July 31, 2019  12:42 PM

I second this concern. In fact when I first saw this RFC process started, I 
was already concerned. The ARG exists for this purpose, and there are 
well-established mechanisms for having these discussions already. 

It's also frankly frustrating to see a proposal that was originally mine to 
begin-with attributed to an "RFC" which appears to come from thin-air with 
no reference to the ongoing discussion that lead to it.

I mean I don't really care about the credit (I don't support the idea anymore 
anyways), I just think it is the wrong approach to fork the discussion like 
that.

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

From: Randy Brukardt
Sent: Wednesday, July 31, 2019  1:08 PM

...
> My biggest concern is that this process devolves into two "teams" 
> rather than being a true collaborative, joint effort.

Agreed. Experience has shown that it is hard to move a discussion from one 
forum to another without losing most of the original participants. Ideally,
there would be only one forum with everyone involved. (Note that the original
intent was that no technical discussion occur on the ARG list, rather that all
such discussion would occur on Ada-Comment. That proved impossible to do, 
despite various attempts and inducements.)

At least the discussions on ARG and Ada-Comment end up filed in the same place 
(in the AIs). External discussions will likely be lost.

P.S. Technologically, it would make sense to change some or all of our forums 
once we've completed work on Ada 202x. For course, we would need our forums to
be vendor-independent. It doesn't make sense to make a major disruption toward
the end of a revision cycle.

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

From: Raphael Amiard
Sent: Thursday, August 1, 2019  5:56 AM

>Contract_Cases did not look appropriate for Ada. Since the ARG solves
>problems, rather than blindly adding features suggested by people, we
>started looking for alternative ways of supporting the functionality. Which
>leads us to the current point. Had there been no request to solve this
>problem, we would probably never have looked in this area.

not sure what you are arguing about at this stage:

1. Yannick asked for the potential inclusion of contract cases in Ada.
2. The ARG considered contract cases as-is as not fitting Ada (something 
   Yannick can even agree on I think)

3. The ARG designed a new feature/bunch of new features to replace it.

So far so good. What is *clearly* the missing link here, is the ARG asking 
proactively for feedback from the SPARK team, or the SPARK team asking about
the result of the ARG work, to see whether the feature actually solves their
problems or not, *before* standardizing it.

That's an endemic ARG problem that I've pointed out many times in the past. 
So rather than fight amongst ourselves, it might be time to just ask 
ourselves the question: Does this solve any problem for anybody, and if it 
doesn't, why would we keep it ?

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

From: Tucker Taft
Sent: Thursday, August 1, 2019  6:47 AM

>So far so good. What is *clearly* the missing link here, is the ARG asking 
>proactively for feedback from the SPARK team, or the SPARK team asking about
>the result of the ARG work, to see whether the feature actually solves their
>problems or not, *before* standardizing it.

I guess we presumed that the author of the AI would look at how it evolved.  
This one was tricky because it was handed off a couple of times, so the link 
back to the author got lost (and apparently got completely forgotten by the 
original author ;-).  So this one did go through an unusual path without 
enough connection back to the original author, at least with hindsight.  Note 
that both Steve and I are pretty familiar with the use of Contract_Cases, and 
we both felt this AI was a reasonable way to provide the functionality, but we
probably should have tracked down Yannick and asked him specifically to 
comment, because of the various handoffs involved.

>That's an endemic ARG problem that I've pointed out many times in the past. 

I think the ARG does make mistakes, but this AI is somewhat special given the 
torturous route it took.  Generally we focus on problem statements when we 
receive proposals for new language features.  We find that it is rare that 
the original syntax proposed ultimately works in the larger context of the 
language as a whole.

>So rather than fight amongst ourselves, it might be time to just ask 
>ourselves the question: Does this solve any problem for anybody, and if it 
>doesn't, why would we keep it ?

That is certainly a worthwhile question. Our belief was that the boolean-based 
"case" had essentially all of the useful features of the Contract_Cases, 
without what we perceived as some of the downsides.  Of course we are always 
making these tradeoffs, but we are busy enough that we presume those 
interested in particular features will keep track of what the ARG is doing.  
Clearly we have overestimated the degree to which this happens, and so we are
considering some way of making a bit more of a "splash" when the ARG moves 
one or more AIs to the "intent" stage.

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

From: Yannick Moy
Sent: Thursday, August 1, 2019  5:04 AM

>Actually, Yannick, you did send the following message in 2017:

Thanks Tuck for having a better memory than me!
So indeed, I proposed this AI in 2017, and participated in the discussions on 
this in 2018, which apparently lead to a new separate AI 0214.

While I would have been happy to see SPARK Contract_Cases included in Ada, 
the new proposal does not cut it for SPARK users. Since it seems to be the 
main target for this AI, I don't think keeping the current direction makes 
sense anymore.

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

From: Yannick Moy
Sent: Thursday, August 1, 2019  5:49 AM

We'd like to restate the goal of the ada-spark-rfcs website, as stated in the 
README which is the first thing you see on that website:

- get people's feedback on new proposed features
- give people the opportunity to propose new features / improvements / fixes

So the audience of this website is on purpose much wider than the audience of 
the ARG mailing-list.

These two groups need not be concerned by the same problems. What we're trying 
to do with the RFC website is prepare work for the ARG, by exploring many 
ideas and see what sticks. Yes, we might discuss syntax to make things more 
concrete, but we don't intend to have the final word on that. Like for this AI 
which I originally submitted to ARG, ARG will be responsible ultimately for 
new features of Ada including syntax.

We're happy to see that our opening of the RFC website has led to many 
programmers within and outside AdaCore (from the Ada Community at large) 
participating in these discussions. We don't see that as a threat to the 
ARG or to Ada, on the contrary.

With this understanding, we think both groups should support each other, in 
their respective roles.

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

From: Randy Brukardt
Sent: Thursday, August 1, 2019  1:35 PM

> We'd like to restate the goal of the ada-spark-rfcs website, as stated 
> in the README which is the first thing you see on that website:
> 
> - get people's feedback on new proposed features
> - give people the opportunity to propose new features / improvements / 
> fixes
> 
> So the audience of this website is on purpose much wider than the 
> audience of the ARG mailing-list.

But it exactly the same purpose as the Ada-Comment mailing list, which exists 
for this purpose for many decades (certainly since 1998). Broad technical 
discussion is not supposed to occur on the ARG mailing list (it was 
supposed to only be throw-away topics like meeting announcements).

...
> We're happy to see that our opening of the RFC website has led to many 
> programmers within and outside AdaCore (from the Ada Community at 
> large) participating in these discussions.
> We don't see that as a threat to the ARG or to Ada, on the contrary.

But this is the primary purpose of the Ada-Comment mailing list. Siphoning 
these discussions away from ARG visibility (at a minimum because they are not 
recorded in the permanent record) is not likely to improve the resulting 
quality of work.

I realize that the quality/quantity of discussions on Ada-Comment have 
declined in recent years, but it would be more helpful to the ARG mission to 
figure out solutions to this issue that don't fracture the community (not 
everyone is comfortable interacting with a site clearly run and slanted 
toward a single vendor).

> With this understanding, we think both groups should support each 
> other, in their respective roles.

The goal all along was that there was only one group (the Ada community).
The more different places things are discussed, the more fractured the 
discussions are. It probably is OK to discuss detailed wording on the ARG 
list, but pretty much everything else should be on Ada-Comment (or it's 
permanent, independent, archived, replacement).

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

From: Randy Brukardt
Sent: Thursday, August 1, 2019  2:03 PM

...
>While I would have been happy to see SPARK Contract_Cases included in 
>Ada, the new proposal does not cut it for SPARK users. Since it seems 
>to be the main target for this AI, I don't think keeping the current 
>direction makes sense anymore.

The problem I see here is that if we don't give SPARK users an alternative
that works in Standard Ada, then there is going to be strong pressure for 
Ada vendors to support Contract_Cases in their compilers. This is worse 
outcome than actually including the feature in the Ada Standard, as 
everyone will have slightly different versions of it.

So what *would* be acceptable to SPARK users, or is it "our way or the 
highway"???

Contract_Cases is a special case feature that rather goes against the grain 
of the usual building block approach of Ada. Ada doesn't provide semaphores,
it provides protected objects to build them and much more. Ada doesn't 
provide managed strings, it provides array operations and libraries to build 
them and much more. The places where we didn't do this (streaming, for
instance) have usually proved limiting or frustrating.

You said yesterday(?) that the dynamic checking of Contract_Cases is useful.
It seems likely that it would be useful in contexts other than the single one 
of postconditions. So we're trying to introduce a building block to allow 
people get this checking in appropriate places. Such a building block could 
be used to replace Contract_Cases where portable Ada code is needed, but also 
has other uses.

I don't want to be in a situation where SPARK can essentially add any 
ill-conceived feature and essentially force every Ada vendor to support it.
That quickly would devalue the Ada Standard, the critical goals of Ada, and 
essentially lead to a situation where Ada itself is irrelevant and "just 
another language".

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

From: Randy Brukardt
Sent: Thursday, August 1, 2019  2:27 PM

...
>So far so good. What is *clearly* the missing link here, is the ARG 
>asking proactively for feedback from the SPARK team, or the SPARK team 
>asking about the result of the ARG work, to see whether the feature 
>actually solves their problems or not, *before* standardizing it.
>	
>That's an endemic ARG problem that I've pointed out many times in the 
>past.

This is the first time I heard this from you, so I don't know who you've been 
pointing it out to. It's always been an indirect criticism from anonymous 
sources ("some people working on SPARK").

The ARG has always functioned as much as possible in public, with meeting 
minutes, technical discussions, AIs (that is, proposals), and even the draft 
Standard posted publicly. I added a web site log last year to make it even 
clearer when new things are posted (http://www.ada-auth.org/log.html),
partly in response to the anonymous concerns. There also is the Ada 202x 
status page, which shows clearly the state of the various proposals 
(http://www.ada-auth.org/ai-files/grab_bag/2020-Amendments.html).

Our presumption has been that interested parties would follow along. It's not 
really practical to "proactively ask for feedback" because most proposals end 
up having elements from many different sources - so who do you ask for 
feedback from and how? Almost any place that you could ask tends to be of 
like-minded people so it is very hard to get feedback from a broad spectrum 
of users. We need the views of the Ada community as a whole, not just SPARK 
users or GNAT users or the old foogies on comp.lang.ada. ;-)

It's certainly true that we could always do better, and Steve and I are always 
open to suggestions for improvements. Perhaps there is some way to make 
proposals that are nearing completion more visible. I personally would
*love* to see more public feedback; I've tried to make Ada-Comment as 
welcoming as possible for that but obviously have not succeeded for the most 
part.

In any case, the ARG procedures and work flow were not handed down on stone 
tablets! They can and have evolved over the years and can evolve more. It 
almost always works best to change institutions from the inside rather than
causing a fork that always carries resentments with it.

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

From: Steve Baird
Sent: Thursday, August 1, 2019  2:35 PM

> But it [has] exactly the same purpose as the Ada-Comment mailing list

I agree that there is some overlap between the purposes of the Ada-Comment 
mailing list and the ada-spark-rfcs portal, but I think there are also some
important differences (ignoring the obvious difference regarding the treatment 
of SPARK).

One such difference is that AdaCore has committed to investing resources to 
evaluating and refining proposals that come in through the latter channel, 
with the goal of stimulating Ada language design discussion (and, in 
particular, attracting ideas from folks who, for whatever reasons, have chosen 
not to use Ada-Comment).

As Randy points out, the ada-spark-rfcs portal is sponsored by a single vendor 
and, as such, certainly should not replace Ada-Comment. On the other hand, if 
someone wants to take advantage of this new option that AdaCore is offering, 
why would anyone want to discourage that?

There is the practical issue of fragmented discussions getting distributed 
over multiple forums.

We've seen this in cases involving the ada-spark-rfcs site and the ARG list 
(e.g., the discussion of improving the parameter profile for Put_Image), but
this seems no worse than what we have seen in the past with Ada-Comment and 
the ARG list.

It might be a problematic new source of confusion if we started seeing ongoing 
discussions of similar topics on both Ada-Comment and the ada-spark-rfcs 
portal. To my knowledge, this has not been a problem in practice. And if it 
does arise, the cost would still have to be weighed against the overall 
benefit of the new portal.

Similarly, if lots of other Ada stakeholders each decided to adopt this 
approach, that proliferation of forums could be a problem; we'll cross that 
bridge in the unlikely event that we ever come to it.

This does mean that ARG-list subscribers now need to look one more place in 
order to keep up with what is going on, but if this new portal can in fact 
help with stimulating constructive discussion then that seems like a small 
price to pay.

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

From: Richard Wai
Sent: Thursday, August 1, 2019  3:13 PM

> One such difference is that AdaCore has committed to investing 
> resources to evaluating and refining proposals that come in through 
> the latter channel, with the goal of stimulating Ada language design 
> discussion (and, in particular, attracting ideas from folks who, for 
> whatever reasons, have chosen not to use Ada-Comment).
> 
> As Randy points out, the ada-spark-rfcs portal is sponsored by a 
> single vendor and, as such, certainly should not replace Ada-Comment. 
> On the other hand, if someone wants to take advantage of this new 
> option that AdaCore is offering, why would anyone want to discourage that?

This is a problem though. Many new-comers to the community often wrongly see 
AdaCore as the owner of Ada. As someone who is active in the more contemporary 
communities (such as Reddit), I can tell you that far too many newcomers to Ada
genuinely believe that AdaCore's "GNAT Community" is the only free Ada compiler
available. This harms Ada adoption because many people dismiss Ada for not 
being free. Rust is popular because anyone can grab the fully free compiler 
and write anything, including commercial software, with zero hindrance. Same
goes for Java, C, C++, Python, GO, et al.

I do not think AdaCore trying to set up their own "rfc" mechanism will help 
people understand that Ada is not owned by anyone.

If AdaCore committed resources to helping the ARG set-up something, I might 
appreciate that "investment" of resources. Otherwise it just looks like a 
marketing ploy.

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

From: Randy Brukardt
Sent: Thursday, September 5, 2019  3:13 PM

> As Randy points out, the ada-spark-rfcs portal is sponsored by a 
> single vendor and, as such, certainly should not replace Ada-Comment.

I note that there are more than 90 valid e-mail addresses joined to 
Ada-Comment, so clearly a large number of people get the e-mails from that 
list and can participate in discussions. Obviously, many of them have not 
chosen to participate in discussions there for whatever reason, and it would 
be valuable to find out what could stimulate more discussion.

Ideally, we would put general feature discussions on the Ada-Comment list, 
whereas stuff like detailed wording discussions and adminstrative stuff would 
stay here. But we've already learned that moving a discussion is impossible, 
and discussions that morph from wording to syntax to goodness inevitably end 
up on the wrong forum.

> This does mean that ARG-list subscribers now need to look one more 
> place in order to keep up with what is going on, but if this new 
> portal can in fact help with stimulating constructive discussion then 
> that seems like a small price to pay.

I think Richard covered this pretty well.

At some point pretty soon we'll need to move from mailing lists to some other 
sort of technology (forums, perhaps), for no other reason than the mailing 
list software is old and running here -- which won't be possible forever 
(I hope I'm not still doing this in 2040, unlike John :-)

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

From: Yannick Moy
Sent: Thursday, August 8, 2019  5:55 AM

I would like to officially take back the proposal made under AI12-0280-1 to 
include something like the SPARK Contract_Cases feature in Ada.

This is by no means to defy the ARG, or to dismiss the work done since then to 
include this proposal in a better proposal for Ada. I'm grateful that the ARG 
took the time to consider this proposal, but we discussed it at length inside 
and outside AdaCore (see comments on the RFC) and concluded that the proposed 
feature does not seem to be a good match for either SPARK users or Ada users.

I fully recognize that it's up to the ARG to independently assess whether to 
abandon this AI. I hope that the discussion we initiated brought enough 
information for that.

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

Questions? Ask the ACAA Technical Agent