[RFC] Exclusive if-then-else

[yannickmoy]

Link to file: https://github.com/yannickmoy/ada-spark-rfcs/blob/exclusive_if_then_else/considered/exclusive_if_then_else.rst

[raph-amiard]

Thoughts:

1. This proposal is a lot better than the ARG one, because it doesn't overload the case statement with something that is essentially an if statement.
2. I still doubt it is very useful in general, or that people will actually think to use it outside of the very specific SPARK use case.
3. I have one general question: Do you ever want an if expression in a post condition that doesn't behave like the one you're describing ?

A syntax based on case is ill-advised if Ada is ever to support richer pattern-matching, which should be using a case syntax. The feature discussed under this RFC is not pattern-matching.

Yes * 100000000000

So general feedback: If we really have to have such a feature, this proposal is better. I doub't either is really required for Ada and outside the scope of SPARK though.

[yannickmoy]

For me, a critical point is that the current ARG proposal imposes a runtime cost that many programmers won't accept, by forcing evaluation of all guards. That's what I avoid here, unless assertions are enabled.

The fact that it's mostly useful for SPARK users does not make it less interesting to include in Ada IMO. That was the case for expression functions and quantified expressions, and will be the case for declare expressions.

[raph-amiard]

The fact that it's mostly useful for SPARK users does not make it less interesting to include in Ada IMO. That was the case for expression functions and quantified expressions, and will be the case for declare expressions.

Yes but those are widely different: They provide an expressivity benefit on top of being useful for proof. orif expressions on the other hand don't seem to me like they will be widely useful outside of the context of proof.

[mosteo]

I have sporadically have had this necessity in regular Ada. But what about making it xorif? Too ugly?

On Sat, Jul 27, 2019, 16:39 Raphaël AMIARD notifications@github.com wrote:

The fact that it's mostly useful for SPARK users does not make it less interesting to include in Ada IMO. That was the case for expression functions and quantified expressions, and will be the case for declare expressions.

Yes but those are widely different: They provide an expressivity benefit on top of being useful for proof. orif expressions on the other hand don't seem to me like they will be widely useful outside of the context of proof.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/AdaCore/ada-spark-rfcs/pull/25?email_source=notifications&email_token=AACAROOW2NZL4YX6RBFE32TQBRM3JA5CNFSM4IG6XNFKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD26MUQI#issuecomment-515689025, or mute the thread https://github.com/notifications/unsubscribe-auth/AACARONRQWROJILDJX7JA2LQBRM3JANCNFSM4IG6XNFA .

[yannickmoy]

I like 'xorif', it is even more explicit than 'orif' in terms of its semantics, and is so further away from 'elsif' that it's hard to imagine confusing them. The question @mosteo is whether it's worth adding in Ada. My feeling is like you, that it would provide a nice specification add-on.

@raph-amiard to me this feature is about specification: to say that your if-elsif sequence is about disjoint conditions, which makes it easier to review the code and helps detect errors should the conditions not be disjoint (could be by static analysis, but also by testing or review!)

[QuentinOchem]

This is inspiring @yannickmoy. In my personal experience, elsif often actually expresses orif / xorif - it might even be the most common meaning. Being able to specify the disjoint intent and providing dynamic and static means of verification sounds very promising.

I have a slight itch not having to symmetric notations and would like to put xelsif in the list of potential reserved words, as in "exclusive else".

[yannickmoy]

xelsif is also a good alternative to orif or xorif. It has the benefit that it's closer to what people use (elsif) so it's a minimal cognitive effort to change to that. The drawback is that it is indeed closer so people could miss the difference. But as I said, we do use or/xor without mistaking one for the other.

[briot]

xelsif is also a good alternative to orif or xorif. It has the benefit that it's closer to what people use (elsif) so it's a minimal cognitive effort to change to that. The drawback is that it is indeed closer so people could miss the difference. But as I said, we do use or/xor without mistaking one for the other.

Would “or elseif” (to match “or else”) work ?

I am not sure I would ever use that feature in practice, but I can see the benefits for proof.

[yannickmoy]

@briot that's indeed a way to avoid introducing a new keyword. But then xor elsif would work better as we're talking of mutually exclusive conditions here.

