Observational purity

[Don]

On 30.08.2011 17:31, bearophile wrote:
> I've found a nice paper, "99.44% pure: Useful Abstractions in Specifications", By Mike Barnett, David A. Naumann, Wolfram Schulte, Qi Sun (Microsoft Research, 2004):
>
> http://www.cs.ru.nl/ftfjp/2004/Purity.pdf
>
> It presents yet another kind of purity, "observational purity", such methods are meant to be used inside contracts. It is quite different from the usual definition of purity and less strict.
>
>> When specifications contain expressions that change the state of the
>> program, then the meaning of the program may differ depending on
>> whether or not the specifications are present; the two are no longer
>> independent. [...] We propose a definition of observational purity
>> and a static analysis to determine it. The intuition behind
>> observational purity is that a function is allowed to have
>> side-effects only if they are not observable to callers of the
>> function. [...] Our prototypical example of an observationally pure
>> function is one that maintains an internal cache. Changing this
>> internal cache is a side-effect, but it is not visible outside of
>> the object. Other examples are methods that write to a log file that
>> is not read by the rest of the program and methods that perform lazy
>> initialization.

I didn't understand this line of the paper. Although what they propose 
clearly works for caching, I don't see how it can possibly apply to the 
log file example.

If caching is the _only_ case which is required, it can be implemented 
strictly with a special pure-aware AA, where the only access to the AA 
is a tiny piece of code:
get(Params p, pure func)
{
   static __pureAA;
   val =_pureAA.get(p);
   if (val) return *val;
   return __pureAA[p] = func(p);
}
 >> Algorithms that are optimized for amortized
>> complexity, such as a list that uses a “move to front” heuristic,
>> also perform significant state updates that are not visible
>> externally. Observationally pure methods often occur in library
>> code that is highly optimized and also frequently used in
>> specifications, e.g., the equality methods in a string library.<
>
> So a strongly pure function with memoization becomes observationally pure :-)
> This seems useful.
>
> Time ago I have suggested a "trusted purity" to allow the implementation of pure function with memoization, but this observational purity seems better.
>
> Bye,
> bearophile