# Version 1.1 of ai12s/ai12-0214-2.txt

Unformatted version of ai12s/ai12-0214-2.txt version 1.1
Other versions for file ai12s/ai12-0214-2.txt

!standard 4.5.7(5/3)          18-05-16 AI12-0214-2/01
!standard 5.4(2/3)
!class Amendment 18-05-16
!status work item 18-05-16
!priority Low
!difficulty Easy
!subject Boolean conditional case expressions and statements
!summary
A new form of case expression/statement, called the Boolean conditional case, is introduced.
!problem
It is common, especially in postconditions, to write a series of mutually exclusion conditions. If those conditions can't be mapped to a case expression, then an if_expression has to be used, losing the mutually exclusive property of the conditions.
For example, we have to write:
(if X > 5 then ...
elsif X < 5 then ... elsif X = 6 then ...)
But the property that the choices are supposed to exclusive is lost, so the error above (6 rather than 5 in the last expression) is lost.
!proposal
A Boolean conditional case expression consists of a number of Boolean conditions. The conditions are assumed to be disjoint -- only one is true for any execution of a Boolean conditional case expression. If one is true, the associated dependent_expression is executed. If none are true or more than one are true, then Program_Error is raised.
The same basic rules applies to Boolean conditional case statements with dependent_expressions replaced by statements.
!wording
Replace 4.5.7(5/3):
case_expression ::= case selecting_expression is case_expression_alternative {, case_expression_alternative} | case is conditional_case_expression_alternative {, conditional_case_expression_alternative}
conditional_case_expression_alternative ::= when condition_list => dependent_expression
choice_condition ::= choice_expression
condition_choice_list ::= choice_condition {| choice_condition}
[Editor's note: We need "choice_condition" to avoid syntax ambiguity with memebrships]
Modify 4.5.7(14/3):
A condition is expected to be of any boolean type. A choice_condition is expected to be of type Boolean.
AARM Reason: We want all of the choices of a case expression to be of the same type.
Modify 4.5.7(21/3):
For the evaluation of a case_expression {with a selecting_expression}, the ...
For the evaluation of a case_expression without a selecting_expression, all of the choice_expressions are evaluated. If exactly one choice_expression is true, the dependent_expression of the conditional_case_expression_alternative containing the choice_condition that is True is is evaluated, converted to the type of the case_expression, and the resulting value is the value of the case_expression. Otherwise (no choice_expression is True, or multiple choice_expressions are True), then Program_Error is raised.
AARM Ramification: This is not a check! It can't be suppressed as we would not know what value to return in such a case. This is consistent with other case exceptions.
[I suppose we could declare this a check and let it be suppressed -- a new check name would be needed -- execution would be erroneous and implementers could do whatever. That would be different than other case errors but it might make sense in this case [groan - pun] given that the disjointness check could cause issues in fielded systems; and one might have used an external tool to prove that the check can't fail.]
-----
Similar changes need to be made to case statements in 5.4. They're sufficiently similar so that writing them doesn't seem worthwhile until we are about to adopt this AI.
!discussion
The disjointness exception could be a hazard in some cases. We could avoid that by making the rule be that the first choice_condition that is True is the one selected. But then there would be no advantage over a regular if expression. Part of the point of this feature is to tell external static analysis tools that these alternatives are disjoint -- if we didn't enforce that it really would not be true.
!example
The example in the Problem statement could be written:
(case is
when X > 5 => ... when X < 5 => ... when X = 6 => ...)
and Program_Error would be raised if X = 6 (two alternatives being selected), exposing the mistake.
-----
Along with AI12-0280-2, this new case expression greatly reduces the need for something like the Contract_Cases aspect as discussed in AI12-0280-1.
For instance, a Contract_Cases example of:
function T_Increment (X : T) return T with Global => null, Pre => X /= Max, Contract_Cases => (X.Seconds < Seconds_T'Last => T_Increment'Result.Seconds = X.Seconds + 1 and then T_Increment'Result.Minutes = X.Minutes and then T_Increment'Result.Hours = X.Hours,
X.Seconds = Seconds_T'Last and then X.Minutes < Minutes_T'Last => T_Increment'Result.Seconds = 0 and then T_Increment'Result.Minutes = X.Minutes + 1 and then T_Increment'Result.Hours = X.Hours,
X.Seconds = Seconds_T'Last and then X.Minutes = Minutes_T'Last => T_Increment'Result.Seconds = 0 and then T_Increment'Result.Minutes = 0 and then T_Increment'Result.Hours = X.Hours + 1);
Could be written as the following given the new facilities of this AI (we don't need AI12-0280-2 facilities in this example):
function T_Increment (X : T) return T with Global => null, Pre => X /= Max, Post => (case is when X.Seconds'Old < Seconds_T'Last => T_Increment'Result.Seconds = X.Seconds + 1 and then T_Increment'Result.Minutes = X.Minutes and then T_Increment'Result.Hours = X.Hours, when X.Seconds'Old = Seconds_T'Last and then X.Minutes'Old < Minutes_T'Last => T_Increment'Result.Seconds = 0 and then T_Increment'Result.Minutes = X.Minutes + 1 and then T_Increment'Result.Hours = X.Hours, when X.Seconds'Old = Seconds_T'Last and then X.Minutes'Old = Minutes_T'Last => T_Increment'Result.Seconds = 0 and then T_Increment'Result.Minutes = 0 and then T_Increment'Result.Hours = X.Hours + 1);
!ASIS
** New ASIS functions needed ** TBD.
!ACATS test
ACATS B- and C-Tests are needed to check that the new capabilities are supported.
!appendix
```
From: Randy Brukardt
Sent: Saturday, April 14, 2018  7:22 PM

...
> Alternative proposals are always of interest, but (as I'm sure you'd
> agree) ya gotta give me something more concrete than that.

I had an idea when I woke up this morning. So here's a quick outline of the
ideas (two).

... [Skipped the other idea, see AI12-0280-2 for that - Editor.]

For checking disjoint cases in a postcondition, I suggest the "alternative"
expression. (I thought about calling it "select", but then a statement version
is impossible, so I think it needs a new keyword.)

The example in the AI would look like using this (and the 'Old suggestion
above):

procedure Incr_Threshold_1 (X : in out Integer; Threshold : in Integer)
with Pre  => (X <= Threshold),
Post => (alternative
when X'Old < Threshold => X = X'Old + 1,
when X'Old = Threshold => X = Threshold);

I don't think we could reasonably overload "case" this way, thus a new keyword
is needed. The semantics would include a disjointness check (only one of the
choices could be true); otherwise it would essentially be an if statement and
the extra construct wouldn't help). One would expect static analysis tools to do
that check statically (and even a compiler could do that and warn
appropriately).

The full syntax would be something like:

(alternative
when <condition> {, <condition>} => <dependent_expression>{,
when <condition> {, <condition>} => <dependent_expression>)

It would be a conditional expression, so the same rules on resolution and
parens, and especially the 'Old rules proposed above, would apply.

This is better than the previous proposal because:
(1) More generally useful, anyone can use it anywhere (for instance, for
composite types);
(2) Doesn't mess with the model of Pre/Post;
(3) Doesn't harm the readability of the precondition for the caller (the more
important usage).

This last point is rather important. The caller needs to know what restrictions
there are on a call. A bunch of separate expressions is just confusing for that
purpose, especially when the set is actually complete and represent no
restriction.

For instance, if you have something like:

procedure Oper (X : in out Integer; Threshold : in Integer)
with Pre  => True,
Post => (alternative
when X'Old < Threshold => ...,
when X'Old = Threshold => ...,
when X'Old > Threshold => ...);

The alternatives represent no restriction on X at all. Having to look through a
mass of Contract_Cases to verify that is nasty. Consider the time example Tucker
sent earlier:

function T_Increment (X : T) return T with
Global         => null,
Pre            => X /= Max,
Contract_Cases =>
(X.Seconds < Seconds_T'Last
=>
T_Increment'Result.Seconds = X.Seconds + 1
and then T_Increment'Result.Minutes = X.Minutes
and then T_Increment'Result.Hours = X.Hours,

X.Seconds = Seconds_T'Last
and then X.Minutes < Minutes_T'Last
=>
T_Increment'Result.Seconds = 0
and then T_Increment'Result.Minutes = X.Minutes + 1
and then T_Increment'Result.Hours = X.Hours,

X.Seconds = Seconds_T'Last
and then X.Minutes = Minutes_T'Last
=>
T_Increment'Result.Seconds = 0
and then T_Increment'Result.Minutes = 0
and then T_Increment'Result.Hours = X.Hours + 1);
--  Provides part of S.count

Here the "cases" don't represent any restriction on X, but verifying that
(especially without any comments to that effect!!!) is difficult. (And the whole
point of using contracts is to get away from comments; if you need a comment to
describe the effective precondition, something is wrong!)

The suggestions I have allow writing the same thing without messing with the
precondition.

Anyway, my \$50 worth. (I wrote this note on-the-clock :-).

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

From: Tucker Taft
Sent: Sunday, April 15, 2018  9:24 PM

These are both interesting ideas.  The 'Old idea seems like a good improvement,
and probably not very controversial.

Some kind of uniqueness-requiring conditional expression/statement does seem an
interesting way to generalize Contract_Cases.  I am worried about "alternative"
as a new reserved word.  It feels like one of those words that might be used
heavily in some programs, probably as a type name.

An alternative to "alternative" might be "case is" -- that is, omit the
expression of a case statement.  Hence:

case is
when X > 5 => ...
when X = 5 => ...
when X < 5 => ...
end case;

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

```

Questions? Ask the ACAA Technical Agent