This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Practical Method for Specification and Analysis of Exception Handling-A Java/JVM Case Study
September 2000 (vol. 26 no. 9)
pp. 872-887

Abstract—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.

[1] Formal Syntax and Semantics of Java, J. Alves-Foss, ed., Springer-Verlag, 1999.
[2] P. Bertelsen, “Semantics of Java Byte Code,” 1997. http://citeseer.nj. nec.com/kropp98,automated.htmlftp:/ /dina.kvl.dk/pub/Staff/Peter.Bertelsen jvm-semantics.ps.gz.
[3] E. Börger, “High Level System Design and Analysis Using Abstract State Machines,” Current Trends in Applied Formal Methods (FM-Trends 98), D. Hutter, W. Stephan, P. Traverso, and M. Ullmann eds., pp. 1–43, Springer-Verlag, 1999.
[4] E. Börger and I. Durdanovic, “Correctness of Compiling Occam to Transputer Code,” Computer J., vol. 39, no. 1, pp. 52–92, 1996.
[5] E. Börger and S. Mazzanti, “A Practical Method for Rigorously Controllable Hardware Design,” Proc. ZUM'97: The Z Formal Specification Notation, J.P. Bowen, M.B. Hinchey, and D. Till, eds., pp. 151–187, 1997.
[6] E. Börger and D. Rosenzweig, “The WAM—Definition and Compiler Correctness,” Logic Programming: Formal Methods and Practical Applications, C. Beierle and L. Plümer, eds., North–Holland, pp. 20–90, Elsevier Science, 1995.
[7] E. Börger, J. Schmid, W. Schulte, and R. Stärk, “Java and the Java Virtual Machine: Definition, Verification, Validation,” submitted for publication, Lecture Notes in Computer Science, Springer-Verlag, 2000.
[8] E. Börger and W. Schulte, “Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation,” Proc. Math. Foundations of Computer Science, MFCS '98, L. Brim, J. Gruska, and J. Zlatuska, eds., 1998.
[9] E. Börger and W. Schulte, “A Programmer Friendly Modular Definition of the Semantics of Java,” Formal Syntax and Semantics of Java™, J. Alves-Foss, ed., pp. 353–404, Springer-Verlag, 1999.
[10] E. Börger and W. Schulte, “A Modular Design for the Java Virtual Machine Architecture,” Architecture Design and Validation Methods, E. Börger, ed., Springer-Verlag, 2000.
[11] E. Börger and W. Schulte, “Initialization Problems for Java,” Software—Concepts and Tools, vol. 20, no. 4, 1999.
[12] R.M. Cohen, “Defensive Java, Virtual Machine, Version 0.5 Alpha Release,” 1997. http://www.cli.com/softwaredjvm.
[13] A. Dold, “A Formal Representation of Abstract State Machines Using PVS,” Verifix Report, Ulm 6.2, pp. 1–25, Germany, 1998.
[14] S.N. Freund, “Pro and Cons of Embedded Subroutines in the JVM,” Proc. Object-Orientated Programming Systems, Languages, and Applications (OOPSLA '98) Workshop Formal Underpinnings of Java, 1998.
[15] S.N. Freund and J.C. Mitchell, “A Type System for Object Initialization in the Java Bytecode Language,” Proc. Object-Orientated Programming Systems, Languages, and Applications OOPSLA '98, 1998.
[16] Y. Gurevich, “Evolving Algebras 1993: Lipari Guide,” Specification and Validation Methods, E. Börger, ed., Oxford Univ. Press, 1995.
[17] J. Gosling, B. Joy, and G. Steele, The Java Language Specification, Addison-Wesley, Reading, Mass., 1996.
[18] W. Goerigk, A. Todd, T. Gaul, G. Goos, A. Heberle, F.W. von Henke, U. Hoffmann, H. Langmaack, H. Pfeifer, H. Ruess, and W. Zimmermann, “Compiler Correctness and Implementation Verification: The Verifix Approach,” Proc. Poster Session CC '96—Int'l Conf. Compiler Construction, P. Fritzson, ed., IDA, Technical Report LiTH-IDA-R-96-12, Linköping, Sweden, 1996.
[19] T. Lindholm and F. Yellin, The Java Virtual Machine Specification, Addison-Wesley, Reading, Mass., 1997.
[20] J.S. Moore, “Proving Theorems About Java-Like Byte Code,” Correct Systems Design Recent Insights and Advances, E.R. Olderog and B. Steffen, eds., Springer-Verlag, 1999.
[21] C. Pusch, “Verification of Compiler Correctness for the WAM,” Proc. Theorem Proving in Higher Order Logics (TPHOLs '96), J. Von Wright, J. Grundy, and J. Harrison, eds., pp. 347–362, 1996.
[22] R. Stärk, “Foundations of Java—Lecture Notes for Computer Science Students,” Univ. of Fribourg, 1999.
[23] G. Schellhorn, “Verifikation Abstrakter Zustandsmaschinen,” doctoral dissertation, Univ. of Ulm, Germany, 1999.
[24] R. Stata and M. Abadi, “A Type System for Java Bytecode Subroutines,” Proc. 25th Ann. SIGPLAN-SIGACT Symp. Principles of Programming Languages, 1998.
[25] K. Winter, “Model Checking for Abstract State Machines,” J. Universal Computer Science, vol. 3, no. 5, 1997.
[26] G. DelCastillo and K. Winter, “Model Checking Support for the ASM High-Level Language,” Technical Report TR-ri-99-209, Univ. of Paderborn, Germany, 1999.

Index Terms:
Semantics, exception handling, compiler, correctness, Java, Java Virtual Machine, abstract state machines.
Citation:
Egon Börger, Wolfram Schulte, "A Practical Method for Specification and Analysis of Exception Handling-A Java/JVM Case Study," IEEE Transactions on Software Engineering, vol. 26, no. 9, pp. 872-887, Sept. 2000, doi:10.1109/32.877847
Usage of this product signifies your acceptance of the Terms of Use.