Abstract
Behavioral semantics abstracts from implementation details and allows to describe the behavior of software components in a representation-independent way. In this paper, we develop a formal behavioral semantics for class-based object-oriented languages with aliasing, subclassing, and dynamic dispatch. The code of an object-oriented component consists of a class and the classes used by it. A component instance is realized by a dynamically evolving set of objects with a clear boundary to the environment. The behavioral semantics is expressed in terms of the messages crossing the boundary. It is defined as an abstraction of an operational semantics based on an ownership-structured heap. We show how the semantics can be used to define substitutability in a program independent way.
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
Ábrahám, E., Grüner, A., Steffen, M.: Abstract interface behavior of object-oriented languages with monitors. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol. 4037, pp. 218–232. Springer, Heidelberg (2006)
Back, R.-J., Mikhajlova, A., von Wright, J.: Class refinement as semantics of correct object substitutability. Formal aspects of computing 12(1), 18–40 (2000)
Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. Journal of the ACM 52(6), 894–960 (2005)
Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 54–84. Springer, Heidelberg (2004)
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6) (2004)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, Springer, Heidelberg (2005)
Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: Proc. OOPSLA 2002, pp. 211–230. ACM Press, New York (2002)
Broy, M.: A core theory of interfaces and architecture and its impact on object orientation. In: Reussner, R., Stafford, J.A., Szyperski, C.A. (eds.) Architecting Systems with Trustworthy Components. LNCS, vol. 3938, pp. 26–47. Springer, Heidelberg (2006)
Büchi, M.: Safe Language Mechanisms for Modularization and Concurrency. PhD thesis, Turku Centre for Computer Science (May 2000)
Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Jurdzinski, M., Mang, F.Y.C.: Interface compatibility checking for software modules. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 428–441. Springer, Heidelberg (2002)
Clarke, D.: Object Ownership and Containment. PhD thesis, University of New South Wales (July 2001)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC/FSE-9, pp. 109–120. ACM Press, New York (2001)
Flatt, M., Krishnamurthi, S., Felleisen, M.: A programmer’s reduction semantics for classes and mixins. Formal Syntax and Semantics of Java 1523, 241–269 (1999)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. TOPLAS 23(3), 396–450 (2001)
Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. Technical Report TR06-20a, Computer Science, Iowa State University (2006)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML a behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes 31(3), 1–38 (2006)
Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–516. Springer, Heidelberg (2004)
Liskov, B., Wing, J.: A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems 16(6), 1811–1841 (1994)
Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)
Nierstrasz, O.: Regular types for active objects. In: Proc. OOPSLA ’93, October 1993, pp. 1–15. ACM Press, New York (1993)
Poetzsch-Heffter, A., Geilmann, K., Schäfer, J.: Inferring ownership types for encapsulated object-oriented program components. In: Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm. LNCS, vol. 4444, Springer, Heidelberg (2007)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of LICS’02, pp. 55–74 (2002)
Rinetzky, N., Poetzsch-Heffter, A., Ramalingam, G., Sagiv, M., Yahav, E.: Modular shape analysis for dynamically encapsulated programs. In: ESOP’07. European Symposium on Programming, March 2007, Springer, Heidelberg (2007)
Schäfer, J., Poetzsch-Heffter, A.: A parameterized type system for simple loose ownership domains. Journal of Object Technology (to appear, 2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
Poetzsch-Heffter, A., Schäfer, J. (2007). A Representation-Independent Behavioral Semantics for Object-Oriented Components. In: Bonsangue, M.M., Johnsen, E.B. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2007. Lecture Notes in Computer Science, vol 4468. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72952-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-72952-5_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72919-8
Online ISBN: 978-3-540-72952-5
eBook Packages: Computer ScienceComputer Science (R0)