A machine-checked model for a Java-like language, virtual machine, and compiler

ABSTRACT

We introduce Jinja, a Java-like programming language with a formal semantics designed to exhibit core features of the Java language architecture. Jinja is a compromise between the realism of the language and the tractability and clarity of its formal semantics. The following aspects are formalised: a big and a small step operational semantics for Jinja and a proof of their equivalence, a type system and a definite initialisation analysis, a type safety proof of the small step semantics, a virtual machine (JVM), its operational semantics and its type system, a type safety proof for the JVM; a bytecode verifier, that is, a data flow analyser for the JVM, a correctness proof of the bytecode verifier with respect to the type system, and a compiler and a proof that it preserves semantics and well-typedness. The emphasis of this work is not on particular language features but on providing a unified model of the source language, the virtual machine, and the compiler. The whole development has been carried out in the theorem prover Isabelle/HOL.

REFERENCES

• 1: Formal Syntax and Semantics of Java, January 1999
• 2: D. Ancona , G. Lagorio , E. Zucca, A core calculus for Java exceptions, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.16-30, October 14-18, 2001, Tampa Bay, FL, USA
• 3: David Aspinall, Proof General: A Generic Tool for Proof Development, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.38-42, March 25-April 02, 2000
• 4: Ballarin, C. 2003. Locales and locale expressions in Isabelle/Isar. In Proceedings of the Types for Proofs and Programs Conference, TYPES 2003, S. Berardi, et al. eds. LNCS, vol. 3085. Springer, New York, 34--50.
• 5: Barthe, G. and Dufay, G. 2004. A tool-assisted framework for certified bytecode verification. In Proceedings of the Conference Fundamental Approaches to Software Engineering, FASE 2004, M. Wermelinger and T. Margaria, eds. LNCS, vol. 2984. Springer, New York, 99--113.
• 6: Gilles Barthe , Guillaume Dufay , Line Jakubiec , Bernard P. Serpette , Simão Melo de Sousa, A Formal Executable Semantics of the JavaCard Platform, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.302-319, April 02-06, 2001
• 7: Berghofer, S. 2003. Proofs, programs and executable specifications in higher order logic. Ph.D. thesis, Institut für Informatik, Technische Universität München.
• 8: Stefan Berghofer , Tobias Nipkow, Executing Higher Order Logic, Selected papers from the International Workshop on Types for Proofs and Programs, p.24-40, December 08-12, 2000
• 9: Bertelsen, P. 1997. Semantics of Java bytecode. Tech. rep., Technical University of Denmark. Mar. http://home.tiscali.dk/petermb/.
• 10: Martin Büchi , Wolfgang Weck, Compound types for Java, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.362-373, October 18-22, 1998, Vancouver, British Columbia, Canada
• 11: Alessandro Coglio, Simple verification technique for complex Java bytecode subroutines: Research Articles, Concurrency and Computation: Practice & Experience, v.16 n.7, p.647-670, June 2004 [doi>10.1002/cpe.v16:7]
• 12: Coglio, A., Goldberg, A., and Qian, Z. 2000. Toward a provably-correct implementation of the JVM bytecode verifier. In Proceedings of the DARPA Information Survivability Conference and Exposition (DISCEX'00), vol. 2. IEEE Computer Society Press, Las Alamitos, Calif., 403--410.
• 13: Cohen, R. 1997. The defensive Java virtual machine specification. Tech. rep., Computational Logic Inc. http://www.cli.com/software/djvm/.
• 14: Maulik A. Dave, Compiler verification: a bibliography, ACM SIGSOFT Software Engineering Notes, v.28 n.6, November 2003 [doi>10.1145/966221.966235]
• 15: Sophia Drossopoulou , Susan Eisenbach, Describing the Semantics of Java and Proving Type Soundness, Formal Syntax and Semantics of Java, p.41-82, January 1999
• 16: Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, A Programmer's Reduction Semantics for Classes and Mixins, Formal Syntax and Semantics of Java, p.241-269, January 1999
• 17: Stephen Neil Freund , John C. Mitchell, Type systems for object-oriented intermediate languages, 2000
• 18: Stephen N. Freund , John C. Mitchell, A Type System for the Java Bytecode Language and Verifier, Journal of Automated Reasoning, v.30 n.3-4, p.271-321, 2003 [doi>10.1023/A:1025011624925]
• 19: Allen Goldberg, A specification of Java loading and bytecode verification, Proceedings of the 5th ACM conference on Computer and communications security, p.49-58, November 02-05, 1998, San Francisco, California, United States [doi>10.1145/288090.288104]
• 20: Pieter H. Hartel , Luc Moreau, Formalizing the safety of Java, the Java virtual machine, and Java card, ACM Computing Surveys (CSUR), v.33 n.4, p.517-558, December 2001 [doi>10.1145/503112.503115]
• 21: Huisman, M. 2001. Reasoning about Java programs in higher order logic with PVS and Isabelle. Ph.D. thesis, Universiteit Nijmegen.
• 22: Hutton, G. and Wright, J. 2004. Compiling exceptions correctly. In Mathematics of Program Construction, MPC 2004, D. Kozen and C. Shankland, eds. LNCS, vol. 3125. Springer, New York, 211--227.
• 23: Atsushi Igarashi , Benjamin C. Pierce , Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.396-450, May 2001 [doi>10.1145/503502.503505]
• 24: Gary A. Kildall, A unified approach to global program optimization, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-206, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512945]
• 25: Klein, G. 2003. Verified Java bytecode verification. Ph.D. thesis, Institut für Informatik, Technische Universität München.
• 26: Klein, G. and Nipkow, T. 2001. Verified lightweight bytecode verification. Concurrency and Comput. Practice and Experience 13, 1133--1151.
• 27: Gerwin Klein , Tobias Nipkow, Verified bytecode verifiers, Theoretical Computer Science, v.298 n.3, p.583-626, 11 April 2003 [doi>10.1016/S0304-3975(02)00869-1]
• 28: Klein, G. and Strecker, M. 2004. Verified bytecode verification and type-certifying compilation. J. Logic Algebraic Program. 58, 1--2, 27--60.
• 29: G. Klein , M. Wildmoser, Verified Bytecode Subroutines, Journal of Automated Reasoning, v.30 n.3-4, p.363-398, 2003 [doi>10.1023/A:1025095122199]
• 30: Christopher League , Zhong Shao , Valery Trifonov, Type-preserving compilation of Featherweight Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.2, p.112-152, March 2002 [doi>10.1145/514952.514954]
• 31: Xavier Leroy, Java Bytecode Verification: Algorithms and Formalizations, Journal of Automated Reasoning, v.30 n.3-4, p.235-269, 2003 [doi>10.1023/A:1025055424017]
• 32: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 33: Hanbing Liu , J Strother Moore, Executable JVM model for analytical reasoning: a study, Proceedings of the 2003 workshop on Interpreters, virtual machines and emulators, p.15-23, June 12-12, 2003, San Diego, California [doi>10.1145/858570.858572]
• 34: Steven S. Muchnick, Advanced compiler design and implementation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1998
• 35: Nipkow, T. 1991. Higher-order critical pairs. In Proceedings of the 6th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 342--349.
• 36: Tobias Nipkow, Verified Bytecode Verifiers, Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures, p.347-363, April 02-06, 2001
• 37: Tobias Nipkow, Java Bytecode Verification, Journal of Automated Reasoning, v.30 n.3-4, p.233-233, 2003 [doi>10.1023/A:1025086804452]
• 38: Nipkow, T. 2003b. Structured proofs in Isar/HOL. In Proceedings of the Types for Proofs and Programs Conference (TYPES 2002), H. Geuvers and F. Wiedijk, eds. LNCS, vol. 2646. Springer, New York, 259--278.
• 39: Nipkow, T. 2005. Jinja: Towards a comprehensive formal semantics for a Java-like language. In Proof Technology and Computation, Proceedings of the Marktobderdorf Summer School Conference 2003, H. Schwichtenberg and K. Spies, eds. IOS Press Amsterdam, the Netherlands.
• 40: Tobias Nipkow , David von Oheimb, Java_light is type-safe—definitely, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-170, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268960]
• 41: Isabelle/HOL: a proof assistant for higher-order logic, Springer-Verlag, London, 2002
• 42: David von Oheimb , Tobias Nipkow, Machine-Checking the Java Specification: Proving Type-Safety, Formal Syntax and Semantics of Java, p.119-156, January 1999
• 43: Cornelia Pusch, Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.89-103, March 22-28, 1999
• 44: Zhenyu Qian, Standard fixpoint iteration for Java bytecode verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.638-672, July 2000 [doi>10.1145/363911.363915]
• 45: Rose, E. 2002. Vérification de code d'octet de la machine virtuelle Java. Formalisation et implantation. Ph.D. thesis, Université Paris VII.
• 46: Eva Rose, Lightweight Bytecode Verification, Journal of Automated Reasoning, v.31 n.3-4, p.303-334, 2003 [doi>10.1023/B:JARS.0000021015.15794.82]
• 47: Rose, E. and Rose, K. 1998. Lightweight bytecode verification. In Proceedings of the OOPSLA'98 Workshop on Formal Underpinnings of Java.
• 48: Schirmer, N. 2003. Java definite assignment in Isabelle/HOL. In Proceedings of the Formal Techniques for Java-like Programs 2003 Conference, S. Eisenbach et al. eds. Chair of Software Engineering, ETH Zürich. Technical Report 108.
• 49: Norbert Schirmer, Analysing the Java package/access concepts in Isabelle/HOL: Research Articles, Concurrency and Computation: Practice & Experience, v.16 n.7, p.689-706, June 2004 [doi>10.1002/cpe.v16:7]
• 50: Stärk, R. and Schmid, J. 2001. The problem of bytecode verification in current implementations of the JVM. Tech. rep., Department of Computer Science, ETH Zürich.
• 51: Robert F. Stark , E. Borger , Joachim Schmid, Java and the Java Virtual Machine: Definition, Verification, Validation with Cdrom, Springer-Verlag New York, Inc., Secaucus, NJ, 2001
• 52: Raymie Stata , Martín Abadi, A type system for Java bytecode subroutines, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.149-160, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268959]
• 53: Martin Strecker, Formal Verification of a Java Compiler in Isabelle, Proceedings of the 18th International Conference on Automated Deduction, p.63-77, July 27-30, 2002
• 54: Don Syme, Proving Java Type Soundness, Formal Syntax and Semantics of Java, p.83-118, January 1999
• 55: Wenzel, M. 2002. Isabelle/Isar---A versatile environment for human-readable formal proof documents. Ph.D. thesis, Institut für Informatik, Technische Universität München. http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html.
• 56: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]
• 57: William D. Young, A mechanically verified code generator, Journal of Automated Reasoning, v.5 n.4, p.493-518, Dec. 1989

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Object-oriented constructs

General Terms:
Languages, Verification

Keywords:
Java, operational semantics, theorem proving