--- ai12s/ai12-0214-2.txt 2018/06/12 05:28:47 1.3 +++ ai12s/ai12-0214-2.txt 2019/07/06 00:26:43 1.4 @@ -1,4 +1,4 @@ -!standard 4.5.7(5/3) 18-05-16 AI12-0214-2/01 +!standard 4.5.7(5/3) 19-06-15 AI12-0214-2/02 !standard 5.4(2/3) !class Amendment 18-05-16 !status work item 18-05-16 @@ -14,7 +14,7 @@ !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, +exclusive 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. @@ -28,8 +28,8 @@ !proposal -A Boolean conditional case expression consists of a number of Boolean -conditions. The conditions are assumed to be disjoint -- only one is true +A Boolean conditional case expression consists of a number of alternatives +guarded by Boolean conditions. The conditions are such that 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. @@ -64,8 +64,8 @@ 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. +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. @@ -79,10 +79,10 @@ 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 +containing this choice_condition 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. +choice_expressions are True), 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 @@ -95,11 +95,52 @@ could cause issues in fielded systems; and one might have used an external tool to prove that the check can't fail.] +Modify 4.9(12.1/3): + +a conditional_expression all of whose conditions, selecting_expressions, +choice_expressions, and dependent_expressions are static expressions; + +Modify 4.9(32.5/3): + +a dependent_expression of a case_expression whose associated choice_condition +is static and whose value evaluating to False; or + ----- + +Replace 5.4(2/3) with: -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. +case_statement ::= + case selecting_expression is + case_statement_alternative + {case_statement_alternative} + end case; + | case is + conditional_case_statement_alternative + {conditional_case_statement_alternative} + end case; + +Add after 5.4(3) with: + +conditional_case_statement_alternative ::= + when condition_list => + sequence_of_statements + +Modify 5.4(11/3): + +For the execution of a case_statement {with a selecting_expression,} the +selecting_expression is first evaluated. + +Add after 5.4(13/3): + +For the evaluation of a case_statement without a selecting_expression, all +of the choice_expressions are evaluated. If exactly one choice_expression is +true, the sequence_of_statements of the conditional_case_statement_alternative +containing this choice_condition is executed. Otherwise (no choice_expression +is True, or multiple choice_expressions are True), 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. !discussion @@ -523,18 +564,18 @@ If you want to go this way, @ would be more appropriate: > For example: -> case is -> when X > 5 => ... -> when X = 5 => ... -> when X < 5 => ... -> end case; +> case is +> when X > 5 => ... +> when X = 5 => ... +> when X < 5 => ... +> end case; > > Could be: -> case X is -> when @ > 5 => ... -> when @ = 5 => ... -> when @ < 5 => ... -> end case; +> case X is +> when @ > 5 => ... +> when @ = 5 => ... +> when @ < 5 => ... +> end case; > ... ****************************************************************

Questions? Ask the ACAA Technical Agent