Gerwin Klein
Skip Abstract Section
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.
- Alves-Foss, J., ed. 1999. Formal Syntax and Semantics of Java. LNCS, vol. 1523. Springer, New York.]] Google Scholar
Digital Library
- Ancona, D., Lagorio, G., and Zucca, E. 2001. A core calculus for Java exceptions. In Proceedings of the 16th ACM Conference on Object Oriented Programming, Systems, Languages, and Applications. 16--30.]] Google ScholarDigital Library
- Aspinall, D. 2000. Proof general---A generic tool for proof development. In Proceedings of the Tools and Algorithms for Construction and Analysis of Systems Conference, TACAS 2000, S. Graf and M. Schwartzbach, eds. LNCS, vol. 1785. Springer, New York, 38--42.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 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.]]Google Scholar
- Barthe, G., Dufay, G., Jakubiec, L., Serpette, B., and de Sousa, S. M. 2001. A formal executable semantics of the JavaCard platform. In Proceedings of the Programming Languages and Systems (ESOP 2001) Conference, D. Sands, ed. LNCS, vol. 2028. Springer, New York, 302--319.]] Google ScholarDigital Library
- Berghofer, S. 2003. Proofs, programs and executable specifications in higher order logic. Ph.D. thesis, Institut für Informatik, Technische Universität München.]]Google Scholar
- Berghofer, S. and Nipkow, T. 2002. Executing higher order logic. In Proceedings of the Types for Proofs and Programs (TYPES'00) Conference, P. Callaghan, et al. eds. LNCS, vol. 2277. Springer, New York, 24--40.]] Google ScholarDigital Library
- Bertelsen, P. 1997. Semantics of Java bytecode. Tech. rep., Technical University of Denmark. Mar. http://home.tiscali.dk/petermb/.]]Google Scholar
- Büchi, M. and Weck, W. 1998. Compound types for Java. In Proceedings of the 13th ACM Conference Object-Oriented Programming, Systems, Languages, and Application. ACM Press, New York.]] Google ScholarDigital Library
- Coglio, A. 2004. Simple verification technique for complex Java bytecode subroutines. Concurrency and Comput. Practice and Experience 16, 7 (June), 647--670.]] Google ScholarDigital Library
- 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.]]Google Scholar
- Cohen, R. 1997. The defensive Java virtual machine specification. Tech. rep., Computational Logic Inc. http://www.cli.com/software/djvm/.]]Google Scholar
- Dave, M. A. 2003. Compiler verification: A bibliography. SIGSOFT Softw. Eng. Notes 28, 6, 2--2.]] Google ScholarDigital Library
- Drossopoulou, S. and Eisenbach, S. 1999. Describing the semantics of Java and proving type soundness. In Formal Syntax and semantics of a Java. LNCS, vol. 1523. Springer, New York 41--82.]] Google ScholarDigital Library
- Flatt, M., Krishnamurthi, S., and Felleisen, M. 1999. A programmer's reduction semantics for classes and mixins. In Formal Syntax and semantics of a Java. LNCS, vol. 1523. Springer, New York, 241--269.]] Google ScholarDigital Library
- Freund, S. N. 2000. Type systems for object-oriented intermediate languages. Ph.D. thesis, Stanford University.]] Google ScholarDigital Library
- Freund, S. N. and Mitchell, J. C. 2003. A type system for the Java bytecode language and verifier. J. Automated Reasoning 30, 271--321.]] Google ScholarDigital Library
- Goldberg, A. 1998. A specification of Java loading and bytecode verification. In Proceedings of the 5th ACM Conference on Computer and Communications Security. ACM Press, New York, 49--58.]] Google ScholarDigital Library
- Hartel, P. and Moreau, L. 2001. Formalizing the safety of Java, the Java virtual machine and Java card. ACM Comput. Surv. 33, 517--558.]] Google ScholarDigital Library
- Huisman, M. 2001. Reasoning about Java programs in higher order logic with PVS and Isabelle. Ph.D. thesis, Universiteit Nijmegen.]]Google Scholar
- 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.]]Google Scholar
- Igarashi, A., Pierce, B. C., and Wadler, P. 2001. Featherweight Java: A minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23, 396--450.]] Google ScholarDigital Library
- Kildall, G. A. 1973. A unified approach to global program optimization. In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM Press, New York, 194--206.]] Google ScholarDigital Library
- Klein, G. 2003. Verified Java bytecode verification. Ph.D. thesis, Institut für Informatik, Technische Universität München.]]Google Scholar
- Klein, G. and Nipkow, T. 2001. Verified lightweight bytecode verification. Concurrency and Comput. Practice and Experience 13, 1133--1151.]]Google ScholarCross Ref
- Klein, G. and Nipkow, T. 2003. Verified bytecode verifiers. Theor. Comput. Sci. 298, 583--626.]] Google ScholarDigital Library
- Klein, G. and Strecker, M. 2004. Verified bytecode verification and type-certifying compilation. J. Logic Algebraic Program. 58, 1--2, 27--60.]]Google ScholarCross Ref
- Klein, G. and Wildmoser, M. 2003. Verified bytecode subroutines. J. Automated Reasoning 30, 363--398.]] Google ScholarDigital Library
- League, C., Shao, Z., and Trifonov, V. 2002. Type-Preserving compilation of featherweight Java. ACM Trans. Program. Lang. Syst. 24, 112--152.]] Google ScholarDigital Library
- Leroy, X. 2003. Java bytecode verification: Algorithms and formalizations. J. Automated Reasoning 30, 235--269.]] Google ScholarDigital Library
- Lindholm, T. and Yellin, F. 1999. The Java Virtual Machine Specification. Addison-Wesley, Reading, Mass.]] Google ScholarDigital Library
- Liu, H. and Moore, J. S. 2003. Executable JVM model for analytical reasoning: A study. In Proceedings of the 2003 Workshop on Interpreters, Virtual Machines and Emulators. ACM Press, New York 15--23.]] Google ScholarDigital Library
- Muchnick, S. S. 1997. Advanced Compiler Design and Implementation. Morgan Kaufmann San Fransisco, Calif.]] Google ScholarDigital Library
- 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.]]Google ScholarCross Ref
- Nipkow, T. 2001. Verified bytecode verifiers. In Proceedings of the Foundations of Software Science and Computation Structures Conference, (FOSSACS 2001), F. Honsell, ed. LNCS, vol. 2030. Springer, New York, 347--363.]] Google ScholarDigital Library
- Nipkow, T., ed. 2003a. Special Issue on Java Bytecode Verification. J. Automated Reasoning, 30, 3--4.]] Google ScholarDigital Library
- 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.]]Google ScholarCross Ref
- 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.]]Google Scholar
- Nipkow, T. and Oheimb, D. v. 1998. Javaℓight is type-safe---Definitely. In Proceedings of the 25th ACM Symposium on Principles of Programming Languages. ACM Press, New York, 161--170.]] Google ScholarDigital Library
- Nipkow, T., Paulson, L., and Wenzel, M. 2002. Isabelle/HOL---A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, New York. http://www.in.tum.de/~nipkow/LNCS2283/.]]Google Scholar
- Oheimb, D. v. and Nipkow, T. 1999. Machine-Checking the Java specification: Proving type-safety. In Formal Syntax and semantics of a Java. LNCS, vol. 1523. Springer, New York, 119--156.]] Google ScholarDigital Library
- Pusch, C. 1999. Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems Conference (TACAS'99), W. Cleaveland, ed. LNCS, vol. 1579. Springer, New York, 89--103.]] Google ScholarDigital Library
- Qian, Z. 2000. Standard fixpoint iteration for Java bytecode verification. ACM Trans. Program. Lang. Syst. 22, 638--672.]] Google ScholarDigital Library
- Rose, E. 2002. Vérification de code d'octet de la machine virtuelle Java. Formalisation et implantation. Ph.D. thesis, Université Paris VII.]]Google Scholar
- Rose, E. 2003. Lightweight bytecode verification. J. Automated Reasoning 31, 3--4, 303--334.]] Google ScholarDigital Library
- Rose, E. and Rose, K. 1998. Lightweight bytecode verification. In Proceedings of the OOPSLA'98 Workshop on Formal Underpinnings of Java.]]Google Scholar
- 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.]]Google Scholar
- Schirmer, N. 2004. Analysing the Java package/access concepts in Isabelle/HOL. Concurrency and Comput. Practice and Experience 16, 689--706.]] Google ScholarDigital Library
- 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.]]Google Scholar
- Stärk, R., Schmid, J., and Börger, E. 2001. Java and the Java Virtual Machine---Definition, Verification, Validation. Springer, New York.]] Google ScholarDigital Library
- Stata, R. and Abadi, M. 1998. A type system for Java bytecode subroutines. In Proceedings of the 25th ACM Symposium on Principles of Programming Languages. ACM Press, New York, 149--161.]] Google ScholarDigital Library
- Strecker, M. 2002. Formal verification of a Java compiler in Isabelle. In Automated Deduction---CADE-18, A. Voronkov, ed. LNCS, vol. 2392. Springer, New York, 63--77.]] Google ScholarDigital Library
- Syme, D. 1999. Proving Java type soundness. In Formal Syntax and Semantics of Java. LNCS, vol. 1523. Springer, New York. 83--118.]] Google ScholarDigital Library
- 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.]]Google Scholar
- Wright, A. and Felleisen, M. 1994. A syntactic approach to type soundness. Inf. Comput. 115, 38--94.]] Google ScholarDigital Library
- Young, W. D. 1989. A mechanically verified code generator. J. Automated Reasoning 5, 493--518.]] Google ScholarDigital Library
Index Terms
- A machine-checked model for a Java-like language, virtual machine, and compiler
Recommendations
Coinductive big-step operational semantics for type soundness of Java-like languages
FTfJP '11: Proceedings of the 13th Workshop on Formal Techniques for Java-Like ProgramsWe define a coinductive semantics for a simple Java-like language by simply interpreting coinductively the rules of a standard big-step operational semantics.
We prove that such a semantics is sound w.r.t. the usual small-step operational semantics, and ...
How to prove type soundness of Java-like languages without forgoing big-step semantics
FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like ProgramsSmall-step operational semantics is the most commonly employed formalism for proving type soundness of statically typed programming languages, because of its ability to distinguish stuck from non-terminating computations, as opposed to big-step ...
Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler
This article presents JinjaThreads, a unified, type-safe model of multithreaded Java source code and bytecode formalised in the proof assistant Isabelle/HOL. The semantics strictly separates sequential aspects from multithreading features like locks, ...
Comments