Model of Java & Specifications of Typing

Some quick notes:

The ".abs" files are abstracts, which act as specifications.

The ".art" files are proof documents that get checked by DECALRE.

Not all of the hypertext links work, particularly in the proof files.

The specification can be read from bottom to top as follows:

• syntax.abs - Syntax of JavaS and JavaA, the source and annotated-source langauges.
• rsyntax.abs - Syntax of JavaR, which forms the terms of the abstract machine.
• wf.abs - Basic notions: Subclassing, Subinterfaces, Widening and traversing the subclass hierarchy
• wfenv.abs - Wellformedness for type environments, and facts that can be derived from this. The proofs are in wf.art and wfenv.art.
• The runtime machine:
  • runtime0.abs - Preliminary definitions for the abstract runtime machine. Frames, heaps, terms representing exceptional states and so on.
  • runtime1.abs - The structured operational semantics for the abstract runtime machine.
• The typing semantics:
  • statics1.abs and statics2.abs - Types for JavaS terms.
  • cstatics.abs - Types for annotated JavaA terms.
• Correlating the two:
  • rstatics1.abs - Types for runtime terms.
  • conforms.abs - Conformance invariants and crucial lemmas that these are preserved by heap allocation and heap/frame update. The proofs are in conforms.art.
  • link2_0.art - Lemmas correlating method fetch and method types.
  • subred.aux.art - Lemmas about frame allocation (perhaps these shuld go in conforms.abs).
  • subred.art - The subject reduction proof.

The major proof (subject reduction) can be found in subred.art. You can follow the links of imported files to see the specifications that this proof depends on. Important lemmas are proved in conforms.art, wfenv.art, link2_0.art and subred.aux.art.