Form.thy [pdf]

The Sytax of formulas and operations on these.

JBC_Semantics.thy [pdf]

A formal semantics for Jinja Bytecode.

JBC_SafetyPolicy.thy [pdf]

Defines the safety policy: reject arithmetic overflows.

JBC_SafetyLogic.thy [pdf]

First order arithmetics enriched with OO specific operators.

JBC_VCG.thy [pdf]

Instantiates the VCG.

JBC_SysInv.thy [pdf]

Proves system invariants for Jinja.

JBC_wpFcorrect.thy [pdf]

Verifies the weakest precondition operator.

JBC_succsFcorrect.thy [pdf]

Verifies the control flow function. Every machine transition occurs in the control flow.

JBC_Correctness.thy [pdf]

Verifies the correctness of the instantiated VCG. Instantiates PCCFramework/VCG_Correctness.thy.

JBC_succsFprogress.thy [pdf]

Verifies the control flow function. Every edge in the control flow indicates a possible machine transition.

JBC_VCG_Completess.thy [pdf]

Verifies the completeness of the instantiated VCG. Instantiates PCCFramework/VCG_Completeness.thy.

JBC_Expressiveness.thy [pdf]

Verifies the expressiveness requirements. Instantiates locale exprSL from PCCFramework/VCG_Completeness.thy.

VCOpt.thy [pdf] 
Defines and verifies optimizing formula transformers. 
VCGExec.thy [pdf] 
Generates executable ML code for the VCG. 