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

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;

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