Abstract
This paper examines Java’s exception mechanism, and formalises its main operations (throw, try-catch and try-catch-finally) in a type-theoretic setting. This formalisation uses so-called coalgebras for modeling Java statements and expressions, thus providing a convenient setting for handling the various termination options that may arise in exception handling (closely following the Java Language Specification). This semantics of exceptions is used within the LOOP project on Java program verification. It is illustrated in two example verifications in PVS.
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
J. Alves-Foss and F. S. Lam. Dynamic denotational semantics of Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, number 1523 in Lect. Notes Comp. Sci., pages 201–240. Springer, Berlin, 1998.
J. van den Berg, M. Huisman, B. Jacobs, and E. Poll. A type-theoretic memory model for verification of sequential Java programs. In D. Bert, C. Choppy, and P. Mosses, editors, Recent Trends in Algebraic Development Techniques, number 1827 in Lect. Notes Comp. Sci., pages 1–21. Springer, Berlin, 2000.
J. van den Berg and B. Jacobs. The LOOP compiler for Java and JML. Techn. Rep. CSI-R0019, Comput. Sci. Inst., Univ. of Nijmegen. To appear at TACAS’01., 2000.
T. Budd. Understanding Object-Oriented Programming with Java. Addison-Wesley, 2000. Updated Edition.
F. Christian. Correct and robust programs. IEEE Trans. on Software Eng., 10(2):163–174, 1984.
J. Gosling, B. Joy, and G. Steele. The Java Language Specification. The Java Series. Addison-Wesley, 1996.
J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification Second Edition. The Java Series. Addison-Wesley, 2000.
M. Huisman. Reasoning about JAVA Programs in higher order logic with PVS and Isabelle. PhD thesis, Univ. Nijmegen, 2001.
M. Huisman and B. Jacobs. Inheritance in higher order logic: Modeling and reasoning. In M. Aagaard and J. Harrison, editors, Theorem Proving in Higher Order Logics, number 1869 in Lect. Notes Comp. Sci., pages 301–319. Springer, Berlin, 2000.
M. Huisman and B. Jacobs. Java program verification via a Hoare logic with abrupt termination. In T. Maibaum, editor, Fundamental Approaches to Software Engineering, number 1783 in Lect. Notes Comp. Sci., pages 284–303. Springer, Berlin, 2000.
M. Huisman, B. Jacobs, and J. van den Berg. A case study in class library verification: Java’s Vector class. Techn. Rep. CSI-R0007, Comput. Sci. Inst., Univ. of Nijmegen. To appear in Software Tools for Technology Transfer, 2001.
B. Jacobs and E. Poll. A logic for the Java Modeling Language JML. Techn. Rep. CSI-R0018, Comput. Sci. Inst., Univ. of Nijmegen. To appear at FASE’01., 2000.
B. Jacobs and E. Poll. A monad for basic Java semantics. In T. Rus, editor, Algebraic Methodology and Software Technology, number 1816 in Lect. Notes Comp. Sci., pages 150–164. Springer, Berlin, 2000.
B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:222–259, 1997.
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. JML: A notation for detailed design. In H. Kilov and B. Rumpe, editors, Behavioral Specifications of Business and Systems, pages 175–188. Kluwer, 1999.
K.R.M. Leino. Toward Reliable Modular Programs. PhD thesis, California Inst. of Techn., 1995.
K.R.M. Leino and J.L.A. van de Snepscheut. Semantics of exceptions. In E.-R. Olderog, editor, Programming Concepts, Methods and Calculi, pages 447–466. North-Holland, 1994.
T. Lindholm and F. Yellin. The Java Virtual Machine Specification Second Edition. The Java Series. Addison-Wesley, 1999.
B. Meyer. Object-Oriented Software Construction. Prentice Hall, 2nd rev. edition, 1997.
D. von Oheimb. Analyzing Java in Isabelle/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Techn. Univ. München, 2000.
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, number 1523 in Lect. Notes Comp. Sci., pages 119–156. Springer, Berlin, 1998.
S. Owre, J.M. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. on Softw. Eng., 21(2):107–125, 1995.
L.C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and computer science, pages 361–386. Academic Press, London, 1990. The APIC series, vol. 31.
E. Poll, J. van den Berg, and B. Jacobs. Specification of the JavaCard API in JML. In J. Domingo-Ferrer, D. Chan, and A. Watson, editors, Smart Card Research and Advanced Application, pages 135–154. Kluwer Acad. Publ., 2000.
E. Poll, J. van den Berg, and B. Jacobs. Formal specification of the JavaCard API in JML: the APDU class. Comp. Networks Mag., 2001. To appear.
Loop Project. http://www.cs.kun.nl/~bart/LOOP/.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jacobs, B. (2001). A Formalisation of Java’s Exception Mechanism. In: Sands, D. (eds) Programming Languages and Systems. ESOP 2001. Lecture Notes in Computer Science, vol 2028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45309-1_19
Download citation
DOI: https://doi.org/10.1007/3-540-45309-1_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41862-7
Online ISBN: 978-3-540-45309-3
eBook Packages: Springer Book Archive