On Fri, 9 Oct 2015, Maciej Sobczak wrote:

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

        case Thingsome(Something(E)) is -- this was "case E is"

>         when A => null;
>         when B => null;
>      end case;
>   end Test;

with some functions Thingsome and Something (X: Enum) return Enum.

> The Pre contract says that C is never used as a value for E. Still, 
> GNATProve complains about missing case value C in the case statement. 
> The compiler complains, too.

Well, your example is a triviality to prove.

But if Ada where required to deal with your example, why should it not 
also be required to deal with my example?

On the other hand, assume the program is technically correct. I.e., for 
all E /= C, the property

   Thingsome(Something(E)) /=C

actually holds. Do you really expect the Ada compiler to prove this?

SPARK should prove this, in principle. But, for sufficiently complicated 
functions Something and Thingsome, SPARKs success on proving this may 
depend on your settings (which theorem provers and how much time for 
proving you set). The legality of an Ada program should never depend on 
such settings. Everything else would kill portability.

And allowing SPARK to compile formally illegal Ada programs would very 
regrettably break the compability between SPARK and Ada -- even if there 
acutally where any "pure-SPARK-compilers" at all.

So long

Stefan


--------  I  love  the  taste  of  Cryptanalysis  in  the morning!  --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----