A Bytecode Logic for JML and Types

This document contains the Isabelle/HOL sources underlying our paper A bytecode logic for JML and types [2], updated to Isabelle 2008. We present a program logic for a subset of sequential Java bytecode that is suitable for representing both, features found in high-level specification language JML as well as interpretations of high-level type systems. To this end, we introduce a fine-grained collection of assertions, including strong invariants, local annotations and VDM-reminiscent partial-correctness specifications. Thanks to a goal-oriented structure and interpretation of judgements, verification may proceed without recourse to an additional control flow analysis. The suitability for interpreting intensional type systems is illustrated by the proof-carryingcode style encoding of a type system for a first-order functional language which guarantees a constant upper bound on the number of objects allocated throughout an execution, be the execution terminating or non-terminating....

• Type: Conference
• Year: 2006
• Where: APLAS
• Authors: Lennart Beringer, Martin Hofmann
• Keywords: APLAS 2006, Mobius Base Logic, Program Logic, Type System