Observational purity and encapsulation

Research output: Contribution to journalArticlepeer-review

28 Scopus citations

Abstract

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.

Original languageEnglish
Pages (from-to)205-224
Number of pages20
JournalTheoretical Computer Science
Volume376
Issue number3
DOIs
StatePublished - 15 May 2007

Keywords

  • Benevolent side effects
  • Information hiding
  • Specification and verification

Fingerprint

Dive into the research topics of 'Observational purity and encapsulation'. Together they form a unique fingerprint.

Cite this