User:Nicolas/Collections/ADVANCE D3.4 Language extension
Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this new feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (proof extensions).
The Theory plug-in provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. A theory is the dedicated component used to hold mathematical extensions (datatypes, operators with direct definitions, operators with recursive definitions and operators with axiomatic definitions), and proof extensions (polymorphic theorems, rewrite and inference rules). Theories are developed in the workspace (akin to models), and are subject to static checking and proof obligation generation. Proof obligations generated from theories ensure any contributed extensions do not compromise the soundness of the existing infrastructure for modelling and proof. In essence, the Theory plug-in provides a systematic platform for defining, validating and using extensions while exploiting the benefits brought by proof obligations.
Motivations / Decisions