Advertisement

A Formalisation of Java’s Exception Mechanism

  • Bart Jacobs
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)

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.

Keywords

Type Theory Java Program High Order Logic Exception Handling Note Comp 
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

  1. 1.
    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.CrossRefGoogle Scholar
  2. 2.
    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.Google Scholar
  3. 3.
    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.Google Scholar
  4. 4.
    T. Budd. Understanding Object-Oriented Programming with Java. Addison-Wesley, 2000. Updated Edition.Google Scholar
  5. 5.
    F. Christian. Correct and robust programs. IEEE Trans. on Software Eng., 10(2):163–174, 1984.CrossRefGoogle Scholar
  6. 6.
    J. Gosling, B. Joy, and G. Steele. The Java Language Specification. The Java Series. Addison-Wesley, 1996.Google Scholar
  7. 7.
    J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification Second Edition. The Java Series. Addison-Wesley, 2000.Google Scholar
  8. 8.
    M. Huisman. Reasoning about JAVA Programs in higher order logic with PVS and Isabelle. PhD thesis, Univ. Nijmegen, 2001.Google Scholar
  9. 9.
    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.CrossRefGoogle Scholar
  10. 10.
    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.CrossRefGoogle Scholar
  11. 11.
    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.Google Scholar
  12. 12.
    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.Google Scholar
  13. 13.
    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.CrossRefGoogle Scholar
  14. 14.
    B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:222–259, 1997.zbMATHGoogle Scholar
  15. 15.
    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.Google Scholar
  16. 16.
    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.Google Scholar
  17. 17.
    K.R.M. Leino. Toward Reliable Modular Programs. PhD thesis, California Inst. of Techn., 1995.Google Scholar
  18. 18.
    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.Google Scholar
  19. 19.
    T. Lindholm and F. Yellin. The Java Virtual Machine Specification Second Edition. The Java Series. Addison-Wesley, 1999.Google Scholar
  20. 20.
    B. Meyer. Object-Oriented Software Construction. Prentice Hall, 2nd rev. edition, 1997.Google Scholar
  21. 21.
    D. von Oheimb. Analyzing Java in Isabelle/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Techn. Univ. München, 2000.Google Scholar
  22. 22.
    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.CrossRefGoogle Scholar
  23. 23.
    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.CrossRefGoogle Scholar
  24. 24.
    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.Google Scholar
  25. 25.
    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.Google Scholar
  26. 26.
    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.Google Scholar
  27. 27.

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Bart Jacobs
    • 1
  1. 1.Dep. Comp. Sci.Univ. NijmegenNijmegenThe Netherlands

Personalised recommendations