, 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
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.
Bye,
bearophile
, but you could. Observational purity only works because we restrict
ourselves to operations that are in the spirit of things like 'private
members' or 'log files'. Admittedly it is possible for a language/compiler
to disallow unsafe pointer operations, but not keep you from reading your
log
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
On 8/31/2011 7:55 AM, Marco Leise wrote:
Admittedly it is
possible for a language/compiler to disallow unsafe pointer operations, but not
keep you from reading your log files back in.
But that's purity by convention, not by static checking.
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
, 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
/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
On 8/30/2011 8:31 AM, bearophile wrote:
Time ago I have suggested a trusted purity to allow the implementation of
pure function with memoization, but this observational purity seems better.
observational purity seems like another word for logical const. This has
been debated here many times.
Walter Bright:
observational purity seems like another word for logical const. This has
been debated here many times.
They show how to enforce observational purity. I don't remember people
discussing this here.
They use observational purity just for methods called by contracts, to find
10 matches
Mail list logo
