Re: SPARK

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Thu, 13 May 2010 11:28:03 +0200, <stefan-lucks@see-the.signature> a  
écrit:
> When working with SPARK, it is difficult *not* to face that. E.g.,
> usually, you would write a pseudorandom number generator as
>
>   function Rnd return T is
>   begin
>     Global_State := f(Global_State);
>     return g(Global_State);
>   end;
>
> In SPARK, you have to replace the function RND by a procedure, which
> delivers the result as an out parameter.

Yes, an example from Barnes gives the same:
Quote from  
http://people.cis.ksu.edu/~hatcliff/890-High-Assurance/Slides/Barnes-Ch-02-Language-Principles.pdf

    package Random_Numbers
    --# own Seed;
    --# initializes Seed;
    is

       procedure Random(X: out Float);
       --# global in out Seed;
       --# derives X, Seed from Seed;

    end Random_Numbers;

    package body Random_Numbers is

       Seed: Integer;
       Seed_Max: constant Integer := … ;

       procedure Random(X: out Float) is
       begin
          Seed := … ;
          X := Float(Seed) / Float(Seed_Max);
       end Random;

    begin -- initialization part
       Seed := 12345;
    end Random_Numbers


> Very inconvenient! But reasonable:

For that purpose, yes, as a radom generator is not a pure function.

> Note that the result from evaluating an expression such as "Rnd + Rnd**2"
> depends on the order of evaluation, which isn't specified in the Ada
> standard. If we write I for the initial global state, then "Rnd + Rnd**2"
> can either evaluate to
>
>   f(g(I) + f(f(g(I)))**2,
>
> or to
>
>   f(f(g(I))) + f(g(I))**2.
A function optimized (which save computing of already computed inputs)  
using memoisation, does not exposes this behavior.

> Such an unspecified behaviour makes static analysis very difficult. In
> principle, you would have to consider all possible orders of evaluation
> and check if something is going wrong. That would be very hard for SPARK,
> and, with a few legitimate exceptions, such that pseodorandom numbers,
> this is bad programming style anyway. Thus, SPARK prohibits this.
Indeed, there should not be any attempt to make proof on a language which  
would allow function whose result depends on the invokation time-stamp,  
and so whose result may depend on evaluation order.

Functions using memoisation are different case and are still pure  
function. What change between each invokation, is not the result, just the  
time to compute it (which may be shorter for some next invokation).

How to make it formal : may be giving the proof the function is the only  
one to access memoisation storage between function invokation, so, that  
this data are mechanically private to the function. Then, demonstrate  
there is two paths to the result : one which is the basic computation and  
one which retrieve the result of a similar previous computation. This  
latter step could rely on the computation of a key to access this data.  
Then demonstrate that for a given input, the computed key is always the  
same (input <-> key association). Now, the hard part may be to demonstrate  
the key is used to access the result which was computed previously for the  
same input that the one which was used to compute the key.

Obviously, the function should be the only one to access this data.

There is a concept in SPARK, the one of variable package and  
state-machines. May be there could be some room for a concept which could  
be something like function-package ?

Just some seed of an idea... will think about it some later day

-- 
pragma Asset ? Is that true ? Waaww... great