Observational purity and encapsulation

Research output: Contribution to journalConference articlepeer-review

13 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 strongly 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 and extends a recently proposed notion of observational purity, reducing the proof obligation to a familiar one for equivalence of two class implementations.

Original languageEnglish
Pages (from-to)190-204
Number of pages15
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3442
DOIs
StatePublished - 2005
Event8th International Conference on Fundamental Approaches to Software Engineering, FASE 2005, held as part of the Joint Conferences on Theory and Practice of Software, ETAPS 2005 - Edinburgh, United Kingdom
Duration: 4 Apr 20058 Apr 2005

Fingerprint

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

Cite this