Re: SPARK: missing case value

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Fri, 09 Oct 2015 10:39:01 -0400, Bob Duff wrote:

> 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.

Because the above is a proper contract, while precondition is a land mine.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de