TY - JOUR
T1 - Observational purity and encapsulation
AU - Naumann, David A.
PY - 2007/5/15
Y1 - 2007/5/15
N2 - Practical specification languages for imperative and object-oriented programs, such as JML, Eiffel, and Spec#, allow the use of program expressions including method calls in specification formulas. For coherent semantics of specifications, and to avoid anomalies with runtime assertion checking, expressions in specifications and assertions are typically required to be weakly pure in the sense that their evaluation has no effect on the state of preexisting objects. For specification of large systems using standard libraries this restriction is impractical: it disallows many standard methods that mutate state for purposes such as caching or lazy initialization. Calls of such methods can sensibly be used for specifications and annotations in contexts where their effects cannot be observed. This paper formalizes a notion of observational purity, justifies the use of weakly and observationally pure methods in specifications, and shows that a method is observationally pure if it simulates a weakly pure method.
AB - Practical specification languages for imperative and object-oriented programs, such as JML, Eiffel, and Spec#, allow the use of program expressions including method calls in specification formulas. For coherent semantics of specifications, and to avoid anomalies with runtime assertion checking, expressions in specifications and assertions are typically required to be weakly pure in the sense that their evaluation has no effect on the state of preexisting objects. For specification of large systems using standard libraries this restriction is impractical: it disallows many standard methods that mutate state for purposes such as caching or lazy initialization. Calls of such methods can sensibly be used for specifications and annotations in contexts where their effects cannot be observed. This paper formalizes a notion of observational purity, justifies the use of weakly and observationally pure methods in specifications, and shows that a method is observationally pure if it simulates a weakly pure method.
KW - Benevolent side effects
KW - Information hiding
KW - Specification and verification
UR - http://www.scopus.com/inward/record.url?scp=34247472572&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34247472572&partnerID=8YFLogxK
U2 - 10.1016/j.tcs.2007.02.004
DO - 10.1016/j.tcs.2007.02.004
M3 - Article
AN - SCOPUS:34247472572
SN - 0304-3975
VL - 376
SP - 205
EP - 224
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 3
ER -