Rodin Developer Support: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Stefan
No edit summary
imported>Stefan
No edit summary
Line 24: Line 24:
=== Event-B Component Library ===
=== Event-B Component Library ===


[[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]].


[[Static Checker]]
[[Static Checker]]

Revision as of 14:28, 4 July 2008

The Developer Support provides resources for developing plug-ins for the Rodin Platform.

Rodin Platform Overview

Architecture of the Rodin Platform

Rodin Platform Core

Database

Builder

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.

Editing

Proving

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.

Static Checker

Proof Obligation Generator

Proof Manager

Extending the Rodin Platform

Getting Started

Plug-in Tutorials

Useful Hints

Testing

Debugging

Rodin Developer FAQ