Abstract
This paper formalises a semantics for statements and expressions (in sequential imperative languages) which includes non-termination, normal termination and abrupt termination (e.g. because of an exception, break, return or continue). This extends the traditional semantics underlying e.g. Hoare logic, which only distinguishes termination and non-termination. An extension of Hoare logic is elaborated that includes means for reasoning about abrupt termination (and side-effects). It prominently involves rules for reasoning about while loops, which may contain exceptions, breaks, continues and returns. This extension applies in particular to Java. As an example, a standard pattern search algorithm in Java (involving a while loop with returns) is proven correct using the proof-tool PVS.
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’97: Theory and Practice of Software Development, volume 1214 of LNCS, pages 682–696. Springer-Verlag, 1997.
K.R. Apt. Ten years of Hoare’s logic: A survey—part I. ACM Trans. on Progr. Lang. and Systems, 3(4):431–483, 1981.
K.R. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Springer, 2nd rev. edition, 1997.
K. Arnold and J. Gosling. The Java Programming Language. Addison-Wesley, 2nd edition, 1997.
E.A. Ashcroft, M. Clint, and C.A.R. Hoare. Remarks on “Program proving: jumps and functions by M. Clint and C.A.R. Hoare”. Acta Informatica, 6:317–318, 1976.
J.W. de Bakker. Mathematical Theory of Program Correctness. Prentice Hall, 1980.
J. van den Berg, M. Huisman, B. Jacobs, and E. Poll. A type-theoretic memory model for verification of sequential Java programs. Techn. Rep. CSI-R9924, Comput. Sci. Inst., Univ. of Nijmegen, 1999.
F.S. de Boer. A WP-calculus for OO. In W. Thomas, editor, Foundations of Software Science and Computation Structures, number 1578 in LNCS, pages 135–149. Springer, Berlin, 1999.
F. Christian. Correct and robust programs. IEEE Trans. on Software Eng., 10(2):163–174, 1984.
M. Clint and C.A.R. Hoare. Program proving: jumps and functions. Acta Informatica, 1:214–224, 1972.
M.J.C. Gordon. Programming Language Theory and its Implementation. Prentice Hall, 1988.
M.J.C. Gordon. Mechanizing programming logics in higher order logic. In Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag, 1989.
J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.
D. Gries. The Science of Programming. Springer, 1981.
W.O.D. Griffioen and M. Huisman. A comparison of PVS and Isabelle/HOL. In J. Grundy and M. Newey, editors, Proceedings of the 12 International Workshop on Theorem Proving in Higher Order Logics (TPHOLs’ 98), volume 1479 of LNCS, September 1998.
U. Hensel, M. Huisman, B. Jacobs, and H. Tews. Reasoning about classes in object-oriented languages: Logical models and tools. In Proceedings of European Symposium on Programming (ESOP), volume 1381 of LNCS, pages 105–121. Springer-Verlag, March 1998.
M. Huisman, B. Jacobs, and J. van den Berg. A case study in class library verification: Java’s Vector class (abstract). In B. Jacobs, G.T. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, Formal Techniques for Java Programs, volume 251-5/1999 of Informatik berichte FernUniversität Hagen, 1999.
B. Jacobs and E. Poll. A monad for basic Java semantics. Techn. Rep. CSI-R9926, Comput. Sci. Inst., Univ. of Nijmegen, 1999.
B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about classes in Java (preliminary report). In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pages 329–340. ACM Press, 1998.
G.T. Leavens, A.L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06c, Iowa State University, Department of Computer Science, January 1999.
K.R.M. Leino. Toward Reliable Modular Programs. PhD thesis, California Inst. of Techn., 1995.
R. Leino and J. van de Snepscheut. Semantics of exceptions. In E.-R. Olderog, editor, Programming Concepts, Methods and Calculi, pages 447–466. North-Holland, 1994.
S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T.A. Henzinger, editors, Computer-Aided Verification (CAV’ 96), volume 1102 of LNCS, pages 411–414, New Brunswick, NJ, July/August 1996. Springer-Verlag.
S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.
D. Parnas. A generalized control structure and its formal definition. Communications of the ACM, 26(8):572–581, 1983.
L.C. Paulson. Isabelle-a generic theorem prover, volume 828 of LNCS. Springer-Verlag, 1994. With contributions by Tobias Nipkow.
A. Poetzsch-Heffter and P. Müller. A programming logic for sequential Java. In S.D. Swierstra, editor, Programming Languages and Systems, LNCS, pages 162–176. Springer, Berlin, 1999.
J.C. Reynolds. Theories of Programming Languages. Cambridge University Press, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Huisman, M., Jacobs, B. (2000). Java Program Verification via a Hoare Logic with Abrupt Termination. In: Maibaum, T. (eds) Fundamental Approaches to Software Engineering. FASE 2000. Lecture Notes in Computer Science, vol 1783. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46428-X_20
Download citation
DOI: https://doi.org/10.1007/3-540-46428-X_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67261-6
Online ISBN: 978-3-540-46428-0
eBook Packages: Springer Book Archive