[Fabien-Chouteau]

My two cents as a programmer without language design background or knowledge of many programming languages...

I don't understand what the proposed orif/xorif is supposed to do. I understood the original AI syntax immediately, and I actually only understand what is being discussed in this RFC because of the original AI.

The relationship between orif, elsif, else is not clear at all to me. Reading the code I don't know what to expect during execution.

a programmer is likely to need from time to time

I cannot think of a single time where I needed this.

If I understand correctly, the only difference with a classic if statement is the exclusive property of the conditions. In that case I find the case version to be more explicit, because I already know that case requires exclusive conditions.

The feature of "exclusive if" is one that is missing in all mainstream programming languages

This doesn't necessarily sound like a positive argument for me. It could mean that the code will not be readable for most developers.

[pmderodat]

@Fabien-Chouteau Thanks for the feedback! I agree that using case makes it clear about exclusivity than orif, however as Yannick said in his proposal, this could easily conflict with a future extension for pattern matching in Ada. I would be very much disappointed if this new feature closed the door for using case to implement pattern matching, as I find pattern matching much more useful than this exclusive if-then-else extension.

What do you think about Yannick’s last proposall? Something like xor else/xor elsif) would make the exclusivity much more explicit (xor litterally means exclusive or) and has the advantage of not adding new keywords/reserved identifiers.

Besides, I just thought about another disadvantage of using case: the fact that the clause are all booleans makes it odd, because for now, one expects when clauses in case blocks to contain exclusive values, whereas here one or several clauses would evaluate to False.

[clairedross]

It is an interesting idea, though I am not sure I would use it in practice. Compared to a normal, non exclusive, if statement, I think it still suffers from a runtime penality (and also maybe a readability issue) in the sense that users would potentially have to repeat part of their previous conditions in the following ones to make them exclusive (it is something that I feel I often need to do when using Contract_Cases). I think a pattern which is sometimes used to avoid the problem of big if statements with conditions too far away, is to add some assertions at the beginning of the bloc. These assertions will typically repeat previous conditions, so that they are available to the reviewer, but having them only as assertions, and not as actual conditions, facilitate readability and avoids the runtime cost needed to evaluate them. This idea gives a different syntax, which maybe is a bit far from the proposed RFC:

if Condition1 then elsif Condition2 knowning not Condition3 then ... end if;

We could imaging turning the "knowing ..." part into an assertion at runtime, and possibly having exclusivity checks to show that Condition1 and (Condition2 and Condition3) are exclusive.

[Fabien-Chouteau]

What do you think about Yannick’s last proposall? Something like xor else/xor elsif) would make the exclusivity much more explicit (xor litterally means exclusive or) and has the advantage of not adding new keywords/reserved identifiers.

@pmderodat orif vs xorif vs xor elsif is not the problem for me here .The problem is the relation between orif, elsif, else.

   if condition_1 then
   elsif condition_2 then
   orif condition_3 then
   else
   end if;

What are the conditions that have to be exclusive here?

Maybe it would be more clear if the entire if statement is marked as exclusive:

   exclusive if condition_1 then
   elsif condition_2 then
   elsif condition_3 then
   else
   end if;

[pmderodat]

Maybe it would be more clear if the entire if statement is marked as exclusive:

Ah yes, so far I assumed that an if block would be either all exclusive, or not at all. :-) I agree that mixed configurations are confusing.

