Mobius Bytecode Subsystem Overview
Authors: Joseph Kiniry
Version: 1 March 2006
Revision History
1 March 2006 - Initial outline.
Related Documents
Introduction
TBW: An overview of this subsystem.
Requirements
The mandatory requirements for the Mobius Bytecode Subsystem are:
- BCEL with BCSL support (UCD)
- pretty-print BCSL-annotated bytecode to screen and La Te X?/PDF (UCD)
- BCSL-annotated bytecode compiler for JML level 0 and level C-annotated Java 1.4 source (INRIA)
- weakest-precondition calculus for sequential bytecode (INRIA)
- weakest-precondition VC generator for sequential bytecode (INRIA)
- Hoare logic for sequential bytecode (ETHZ)
- Hoare logic VC generator for sequential bytecode (ETHZ?)
- synchronization checker for arbitrary bytecode (UCD)
- interaction with Coq instance for reasoning in Mobius logic(s)
- Bicolano formalization of VM (INRIA)
- Mobius base logic (Munich)
- formalisation of sequential bytecode to guarded command language (ETHZ)
- sequential bytecode to guarded command translator (ETHZ?)
- Coq-specific PCC certificate generator
Secondary, desirable requirements for the Mobius Bytecode Subsystem include:
- interactive bytecode editor with BCSL support (UW, UCD)
- BCSL-annotated bytecode compiler for JML level 1 and level C-annotated Java 1.4 source (INRIA, UCD)
- strongest-postcondition calculus for sequential bytecode (?)
- strongest-postcondition generator for sequential bytecode (?)
- general-purpose PCC certificate generator
The following are not requirements of the Mobius Bytecode Subsystem:
Overview
TBW: An extended discussion of this subsystem, its interdependencies, who is responsible for what, etc.
Technology
TBW: A summary of which tools, libraries, frameworks, and the like that are dependencies of this subsystem.
Dictionary
TBW: A dictionary of domain terms/concepts for this subsystem, each of which is captured as an independent page in the Tool wiki.
-- JosephKiniry - 02 Mar 2006
