Theory Plug-in User Manual

University of Southampton

July 8, 2011

The Theory plug-in is a contribution to the Rodin platform that facilitates the specification, validation and deployment of language and prover extensions for Event-B. Language extensions are contributions to the Event-B language in the form of operators (both predicate and expression) and datatype definitions. Prover extensions are contributions to the Event-B proving infrastructure in the form of rewrite rules, inference rules and polymorphic theorems. The Theory plug-in provides an Event-B component (similar to contexts and machines) called theory $\includegraphics{thy.png}$ that can be used to define operators, datatypes and rules. Proof obligations are generated to validate semantic properties of extensions to ensure logical conservativity. The Theory plug-in is the successor of the Rule-based Prover (which will be referred to as RbP) plug-in. The following sections provide a concise description of the functionality of the plug-in.

For a quick start guide, the user can skip to Section 3.

$\includegraphics{nike.png}$ The Rule-based Prover only supported rewrite rules, and is superseded by the Theory plug-in.

$\includegraphics{info.png}$ The Event-B mathematical language refers to the language used to write axioms, invariants, guards etc. in Event-B models.

$\includegraphics{info.png}$ Language extensions refer to new operators and new datatypes.

$\includegraphics{info.png}$ Prover extensions refer to new rewrite rules, inference rules and polymorphic theorems that can be made available to the Event-B prover.