On Thu, 13 May 2010, Yannick Duch�ne (Hibou57) wrote:

> Functions may have legitimate side effects, like for memoisation. Memoisation
> is a kind of optimization and optimizations should be transparent to clients.
> SPARK would requires to split it into two parts: a kind of �prepare/compute�
> procedure and a �get result� function ; the procedure being supposedly invoked
> prior to each function invokation. Did you ever face this ?

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. 

Very inconvenient! But reasonable:

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.

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. 

-- 
------ Stefan Lucks   --  Bauhaus-University Weimar  --   Germany  ------
               Stefan dot Lucks at uni minus weimar dot de
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------