Abstract
In object-oriented programming one distinguishes two kinds of languages. Class-based languages are centered around the concept of classes as descriptions of objects. In object-based languages the concept of a class is substituted by constructs for the creation of individual objects. Usually, the object-based languages attract interest because of their “simplicity”. This paper contains a thorough denotational analysis which reveals that simplicity is quickly lost if one tackles verification issues. This is due to what is sometimes called “recursion through the store”. By providing a denotational semantics for a simple class-based and a simple object-based language it is shown that the denotational semantics of the object-based language needs much more advanced domain theoretic machinery than the class based one. The gap becomes even wider when we define concepts of specification and appropriate verification rules.
partially supported by the EPSRC under grant GR/R65190/01 and by the Nuffield Foundation under grant NAL/00244/A
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi and L. Cardelli. A Theory of Objects. Springer Verlag, 1996.
M. Abadi and K. R. M. Leino. A logic of object-oriented programs. In Michel Bidoit and Max Dauchet, editors, Theory and Practice of Software Development: Proceedings / TAPSOFT’ 97, 7th International Joint Conference CAAP/FASE, volume 1214 of Lecture Notes in Computer Science, pages 682–696. Springer-Verlag, 1997.
J. Alves-Foss, editor. Formal Syntax and Semantics of Java, volume 1523 of Lect. Notes Comp. Sci. Springer, Berlin, 1999.
P. America and F. S. de Boer. A proof theory for a sequential version of POOL. Technical Report http://www.cs.uu.nl/people/frankb/Availablepapers/spool.dvi, University of Utrecht, 1999.
K. B. Bruce, L. Cardelli, and B. C. Pierce. Comparing object encodings. In Theoretical Aspects of Computer Software (TACS’97), Sendai, Japan, volume 1281, pages 415–438. Springer LNCS, September 1997.
C. Calcagno, S. Ishtiaq, and P. W. O’Hearn. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. In Principles and Practice of Declarative Programming. ACM Press, 2000.
C. Calcagno and P. W. O’Hearn. A logic for objects. Talk given in March 2001, 2001.
F. S. de Boer. A WP-calculus for OO. In W. Thomas, editor, Foundations of Software Science and Computations Structures, volume 1578 of Lecture Notes in Computer Science. Springer-Verlag, 1999.
A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java. A minimal core calculus for Java and GJ. In Object Oriented Programming: Systems, Languages and Applications (OOPSLA), volume 34, pages 132–146. ACM SIGPLAN Notices, 1999.
B. Jacobs and E. Poll. A monad for basic java semantics. In T. Rus, editor, Algebraic Methodology and Software Technology (AMAST’00), volume 1816 of LNCS, pages 150–164. Springer Verlag, 2000.
S. N. Kamin and U. S. Reddy. Two semantic models of object-oriented languages. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, pages 464–495. The MIT Press, 1994.
T. Nipkow and D. von Oheimb. Machine-checking the Java Specification: Proving Type-Saftey. In Alves-Foss [3].
L. C. Paulson. Logic and Computation, volume 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1987.
A. M. Pitts. Relational properties of domains. Information and Computation, 127:66–90, 1996. (A preliminary version of this work appeared as Cambridge Univ. Computer Laboratory Tech. Rept. No. 321, December 1993.).
A. Poetzsch-Heffter and P. Müller. Logical foundations for typed object-oriented languages. In D. Gries and W. De Roever, editors, Programming Concepts and Methods, 1998.
U. Reddy. Objects and classes in Algol-like languages. In FOOL 5, 1998. Available at URL http://pauillac.inria.fr/~remy/fool/proceedings.html.
B. Reus. A logic of recursive objects. In Formal Techniques for Java Programs, volume 251— 5/1999 of Informatik Berichte, pages 58–64. Fern Universität Hagen, 1999.
B. Reus. A logic of recursive objects (abstract). In S. Demeyer A. Moreira, editor, Object-oriented Technology, ECOOP’ 99 Workshop Reader, volume 1743 of Lecture Notes in Computer Science, page 107, Berlin, 1999. Springer.
B. Reus and Th. Streicher. Semantics and logics of objects. In Proceedings of the 17th Symp. Logic in Computer Science, 2002. To appear. Draft available from http://www.cogs.susx.ac.uk/users/bernhard/papers.html.
B. Reus, M. Wirsing, and R. Hennicker. A Hoare-Calculus for Verifying Java Realizations of OCL-Constrained Design Models. In FASE 2001, volume 2029 of Lecture Notes in Computer Science, pages 300–317, Berlin, 2001. Springer.
D. von Oheimb. Hoare logic for mutual recursion and local variables. In V. Raman C. Pandu Rangan and R. Ramanujam, editors, Found. of Software Techn. and Theoret. Comp. Sci., volume 1738 of LNCS, pages 168–180. Springer, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Reus, B. (2002). Class-Based versus Object-Based: A Denotational Comparison. In: Kirchner, H., Ringeissen, C. (eds) Algebraic Methodology and Software Technology. AMAST 2002. Lecture Notes in Computer Science, vol 2422. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45719-4_32
Download citation
DOI: https://doi.org/10.1007/3-540-45719-4_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44144-1
Online ISBN: 978-3-540-45719-0
eBook Packages: Springer Book Archive