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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aldrich, J., Chambers, C.: Ownership domains: Separating aliasing policy from mechanism. In: European Conference on Object-Oriented Programming, pp. 1–25 (2004)
Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. Journal of the ACM (2002); Accepted, revision pending. Extended version of [3]
Banerjee, A., Naumann, D.A.: Representation independence, confinement and access control. In: ACM Symp. on Princ. of Program. Lang (POPL), pp. 166–177 (2002)
Banerjee, A., Naumann, D.A.: State based ownership, reentrance, and encapsulation. Submitted (December 2004)
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of objectoriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)
Barnett, M., Naumann, D.A., Schulte, W., Sun, Q.: 99.44% pure: Useful abstractions in specifications. In: ECOOP workshop on Formal Techniques for Java-like Programs (FTfJP), Technical Report NIII-R0426, University of Nijmegen (2004)
Calcagno, C., O’Hearn, P., Bornat, R.: Program logic and equivalence in the presence of garbage collection. Theoretical Comput. Sci. 298(3), 557–581 (2003)
Cavalcanti, A.L.C, Naumann, D.A.: Forward simulation for data refinement of classes. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 471–490. Springer, Heidelberg (2002)
Clarke, D., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: OOPSLA, pp. 292–310 (November 2002)
de Roever, W.-P., Engelhardt., K. (eds.): Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: ACM Conf. on Program. Lang. Design and Implementation (PLDI), pp. 234–245 (2002)
Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 262–284. Springer, Heidelberg (2003)
Meyer, B.: Object-oriented Software Construction, 2nd edn. Prentice Hall, NewYork (1997)
Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)
Müller, P.: Modular Specification and Verification of Object-Oriented Programs. In: Müller, P. (ed.) Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)
Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state (extended abstract). In: IEEE Symp. on Logic in Computer Science (LICS), pp. 313–323 (2004)
Pierik, C., Clarke, D., de Boer, F.S.: Creational invariants. In: Proceedings of ECOOP workshop on Formal Techniques for Java-like Programs (FTfJP), Technical Report NIII-R0426, University of Nijmegen (2004)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21(1), 5–19 (2003)
Sălcianu, A., Rinard, M.: A combined pointer and purity analysis for Java programs. Technical Report MIT-CSAIL-TR-949, Department of Computer Science, Massachusetts Institute of Technology (May 2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Naumann, D.A. (2005). Observational Purity and Encapsulation. In: Cerioli, M. (eds) Fundamental Approaches to Software Engineering. FASE 2005. Lecture Notes in Computer Science, vol 3442. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31984-9_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-31984-9_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25420-1
Online ISBN: 978-3-540-31984-9
eBook Packages: Computer ScienceComputer Science (R0)