Abstract
This paper outlines a sound and complete Hoare logic for a sequential object-oriented language with inheritance and subtyping like Java. It describes a weakest precondition calculus for assignments and object-creation, as well as Hoare rules for reasoning about (mutually recursive) method invocations with dynamic binding. Our approach enables reasoning at an abstraction level that coincides with the general abstraction level of object-oriented languages.
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
Poetzsch-Heffter, A., Müller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 162–176. Springer, Heidelberg (1999)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12, 576–580 (1969)
Pierik, C., de Boer, F.S.: A syntax-directed Hoare logic for object-oriented programming concepts. Technical Report UU-CS-2003-010, Institute of Information and Computing Sciences, Utrecht University, The Netherlands (2003), Available at http://www.cs.uu.nl/research/techreps/UU-CS-2003-010.html
Kowaltowski, T.: Axiomatic approach to side effects and general jumps. Acta Informatica 7, 357–360 (1977)
Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley, Reading (1996)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06u, Department of Computer Science, Iowa State University (2003)
de Boer, F.S.: A wp-calculus for OO. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 135–149. Springer, Heidelberg (1999)
de Boer, F., Pierik, C.: Computer-aided specification and verification of annotated object-oriented programs. In: Jacobs, B., Rensink, A. (eds.) FMOODS V, pp. 163–177. Kluwer Academic Publishers, Dordrecht (2002)
Reus, B., Wirsing, M., Hennicker, R.: A Hoare calculus for verifying Java realizations of OCL-constrained design models. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 300–317. Springer, Heidelberg (2001)
von Oheimb, D.: Hoare logic for Java in Isabelle/HOL. Concurrency and Computation: Practice and Experience 13, 1173–1214 (2001)
Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer, Heidelberg (2000)
Abraham-Mumm, E., de Boer, F., de Roever, W., Steffen, M.: Verification for Java’s reentrant multithreading concept. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 5–20. Springer, Heidelberg (2002)
Distefano, D., Katoen, J.P., Rensink, A.: On a temporal logic for object-based systems. In: Smith, S.F., Talcott, C.L. (eds.) FMOODS III, pp. 305–326. Kluwer Academic Publishers, Dordrecht (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this paper
Cite this paper
Pierik, C., de Boer, F.S. (2003). A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts. In: Najm, E., Nestmann, U., Stevens, P. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2003. Lecture Notes in Computer Science, vol 2884. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39958-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-39958-2_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20491-6
Online ISBN: 978-3-540-39958-2
eBook Packages: Springer Book Archive