D32 Mathematical Extensions

Overview

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 defining his own mathematical operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (prover extensions).

A theory is a file that gathers of new algebraic types, new operators/predicates and new proof rules. It is developed in the Rodin workspace. When it is complete, the user makes it available to his models (this action is called the deployment of a theory). He can then start using his own operators, datatypes and proof rules for the development of his models.

Records Plug-in has been developed by University of Southampton before the mathematical extensions as a new feature to provide structured types in Event-B. The plug-in extends Rodin standard context editor with a new modelling construct to provide support for structured types, which can be defined in terms of two new clauses: record declarations and record extensions. Both enable users to define their custom reusable types, that are treated underline by Rodin as Event-B constant sets and relations, supported by additional axioms, which the plug-in generates to simplify the proofs.

Motivations

Main reasons for implementing mathematical extensions are:

• increased readability ($a \; \operatorname{OR} \; b$ rather than $\operatorname{bool}(a=TRUE \or b=TRUE)$)
• polymorphism ($l \in List(S \cprod T)$)
• decreased proving effort, thanks to extension specific proof rules instead of general purpose ones

Choices / Decisions

On the Core Rodin Platform side, implementing mathematical extensions required to make some parts of the code extensible, that were not designed to be so, namely the lexer and the parser. We were using tools that automatically generated them from a fixed grammar description, so we had to change to other technologies. A study has been made on available technologies. The Pratt algorithm was selected for its adequation with the purpose and it did not have the drawbacks of other technologies:

• foreign language integration
• overhead due to over generality

After a mocking up phase to verify feasibility, the Pratt algorithm has been confirmed as the chosen option and implemented in the Rodin Platform.

Besides, we wanted to set up a way to publish and share theories for Rodin users, in order to constitute a database of pre-built theories for everyone to use and contribute. This has been realised by adding a new tracker on SourceForge site ([1]).

Available Documentation

• Pre-studies (states of the art, proposals, discussions).
  • Proposals for Mathematical Extensions for Event-B
  • Mathematical Extension in Event-B through the Rodin Theory Component
  • [2]
  • Theoretical Description of Structured Types
• Technical details (specifications).
  • [3]
  • [4]
  • [5]
  • [6]
  • Records Extension Documentation
• Teaching materials (tutorials).
• User's guides.
  • [7]

Planning

This paragraph shall give a timeline and current status (as of 28 Jan 2011).

TODO: What will remain to do after Rodin 2.1 ?