A practical method for specification and analysis of exception handling -: A Java']Java/JVM case study

被引：8

作者：

Börger, E

Schulte, W

机构：

[1] Univ Pisa, Dipartimento Informat, Pisa, Italy

[2] Microsoft Res, Redmond, WA 98052 USA

来源：

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING | 2000年 / 26卷 / 09期

关键词：

semantics; exception handling; compiler; correctness; !text type='Java']Java[!/text; !text type='Java']Java[!/text] Virtual Machine; abstract state machines;

D O I：

10.1109/32.877847

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：872 / 887

页数：16