Issue No. 09 - September (2000 vol. 26)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.877847
<p><b>Abstract</b>—In this paper, we provide a rigorous framework for language and platform independent design and analysis of exception handling mechanisms in modern programming languages and their implementations. To illustrate the practicality of the method we develop it for the exception handling mechanism of Java and show that its implementation on the Java Virtual Machine (JVM) is correct. For this purpose we define precise abstract models for exception handling in Java and in the JVM and define a compilation scheme of Java to JVM code which allows us to prove that, in corresponding runs, Java and the JVM throw the same exceptions and with equivalent effect. Thus, the compilation scheme can, with reasonable confidence, be used as a standard reference for Java exception handling compilation.</p>
Semantics, exception handling, compiler, correctness, Java, Java Virtual Machine, abstract state machines.
Wolfram Schulte, Egon Börger, "A Practical Method for Specification and Analysis of Exception Handling-A Java/JVM Case Study", IEEE Transactions on Software Engineering, vol. 26, no. , pp. 872-887, September 2000, doi:10.1109/32.877847