Re: SPARK: missing case value

[Bob Duff <bobduff@theworld.com>]

Maciej Sobczak <see.my.homepage@gmail.com> writes:

> Consider:
>
>    type Enum is (A, B, C);
>
>    procedure Test (E : in Enum)
>       with Pre => E /= C
>    is
>    begin
>       case E is
>          when A => null;
>          when B => null;
>       end case;
>    end Test;

That's illegal Ada, as you noted.  And illegal SPARK.

But this works:

   type Enum is (A, B, C);
   subtype A_C is Enum with Predicate => A_C /= B;

   procedure Test (E : in A_C) is
   begin
      case E is
         when A => null;
         -- "when B" is not needed.
         when C => null;
      end case;
   end Test;

And that has the advantage that A_C need not be a subrange;
it can have holes.

I find that predicates are often better than preconditions,
because the same precondition often applies to many parameters,
and also to local variables.  The predicate allows you to avoid
repetition.

("Predicate =>" is a GNAT-specific extension.  In Ada, you need to
say "Static_Predicate =>".  IMHO the "Static_" part is just noise,
but I couldn't convince the rest of ARG.)

- Bob