Abstract
This paper formalizes a small object-oriented programming notation. The notation features imperative commands where objects can be shared (aliased), and is rich enough to allow subtypes and recursive object types. The syntax, type checking rules, axiomatic semantics, and operational semantics of the notation are given. A soundness theorem showing the consistency between the axiomatic and operational semantics is also given. A simple corollary of the soundness theorem demonstrates the soundness of the type system. Because of the way types, fields, and methods are declared, no extra effort is required to handle recursive object types.
Chapter PDF
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
Martin Abadi and Luca Cardelli. A Theory of Objects. Springer-Verlag, 1996.
Martin Abadi and K. Rustan M. Leino. A logic of object-oriented programs. In 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, April 1997.
Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, September 1993.
Pierre America and Frank de Boer. Reasoning about dynamically evolving process structures. Formal Aspects of Computing, 6(3):269–316,1994.
Craig Chambers. The Cecil language: Specification & rationale, version 2.1, March 7, 1997. Available from http://www.cs.washington.edu/research/projects/ce cil/www/Papers/cecil-spec.html, 1997.
Krishna Kishore Dhara and Gary T. Leavens. Forcing behavioral subtyping through specification inheritance. Technical Report TR #95-20c, Iowa State University, Department of Computer Science, 1997.
Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ, 1976.
James Gosling, Bill Joy, and Guy Steele. The Java™ Language Specification. Addison-Wesley, 1996.
C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580,583, October 1969.
Kevin Lano and Howard Haughton. Object-Oriented Specification Case Studies. Prentice Hall, New York, 1994.
Gary Todd Leavens. Verifying Object-Oriented Programs that Use Subtypes. PhD thesis, MIT Laboratory for Computer Science, February 1989. Available as Technical Report MIT/LCS/TR-439.
K. Rustan M. Leino. Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, January 1995. Available as Technical Report Caltech-CS-TR-95-03.
K. Rustan M. Leino. Ecstatic: An object-oriented programming language with an axiomatic semantics. In The Fourth International Workshop on Foundations of Object-Oriented Languages, January 1997. Proceedings available from http:/ /www.cs.indiana.edu/hyplan/pierce/fool/.
K. Rustan M. Leino. Recursive object types in a logic of oject-oriented programs. Technical Note 1997-025a, Digital Equipment Corporation Systems Research Center, January 1998.
K. Rustan M. Leino and Greg Nelson. Object-oriented guarded commands. Internal manuscript KRML 50, Digital Equipment Corporation Systems Research Center, March 1995.
Greg Nelson. Verifying reachability invariants of linked structures. Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, pages 38–47, January 1983.
Greg Nelson, editor. Systems Programming with Modula-3. Sries in Innovative Technology. Prentice-Hall, Englewood Cliffs, NJ, 1991.
Arnd Poetzsch-Heffter and Peter Müller. A logic for the verification of object-oriented programs. In R. Berghammer and F. Simon, editors, Programming Languages and Fundamentals of Programming. Christian Albrechts-Universität Kiel, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rustan, K., Leino, M. (1998). Recursive object types in a logic of object-oriented programs. In: Hankin, C. (eds) Programming Languages and Systems. ESOP 1998. Lecture Notes in Computer Science, vol 1381. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0053570
Download citation
DOI: https://doi.org/10.1007/BFb0053570
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64302-9
Online ISBN: 978-3-540-69722-0
eBook Packages: Springer Book Archive