Dynamic class initialization semantics: A Jinja extension

Susannah Mansky, Elsa L. Gunter

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The Java Virtual Machine (JVM) postpones running class initialization methods until their classes are first referenced, such as by a <pre>new</pre> or static instruction. This process is called dynamic class initialization. Jinja is a semantic framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Java-level big-step and small-step semantics, JVM-level small-step semantics, and an intermediate compilation step, J1, between these two levels. In this paper, we extend Jinja to include support for static instructions and dynamic class initialization. We also extend and re-prove related proofs, including Java-level type safety, equivalence between Java-level big-step and small-step semantics, and the correctness of a compilation from the Java level to the JVM level through J1. This work is based on the Java SE 8 specification.

Original languageEnglish (US)
Title of host publicationCPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019
EditorsAssia Mahboubi
PublisherAssociation for Computing Machinery, Inc
Pages209-221
Number of pages13
ISBN (Electronic)9781450362221
DOIs
StatePublished - Jan 14 2019
Event8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 - Cascais, Portugal
Duration: Jan 14 2019Jan 15 2019

Publication series

NameCPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019

Other

Other8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019
CountryPortugal
CityCascais
Period1/14/191/15/19

Keywords

  • Java
  • Java Virtual Machine
  • compilation
  • dynamic class initialization
  • interactive theorem proving
  • operational semantics
  • type safety

ASJC Scopus subject areas

  • Computer Science Applications
  • Software

Fingerprint Dive into the research topics of 'Dynamic class initialization semantics: A Jinja extension'. Together they form a unique fingerprint.

  • Cite this

    Mansky, S., & Gunter, E. L. (2019). Dynamic class initialization semantics: A Jinja extension. In A. Mahboubi (Ed.), CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019 (pp. 209-221). (CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019). Association for Computing Machinery, Inc. https://doi.org/10.1145/3293880.3294104