Language of an Event-B Component: Difference between revisions
imported>Laurent |
imported>Laurent No edit summary |
||
| Line 7: | Line 7: | ||
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 <tt>org.eventb.core.formulaExtensionProvider</tt> 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. | 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 <tt>org.eventb.core.formulaExtensionProvider</tt> 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 | ==Language of Proofs== | ||
There is however a special case for proof files. | |||
[[Category:Design]] | [[Category:Design]] | ||
[[Category:Rodin Platform]] | [[Category:Rodin Platform]] | ||
Revision as of 11:14, 20 November 2013
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 Proofs
There is however a special case for proof files.
