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

The motivation for development of Records plug-in was to fill the gap in Event-B language - a missing support of a syntax for the direct definition of structured types. Some of the industrial partners expressed a desire to have this missing feature in Event-B, that would allow them to define their own structured types such as records or classes. Theoretically these structures could be modelled with existing Event-B capabilities via projection functions. Backed up by a refined theoretical proposal Records plug-in was developed to extend the standard Event-B notation with requested capability.

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]).

Records plug-in required the extension of the Rodin database with the new constructs to support structured types. On the other hand the Event-B language itself did not support extension at that time. For that reason the decision was made to address extensibility problem at the lowest level possible, which was Rodin database, but to model structured types using standard Event-B notation at the level below. The translation from extended to standard syntax has been entrusted to the static checker, that was also extended for this purpose. Thus the plug-in provides the users with notation for record declarations and extensions in unchecked models, but the checked versions operate with standard Event-B constructs.

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 ?