(now I’ll let people who have actually dealt with mutually exclusive conditions address @clairedross's interesting remark :))

[kanigsson]

I agree with @Fabien-Chouteau that this proposal is of doubtful value. Coupling if-statements or if-expressions with this notion of exclusivity is very troubling because if-statements are already exclusive (by their nature of testing the conditions in order). It is much more natural indeed for case statements/expressions.

But even if case is used for this exclusivity, I don't see much value in this feature. The only place where we have seen value for the exclusiveness property is in Contract_Cases, which in addition contains a notion of 'Old, which would be difficult to add to the syntax which is proposed here.

[yannickmoy]

@pmderodat @Fabien-Chouteau the use of regular or exclusive if-then-else is indeed one-or-the-other. The RFC says: "These two forms are mutually exclusive in an if-statement/expression."

[yannickmoy]

@kanigsson the inadequacy of this feature to replace Contract_Cases is precisely what I reported to ARG about the original AI

[kanigsson]

@yannickmoy I know, so I see even less the value of this feature.

[egilhh]

I don't know how complex these contract cases can be, but the example in the AI could be written with existing (Ada 2012) syntax:

function T_Increment (X : T) return T with
  Global    => null,
  Pre       => X /= Max,
  Post      =>
    (case X.Seconds'Old is
       when Seconds_T'Last =>
          (case X.Minutes'Old is
              when Minutes_T'Last =>
                 T_Increment'Result.Seconds = 0
                    and then T_Increment'Result.Minutes = 0
                    and then T_Increment'Result.Hours = X.Hours + 1,
              when others =>
                 T_Increment'Result.Seconds = 0
                    and then T_Increment'Result.Minutes = X.Minutes + 1
                    and then T_Increment'Result.Hours = X.Hours),
       when others =>
          T_Increment'Result.Seconds = X.Seconds + 1
            and then T_Increment'Result.Minutes = X.Minutes
            and then T_Increment'Result.Hours = X.Hours);

More complex expressions can be handled this way:

function T_Increment (X : T) return T with
  Global    => null,
  Pre       => X /= Max,
  Post      =>
    (case Boolean'(X.Seconds'Old = Seconds_T'Last) is
       when True =>
          (case Boolean'(X.Minutes'Old = Minutes_T'Last) is
              when True =>
                 T_Increment'Result.Seconds = 0
                    and then T_Increment'Result.Minutes = 0
                    and then T_Increment'Result.Hours = X.Hours + 1,
              when False =>
                 T_Increment'Result.Seconds = 0
                    and then T_Increment'Result.Minutes = X.Minutes + 1
                    and then T_Increment'Result.Hours = X.Hours),
       when False =>
          T_Increment'Result.Seconds = X.Seconds + 1
            and then T_Increment'Result.Minutes = X.Minutes
            and then T_Increment'Result.Hours = X.Hours);

or even:

type Relation is (Less_Than, Equals, Greater_Than);
function Test_Relation(Left, Right : Some_Type) return Relation;

    (case Test_Relation(Expression_1, Expression_2) is
       when Less_Than => 
          Stuff,
       when Equals =>
          Other_Stuff,
       when Greater_Than => 
          More_Stuff);

I don't think this is too hard to read. Any new syntax should really stand out as an improvement in readability, and I don't see how rewriting this to an if/orif/xorif/exclusive if will add anything in that department. But as I said, I don't know how complex these things can get...

[raph-amiard]

I agree with @Fabien-Chouteau that this proposal is of doubtful value. Coupling if-statements or if-expressions with this notion of exclusivity is very troubling because if-statements are already exclusive (by their nature of testing the conditions in order). It is much more natural indeed for case statements/expressions.

I agree with this. The more I think about it, the more I think that I don't like either of the proposals :)

[yannickmoy]

@egilhh While it is feasible to express contracts with complex nexted if-then-else or case-expression, with 'Old sprinkled where needed, it's not as clear as a Contract_Cases like we have in SPARK, so I think there is no need for pushing that feature to Ada just for this reason.

The value I see is really to augment regular if-expressions/statements with stronger specifications.

[sttaft]

The proposal currently being considered by the ARG looks like:

case select when X < Y => ... when X = Y => ... when X > Y => ... end case;

There no danger that this will somehow interfere with a possible pattern matching version of "case," which will certainly have an expression against which pattern matching will occur.

As far as interaction with 'Old, there is a separate AI about that (AI12-0280-2), which actually makes this more interesting because using this kind of "case" in a postcondition with 'Old will require that the condition choices themselves refer only to read-only inputs or 'Old of read-write input, which gives you something nicely approximating Contract_Cases, without some of the complexity of Contract_Cases, which actually spans pre- and postconditions. At least that was the intent! ;-)

Here is a link to AI12-0280-2: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0280-2.txt?rev=1.4

Take care, -Tuck

On Tue, Jul 30, 2019 at 5:26 AM Johannes Kanig notifications@github.com wrote:

I agree with @Fabien-Chouteau https://github.com/Fabien-Chouteau that this proposal is of doubtful value. Coupling if-statements or if-expressions with this notion of exclusivity is very troubling because if-statements are already exclusive (by their nature of testing the conditions in order). It is much more natural indeed for case statements/expressions.

But even if case is used for this exclusivity, I don't see much value in this feature. The only place where we have seen value for the exclusiveness property is in Contract_Cases, which in addition contains a notion of 'Old, which would be difficult to add to the syntax which is proposed here.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/AdaCore/ada-spark-rfcs/pull/25?email_source=notifications&email_token=AANZ4FLV3WCOIA6KARPOX23QCACLRA5CNFSM4IG6XNFKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD3DLZHA#issuecomment-516340892, or mute the thread https://github.com/notifications/unsubscribe-auth/AANZ4FNS2KHGVZ2X4KAJBH3QCACLRANCNFSM4IG6XNFA .

[egilhh]

The proposal currently being considered by the ARG looks like:

case select 
   when X < Y => ... 
   when X = Y => ... 
   when X > Y => ... 
end case; 

FWIW, I like that a lot better than case is. But should it then also be end case select;?

[sttaft]

Using "end case select;" could work. But note that all Ada loops end with "end loop []" whether they are "while ... loop" or "for ... loop" or our proposed loop with a filter "for ... when loop ..." so I believe we could justify saying that all kinds of case statements end with simply "end case;". In general Ada has gone with "end" markers that are somewhat simpler than the sequence of reserved words that introduce a construct.

Take care, -Tuck

On Tue, Jul 30, 2019 at 10:59 AM egilhh notifications@github.com wrote:

The proposal currently being considered by the ARG looks like:

case select when X < Y => ... when X = Y => ... when X > Y => ... end case;

FWIW, I like that a lot better than case is. But should it then also be end case select;?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/AdaCore/ada-spark-rfcs/pull/25?email_source=notifications&email_token=AANZ4FKPQZEI7QDQGQXA3STQCBJN3A5CNFSM4IG6XNFKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD3EILLY#issuecomment-516457903, or mute the thread https://github.com/notifications/unsubscribe-auth/AANZ4FPUQQSMGDXW5VTOJFLQCBJN3ANCNFSM4IG6XNFA .

[sttaft]

On Tue, Jul 30, 2019 at 9:20 AM Tucker Taft tucker@yaletaft.com wrote:

...

Here is a link to AI12-0280-2: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0280-2.txt?rev=1.4

Actually, that version of AI12-0280-2 is a bit out of date. We were not completely happy with the terminology in that version, so here is a rewritten version with different terminology that we are considering:

---

!standard 6.1.1(24/3) 19-07-09 AI12-0280-2/06 !standard 6.1.1(26.4/4) !standard 6.1.1(39/5) !class Amendment 18-05-15 !status work item 18-05-15 !status received 18-05-14 !priority Low !difficulty Medium !subject Making 'Old more flexible !summary

X’Old may be used in a conditionally evaluated subexpression so long as the condition controlling the subexpression can be evaluated on entry yielding the same result.

!problem

The restrictions on the use of 'Old in conditionally evaluated subexpressions can make it hard to properly express complex postconditions, or can make the evaluation of such postconditions expensive (by requiring the saving of a large object rather than a single, smaller, part).

Additionally, the requirement to evaluate all 'Old prefixes can be expensive (for example, if the object is large or has controlled parts), especially if some of them are in mutually exclusive subexpressions of the postcondition.

!proposal

We define the term "known-on-entry subexpression" to describe expressions that can be evaluated at the point of evaluation of 'Old, getting the same value without side-effects that would be determined when evaluated as part of the postcondition expression.

We then use that to define the term "determined to be unevaluated" to be used on subexpressions in a postcondition that are not going to evaluated given the value of the known-on-entry subexpression. (Note: which subexpressions are determined to be unevaluated is calculated at runtime; this term is referring to a Dynamic Semantics property.)

Finally, we use the above terms to define when parts of the postcondition are evaluated and when the prefix of Old attribute references is not evaluated.

!wording

Replace 6.1.1(20/3-24/3) with the following:

A subexpression of a postcondition expression is /known on entry/ if it is any of:

• a static subexpression (see 4.9);

• a literal whose type does not have any Integer_Literal, Real_Literal, or String_Literal aspect specified, or, the function specified by such an attribute has aspect Global specified to be null;

  AARM Reason: We mention literals explicitly in case they are not static (as when their subtype is not static, they are the literal null, etc.). We exclude literals of types with the aspects that are not Global => null those cause a user-written subprogram with possible side-effects to be called.

• a name statically denoting a full constant declaration of a type for which all views are constant (see 3.3);

  AARM Ramification: Constants of types with immutably limited or controlled parts are not allowed by this rule. Generic formal in objects are allowed by this rule (as they are defined to be full constant declarations).

  AARM Reason: We only want things that cannot be changed. We can't just say "constant" since that includes views of variables in some cases (for instance, a dereference of an access to constant object can be a view of a variable). There are other things we could have allowed (like a loop parameter), but having a subprogram declaration where those could be used (like inside of a loop seems unusual enough to not be worth defining).

• a name statically denoting a non-aliased /in/ parameter of an elementary type;

  AARM Ramification: All such parameters are by-copy, so the value won't change during the execution of the expression.

• an Old attribute_reference;

• an invocation of a predefined operator where all of the operands are known on entry;

• a function call where the function has aspect Global => null where all of the actual parameters are known on entry;

  AARM Reason: Such a function can only depend on the values of its parameters.

• a selected component of a known-on-entry prefix;

• an indexed component of a known-on-entry prefix where all index expressions are known on entry;

• a parenthesized known-on-entry expression;

• a qualified expression or type conversion whose operand is a known-on-entry expression;

• a conditional expression where all of the conditions, selecting_expressions, choice_conditions, and dependent_expressions are known on entry.

  AARM Discussion: It's OK if such an expression raises an exception, so long as every evaluation of the expression raises the same exception.

  A subexpression of a postcondition expression is /unconditionally evaluated/, /conditionally evaluated/, or /repeatedly evaluated/. The following subexpressions are repeatedly evaluated:

  • A subexpression of a predicate of a quantified_expression;

  • A subexpression of the expression of an array_component_association;

  • A subexpression of the expression of an container_element_association.

  If a subexpression is not repeatedly evaluated, and not evaluated unconditionally, then it is /conditionally evaluated/, and there is a set of /determining expressions/ that determine whether the subexpression is actually evaluated at run time. Such subexpressions and their determining expressions are as follows:

  • For an if_expression that is not repeatedly evaluated, a subexpression of any part other than the first condition is conditionally evaluated, and its determining expressions include all conditions of the if_expression that precede the subexpression textually;

  • For a case_expression that is not repeatedly evaluated, a subexpression of any dependent_expression is conditionally evaluated, and its determining expressions include the selecting_expression, or all of the choice_conditions, of the case_expression;

  • For a short-circuit control form that is not repeatedly evaluated, a subexpression of the right-hand operand is conditionally evaluated, and its determining expressions include the left-hand operand of the short-circuit control form;

  • For a membership test that is not repeatedly evaluated, a subexpression of a membership_choice other than the first is conditionally evaluated, and its determining expressions include the tested_simple_expression and the preceding membership_choices of the membership test.

  A conditionally evaluated subexpression is /determined to be unevaluated/ at run time if its set of determining expressions are all known on entry, and when evaluated on entry their values are such that the given subexpression is not evaluated.

  AARM Ramification: To be precise, a conditionally evaluated expression is determined to be unevaluated (including all of its subexpressions) under the following circumstances:

  • Within an if_expression, a dependent_expression with an associated condition that evaluates to False, or a condition or dependent_expression where a condition of a preceding part of the if_expression evaluates to True;
  • Within a case_expression, a dependent_expression with a discrete_choice_list that is not covered by the value of the selecting_expression, or has a choice_condition that evaluates to False;
  • The right-hand operand of a short-circuit control form where the left-hand operand evaluates to False for AND THEN or True for OR ELSE;
  • A membership_choice of a membership test where the individual membership test defined by any prior membership_choice evaluates to True.

Modify 6.1.1.(26/4):

Each X'Old in a postcondition expression that is enabled{, other than those that occur in subexpressions that are determined to be unevaluated,} denotes a constant that is implicitly declared at the beginning of the subprogram body, entry body, or accept statement.

{AARM Ramification: If X'Old occurs in a subexpression that is determined to be unevaluated, then there is no associated constant, and no evaluation of the prefix takes place. In general, this will require evaluating one or more known-on-entry subexpressions before creating and initializing any X'Old constants. Note that any 'Old in a known-on-entry subexpression evaluated this way represents the current value of the prefix (the 'Old itself can be ignored).}

Modify 6.1.1(27/5):

Reference to this attribute is only allowed within a postcondition expression. The prefix of an Old attribute_reference shall not contain a Result attribute_reference, nor an Old attribute_reference, nor a use of an entity declared within the postcondition expression but not within the prefix itself (for example, the loop parameter of an enclosing quantified_expression). The prefix of an Old attribute_reference shall statically name an entity{, unless the attribute_reference is unconditionally evaluated, or is conditionally evaluated where all of the determining expressions are known on entry}.

{AARM Ramification: The prefix of an Old attribute_reference has to statically name an entity if it appears within a repeatedly evaluated expression.}

Add after 6.1.1(39/5):

Implementation Permissions

An implementation may evaluate known-on-entry subexpression of a postcondition expression of an entity at the place where X'Old constants are created for the entity, with the normal evaluation of the postcondition expression, or both.

AARM Reason: We allow the evaluation of known-on-entry subexpressions when they might be needed to determine whether to create a particular 'Old constant. We allow them to be evaluated later as well, or for the results to be saved somehow. This permission shouldn't matter, as the results ought to be same wherever they are evaluated and there should not be any side-effects. The main effect of the permission is to determine when any exceptions caused by such subexpressions may be raised. We never require waiting to determine the value of such subexpressions, even if they aren't used to determine the creation of a constant for 'Old.

!discussion

This proposal addresses some of the same problems that the proposed Contract_Cases aspect does (see AI12-0280-1). Contract_Cases is not a great fit for Ada since it potentially requires a complex static check that its alternatives cover the precondition (provided by SPARK and GNATProve). Without such a check, it modifies the precondition, making it difficult for the caller to be sure what the precondition actually is.

Rather than introducing a new construct that has the needed properties, we instead look to improve the existing description of postconditions to better match the sorts of problems that Contract_Cases handles. We do this in two parts, first, by changing the evaluation of 'Old to avoid extra evaluations and the Legality Rules needed to make those make sense (this AI), and by expanding the abilities of case expressions (and statements), in AI12-0214-2.

!example

Consider:

procedure Proc (A : access Integer) with Post => (if A /= null then (A.all'Old > 1 and A.all > 1));

In Ada 2012, the reference A.all'Old is illegal as the prefix does not statically denote an object (required as the "then" dependent_expression is conditionally evaluated).

With the proposed AI, since "A /= null" meets the requirements of a known-on-entry expression (A being an in parameter of an elementary type), there is no restriction on the use of 'Old, and if A = null, then the 'Old reference is not evaluated at all. This allows the author to write the postcondition they want with less likelihood of tripping over these rules (and as a side-effect, requires less evaluation of 'Old prefixes that are never going to be used).

!ASIS

No ASIS effect.

!ACATS test

ACATS C-Tests are needed to check that the new capabilities are supported, specifically that (A) the restriction on 'Old prefixes is not enforced on a dependent expression that is not conditionally evaluated by these rules; (B) that the prefix of 'Old is not evaluated when it is determined to be unevaluated.

!appendix

[AdaDoom3]

I agree with raph-amiard 's point that this does not seem like a feature many will use outside of very specific cases and as a code reader encountering it for the first time I would have little clue what it is doing. For the purposes of readability and because it seems so specialized I don't support this proposal.

[yannickmoy]

Given the many contradicting views on that feature, we decided it's not of sufficient value for either Ada or SPARK users, and we're closing this RFC.