Language of an Event-B Component

From Event-B
Revision as of 11:13, 20 November 2013 by imported>Laurent (→‎Interface with the Theory Plug-in)
Jump to navigationJump to search

Since the introduction of mathematical extensions in Rodin 2.0, Event-B components can use extended version of the Event-B mathematical language. This page described how this is organized in the core platform.

Interface with the Theory Plug-in

For most files, the actual version of the Event-B language is provided by the Theory plug-in. This is done by contributing to the org.eventb.core.formulaExtensionProvider extension point. Given an Event-B root, the object contributed to this extension point provides the formula factory to use for parsing the contents of the file. In practice, all regular files share the same formula factory, thanks to the Theory Path. However, theory files can each have a separate formula factory.

Language of Unchecked Components

Language of Generated Files

Language of Proofs