Re: SPARK GPL 2012 and generic, any hint?

[Phil Thornley <phil.jpthornley@gmail.com>]

In article <slrnjvinh6.n7f.hugues@soekris-1.pinkyoogx.org>, 
hugues@soekris-1.pinkyoogx.org says...
> 
> Hi,
> 
> I tried SPARK GPL 2012 with a small example for generic, but I keep getting 
> syntax error, do I miss something obvious?
> 
> The documentation lacks a complete example that can be processed, all I could 
> find was limited code snippet :(
> 
> Here is the code source (code taken from SPARK GPL 2012 documentation, i
> I simply added package stuff around)
> 
> package Test is
> 
>    generic
>       type T1 is range <>;
>       type T2 is range <>;
>       --# check T1'Last * T1'Last <= T2'Last and
>       --#       T1'First * T1'First <= T2'Last and
>       --#       T1'First * T1'First >= T2'First;
>    function Square (X : T1) return T2;
>    --# return R => R = T2 (X * X);
> 
> end Test;
> 

The instantion check isn't supported yet, and the subprogram must be at 
library level.

The following code examines OK:

   generic
      type T1 is range <>;
      type T2 is range <>;
   function Square (X : T1) return T2;
   --# return R => R = T2 (X * X);

Cheers,

Phil