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.

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

TODO: add pdf mathextn from BSCW

• Requirements.
• Pre-studies (states of the art, proposals, discussions).
  • [2]
  • [3]
  • [4]
• Technical details (specifications).
  • [5]
  • [6]
  • [7]
  • [8]
• Teaching materials (tutorials).
• User's guides.
  • [9]

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 ?