Skip to topic
|
Skip to bottom
IST-15905
Tools Web
Mobius Public Home
Mobius Intranet
Tools Web Home
Overview
Tools Summary
Tools Contacts
Component Index
Related Tools
Download Tools
Scientific Issues
Tools Publications
Project Management
Development Schedule
Project Status
Documentation And Coding Standards
Latest News
Tools Meetings
Site Visits
GForge
Tools
Index
Search
Changes
RSS Feed
Statistics
Preferences
Edit Toolbar
Help
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 * MobiusToolProjectOverview - a project summary of the Mobius Tool. ---++ Introduction This subsystem is responsible for reading and writing files in the BytecodeModelingLanguage (BML). ---++ Requirements The *mandatory* requirements for the Mobius Bytecode Subsystem are: * BCEL with BML support (UCD) * pretty-print BML-annotated bytecode to screen and LaTeX/PDF (UCD) * BML-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 BML support (UW, UCD) * BML-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 -- Main.JosephKiniry - 18 Sep 2006
End of topic
Skip to action links
|
Back to top
r1.3 :
Edit
|
Attach image or document
|
Printable version
|
Raw text
|
Page history
|
More actions
You are here:
Tools
>
BytecodeSubsystem
to top
Ideas, requests, problems regarding the Mobius site