Abstract
Encapsulation is a major concept in object-oriented designs as design pattern catalogues, approaches for alias control, and the need for modular correctness of components demonstrate. The way encapsulation can be formally specified in existing approaches has several shortcomings. We show how encapsulation in sequential Java programs is specified by means of a new concept, called encapsulation predicates, in a clearly defined and comprehensible way, well fitting into the concept of design by contract. Encapsulation predicates extend existing functional specification languages. There are two kinds: basic predicates, which provide the actual extension, and convenience predicates, which are abbreviations for often used specification patterns. With encapsulation predicates, encapsulation properties in design patterns can be modelled and approaches to control aliasing can be simulated. Specifications containing encapsulation predicates are deductively checkable, but can also be tackled by static analysis methods which are similar to alias control approaches.
Chapter PDF
References
Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling 4, 32–54 (2005)
Almeida, P.S.: Controlling sharing of state in data types. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 32–59. Springer, Heidelberg (1997)
Baar, T.: The definition of transitive closure with OCL – limitations and applications. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 358–365. Springer, Heidelberg (2004)
Beckert, B.: A dynamic logic for the formal verification of Java Card programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol. 2041, pp. 6–24. Springer, Heidelberg (2001)
Boyland, J.: Alias burying: Unique variables without destructive reads. Software – Practice and Experience 31(6), 533–553 (2001)
Buschmann, F., Meunier, R., Rohnert, H., Sommerlad, P., Stal, M.: Pattern- Oriented Software Architecture - A System of Patterns. John Wiley and Sons, Chichester (1996)
Clarke, D., Potter, J., Noble, J.: Ownership types for flexible alias protection. In: ACM Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA’98), Vancouver, Canada (October 1998)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)
Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn. Addison-Wesley, Reading (2000)
Grand, M.: Patterns in Java, volume 1 and 2. John Wiley & Sons, Chichester (1998, 1999)
Gries, D., Schneider, F.B.: Avoiding the undefined by underspecification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 366–373. Springer, Heidelberg (1995)
Hogg, J.: Islands: Aliasing protection in object-oriented languages. In: Conference proceedings on Object-oriented programming systems, languages, and applications, pp. 271–285. ACM Press, New York (1991)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06z, Iowa State University, Department of Computer Science, See (December 2004), http://www.jmlspecs.org
Meyer, B.: Applying “design by contract”. IEEE Computer 25(10), 40–51 (1992)
Müller, P.: Modular specification and verification of object-oriented programs. Springer, New York (2002)
Nelson, G.: Verifying reachability invariants of linked structures. In: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 38–47. ACM Press, New York (1983)
Noble, J., Biddle, R., Tempero, E., Potanin, A., Clarke, D.: Towards a model of encapsulation. In: International Workshop on Aliasing, Confinement, and Ownership (IWACO), Darmstadt, Germany (July 2003)
Roth, Schmitt, P.H.: Ensuring invariant contracts for modules in java. In: Proceedings of the ECOOP Workshop FTfJP 2004 Formal Techniques for Java-like Programs, June 2004. NIII-R0426 in Technical Report, University of Nijmegen, pp. 93–102 (2004)
Vitek, J., Bokowski, B.: Confined types in Java. Software – Practice and Experience 31(6), 507–532 (2001)
Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modelling with UML. Object Technology Series/MA. Addison-Wesley, Reading (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 IFIP International Federation for Information Processing
About this paper
Cite this paper
Roth, A. (2005). Specification and Verification of Encapsulation in Java Programs. In: Steffen, M., Zavattaro, G. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2005. Lecture Notes in Computer Science, vol 3535. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11494881_13
Download citation
DOI: https://doi.org/10.1007/11494881_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26181-0
Online ISBN: 978-3-540-31556-8
eBook Packages: Computer ScienceComputer Science (R0)