Observational purity

[bearophile]

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