On 31.08.2011 09:35, bearophile wrote:
Don:
If caching is the _only_ case which is required,
They have developed this observational purity plus a way to enforce it, to
allow static analyzability of contracts (so they are allowed to call only
observationally pure methods), while keeping them flexible enough.
That's not the impression I got, though I didn't read it very carefully.
It seemed to me that what they have, is a runtime check (an assert that
compares a read from a static variable, with a pure function; if they're
the same, then the static variable isn't providing any extra state). The
static analysis is used to ensure that the runtime check is always present.
They focused on the example of caching, but I found that a bit
misleading, since you can easily get some kind of "real" purity in that
case (there is no observable state AND there are no observable
side-effects).
But this is not true of other forms of observational purity. I do not
see how allowing a call to an impure function from inside a pure one,
could ever be anything other than a convention. So I don't see how the
logfile example could possibly be statically checked.
