Difference between revisions of "Rodin Developer Support"
imported>Stefan |
imported>Stefan |
||
| Line 24: | Line 24: | ||
=== Event-B Component Library === | === Event-B Component Library === | ||
| − | Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an [[Abstract Syntax Tree|abstract syntax tree]]. | + | Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an [[Abstract Syntax Tree|abstract syntax tree]]. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). |
| − | [[ | + | * [[Abstract Syntax Tree]] |
| − | [[ | + | * [[Static Checker]] |
| − | [[Proof Manager]] | + | * [[Proof Obligation Generator]] |
| + | |||
| + | * [[Proof Manager]] | ||
== Extending the Rodin Platform == | == Extending the Rodin Platform == | ||
Revision as of 14:38, 4 July 2008
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
Contents
Rodin Platform Overview
Architecture of the Rodin Platform
Rodin Platform Core
Event-B User Interface
The Event-B User Interface of the Roding Platform has two major components that are concerned with either editing Event-B models or proving properties of models.
Event-B Component Library
Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an abstract syntax tree. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing).
