Language of an Event-B Component
From Event-B
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.
