Skip to topic | Skip to bottom
... Mobius IST-15905


Start of topic | Skip to actions

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:

  • TBD

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.

  • IVE - definition

-- JosephKiniry - 02 Mar 2006


You are here: Tools > Mobius Tool Project Overview > MobiusBytecodeSubsystemOverview

to top

Ideas, requests, problems regarding the Mobius site QUESTION?