Re: SPARK

["Peter C. Chapin" <pcc482719@gmail.com>]

Yannick Duchêne (Hibou57) wrote:

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

If it works properly, yes, but what if it doesn't?

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

While this might be possible, it does sound rather complicated. I can see why
SPARK doesn't currently go down this path.

Peter