!standard 4.5.7(5/3) 19-09-04 AI12-0341-1/01 !standard 5.4(2/3) !standard 5.5.2(7/3) !class Amendment 19-0904 !status Amendment 1-2012 19-09-04 !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 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) @drepl @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @b@ @i@fa@b@hr @ @ @ @fa@ {,@hr @ @ @ @fa}> @dby @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @b@ @i@fa@ @b@hr @ @ @ @fa@ {,@hr @ @ @ @fa}@hr @ |@ @b@hr @ @ @ @fa@ {,@hr @ @ @ @fa}> !corrigendum 5.4(2/3) @drepl @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @b@ @i@fa@b@hr @ @ @ @ @ @ @ @fa@hr @ @ @ @ @ @ {@fa}@hr @ @ @ @b;> @dby @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @b@ @i@fa@ @b@hr @ @ @ @ @ @ @ @fa@hr @ @ @ @ @ @ {@fa}@hr @ @ @ @b;@hr @ |@ @b@hr @ @ @ @ @ @ @ @fa@hr @ @ @ @ @ @ {@fa}@hr @ @ @ @b;> !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: protected if then elsif ... end protected if; (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. > > protected if then > > elsif ... > end protected if; > > > (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 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 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 when .. => ...." to "case select when ... => ..." and make essentially no other change to the AI. ("" 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 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 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. ****************************************************************