Abstract
A Hoare-style programming logic for the sequential kernel of Java is presented. It handles recursive methods, class and interface types, subtyping, inheritance, dynamic and static binding, aliasing via object references, and encapsulation. The logic is proved sound w.r.t. an SOS semantics by embedding both into higher-order logic.
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
M. Abadi and K. R. M. Leino. A logic of object-oriented programs. In M. Bidoit and M. Dauchet, editors, TAPSOFT 1997: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France, volume 1214 of Lecture Notes in Computer Science, pages 682–696. Springer-Verlag, 1997.
P. Borras, D. Clement, T. Despeyroux, J. Incerpi, G. Kahn, B. Lang, and V. Pascual. CENTAUR: The system. In ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, SIGPLAN Notices 24(2), 1989.
M. J. C. Gordon. Mechanizing programming logics in higher order logic. In G. Birtwistle and P.A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag, 1989.
B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about Java classes. In Proceedings of Object-Oriented Programming Systems, Languages and Applications (OOPSLA), 1998. Also available as TR CSI-R9812, University of Nijmegen.
G. T. Leavens. An overview of Larch/C++: Behavioral specifications for C++ modules. In H. Kilov and W. Harvey, editors, Specification of Behavioral Semantics in Object-Oriented Information Modeling, chapter 8, pages 121–142. Kluwer Academic Publishers, Boston, 1996.
K. R. M. Leino. Ecstatic: An object-oriented programming language with an axiomatic semantics. In B. Pierce, editor, Proceedings of the Fourth InternationalWorkshop on Foundations of Object-Oriented Languages, 1997. Available from: http://www.cs.indiana.edu/hyplan/pierce/fool/.
P. M üller and A. Poetzsch-Heffter. Formal specification techniques for object-oriented programs. In M. Jarke, K. Pasedach, and K. Pohl, editors, Informatik 97: Informatik als Innovationsmotor, Informatik Aktuell. Springer-Verlag, 1997.
A. Poetzsch-Heffter. Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich, Jan. 1997. http://www.informatik.fernuni-hagen.de/pi5/publications.html.
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 (PROCOMET), 1998.
D. von Oheimb and T. Nipkow. Machine-checking the Java specification: Proving type-safety. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science. Springer, 1998. To appear.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Poetzsch-Heffter, A., Müller, P. (1999). A Programming Logic for Sequential Java. In: Swierstra, S.D. (eds) Programming Languages and Systems. ESOP 1999. Lecture Notes in Computer Science, vol 1576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49099-X_11
Download citation
DOI: https://doi.org/10.1007/3-540-49099-X_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65699-9
Online ISBN: 978-3-540-49099-9
eBook Packages: Springer Book Archive