zbMATH — the first resource for mathematics

A bytecode logic for JML and types. (English) Zbl 1168.68357
Kobayashi, Naoki (ed.), Programming languages and systems. 4th Asian symposium, APLAS 2006, Sydney, Australia, November 8–10, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-48937-5/pbk). Lecture Notes in Computer Science 4279, 389-405 (2006).
Summary: We present a program logic for virtual machine code that may serve as a suitable target for different proof-transforming compilers. Compilation from JML-specified source code is supported by the inclusion of annotations whose interpretation extends to non-terminating computations. Compilation from functional languages, and the communication of results from intermediate level program analysis phases are facilitated by a new judgement format that admits the compositionality of type systems to be reflected in derivations. This makes the logic well suited to serve as a language in which proofs of a PCC architecture are expressed. We substantiate this claim by presenting the compositional encoding of a type system for bounded heap consumption. Both the soundness proof of the logic and the derivation of the type system have been formally verified by an implementation in Isabelle/HOL.
For the entire collection see [Zbl 1133.68007].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
Isabelle/HOL; JML
Full Text: DOI