Abstract
We define NanoJava, a kernel of Java tailored to the investigation of Hoare logics. We then introduce a Hoare logic for this language featuring an elegant approach for expressing auxiliary variables: by universal quantification on the outer logical level. Furthermore, we give simple means of handling side-effecting expressions and dynamic binding within method calls. The logic is proved sound and (relatively) complete using Isabelle/HOL.
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 K. R. M. Leino. A logic of object-oriented programs. In Theory and Practice of Software Development, volume 1214 of Lect. Notes in Comp. Sci., pages 682–696. Springer-Verlag, 1997.
P. America and F. de Boer. Proving total correctness of recursive procedures. Information and Computation, 84:129–162, 1990.
K. R. Apt. Ten years of Hoare logic: A survey — part I. ACM Trans. on Prog. Languages and Systems, 3:431–483, 1981.
S.A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 7(1):70–90, 1978.
G. A. Gorelick. A complete axiomatic system for proving assertions about recursive and non-recursive programs. Technical Report 75, Department of Computer Science, University of Toronto, 1975.
M. Huisman. Java program verification in Higher-order logic with PVS and Isabelle. PhD thesis, University of Nijmegen, 2001.
M. Huisman and B. Jacobs. Java program verification via a Hoare logic with abrupt termination. In Fundamental Approaches to Software Engineering, volume 1783 of Lect. Notes in Comp. Sci., pages 284–303. Springer-Verlag, 2000.
A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), Oct. 1999. Full version in ACM Transactions on Programming Languages and Systems (TOPLAS), 2001.
B. Jacobs and E. Poll. A logic for the Java Modeling Language JML. In H. Hussmann, editor, Fundamental Approaches to Software Engineering, volume 2029 of Lect. Notes in Comp. Sci., pages 284–299. Springer-Verlag, 2001.
T. Kleymann. Hoare logic and VDM: Machine-checked soundness and completeness proofs. Ph.D. Thesis, ECS-LFCS-98-392, LFCS, 1998.
T. Kleymann. Hoare logic and auxiliary variables. Formal Aspects of Computing, 11:541–566, 1999.
T. Kowaltowski. Axiomatic approach to side effects and general jumps. Acta Informatica, 7:357–360, 1977.
K. R. M. Leino. Ecstatic: An object-oriented programming language with an axiomatic semantics. In Fourth International Workshop on Foundations of Object-Oriented Programming (FOOL 4), 1997.
J. Morris. Comments on “procedures and parameters”. Undated and unpublished.
T. Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. In V. Chandru and V. Vinay, editors, Foundations of Software Technology and Theoretical Computer Science, volume 1180 of Lect. Notes in Comp. Sci., pages 180–192. Springer-Verlag, 1996.
T. Nipkow. Hoare logics for recursive procedures and unbounded nondeterminism. Draft, 2001.
T. Nipkow. Hoare logics in Isabelle/HOL. In Proof and System-Reliability, 2002.
T. Nipkow, D. v. Oheimb, and C. Pusch. μJava: Embedding a programming language in a theorem prover. In F. Bauer and R. Steinbrüggen, editors, Foundations of Secure Computation, pages 117–144. IOS Press, 2000. http://isabelle.in.tum.de/Bali/papers/MOD99.html.
T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. http://www4.in.tum.de/~nipkow/LNCS2283/.
D. v. Oheimb. Hoare logic for mutual recursion and local variables. In C. P. Rangan, V. Raman, and R. Ramanujam, editors, Foundations of Software Technology and Theoretical Computer Science, volume 1738 of Lect. Notes in Comp. Sci., pages 168–180. Springer-Verlag, 1999. http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html.
D. v. Oheimb. Analyzing Java in Isabelle/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Technische Universität München, 2001. http://www4.in.tum.de/~oheimb/diss/.
D. v. Oheimb. Hoare logic for Java in Isabelle/HOL. Concurrency and Computation: Practice and Experience, 13(13), 2001. http://isabelle.in.tum.de/Bali/papers/CPE01.html.
A. Poetzsch-Heffter. Personal communication, Aug. 2001.
A. Poetzsch-Heffter and P. Müller. A programming logic for sequential Java. In S. Swierstra, editor, Programming Languages and Systems (ESOP’ 99), volume 1576 of Lect. Notes in Comp. Sci., pages 162–176. Springer-Verlag, 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
von Oheimb, D., Nipkow, T. (2002). Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited. In: Eriksson, LH., Lindsay, P.A. (eds) FME 2002:Formal Methods—Getting IT Right. FME 2002. Lecture Notes in Computer Science, vol 2391. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45614-7_6
Download citation
DOI: https://doi.org/10.1007/3-540-45614-7_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43928-8
Online ISBN: 978-3-540-45614-8
eBook Packages: Springer Book Archive