Language of an Event-B Component

Since the introduction of mathematical extensions in Rodin 2.0, Event-B components can use extended version of the Event-B mathematical language. This change was implemented then, but there were some places where strange things could happen, weakening the confidence one can have in proofs.

This design document describes how this has been implemented in a better way in the core platform for Rodin 3.0.

Requirement

All Event-B formulas are stored on disk as plain character strings in the Rodin database (i.e., in XML files). It is therefore necessary to know in which language they have been written to be able to parse them back to a tree in memory. Conversely, the serialization of Event-B formulas need to know how to transform the tree in memory into a character string.

General Solution

The language information is implemented by an instance of org.eventb.core.ast.FormulaFactory. Each instance contains a dedicated parser and type-checker which allows to transform a character string into a tree (this operation is called de-serialization). Conversely, each formula tree has a formula factory attached to it which provides a way to transform it back into a string (this is operation is called serialization).

All what is needed then is to know which formula factory to use for deserializing an Event-B component. For most files, this information is provided by the Theory plug-in, which contributes to the org.eventb.core.formulaExtensionProvider extension point. Given an Event-B root, the object contributed to this extension point returns the formula factory to use for parsing its contents.

Unchecked machine and context files are written directly by the end-user and are parsed using the formula factory of their project. If the language changes, it is up to the user to update this file to make it parseable again, if need be.

As concerns generated files (e.g., statically checked files and proof obligation files), they contain formulas in the same language as the component from which they originate. Moreover, the Theory plug-in ensures that they are re-generated whenever the language of their respective component changes. This is implemented by adding a dependency in the Rodin builder to ensure that these files are considered obsolete when the language changes.

Proof status files do not contain any formula and are therefore independent on the Event-B mathematical language.

Solution for Proofs

The last kind of files are proof files which are a bit more delicate. These files are also considered as written by the end-users (sometimes helped by the automated prover working on their behalf). However, their structure is quite intricate and it is not conceivable to have end-user editing them directly. Instead, users have the Proving UI for editing them in a friendly manner.

As proofs are independent of the input component (machine or context), they need to have their own mechanism for retrieving their associated formula factory. This mechanism must be on a per proof basis, as proofs can be edited independently and therefore expressed in different languages across time.

The simplest solution would therefore be to serialize in each proof the formula factory with which it was built so that it can be parsed back.

However, this solution would waste a lot of space as most often all proofs would share the same formula factory. To mitigate this, we instead share a common formula factory at the root of the proof file, which is used by default by all proofs. For the proofs that are expressed in a different language, we store the formula factory in the proof node.

An Event-B model has been developed to prove that this factory sharing can be implemented soundly and serves as a specification of this optimization.

The last degree of freedom is the choice of the formula factory stored at the root. In a stable model, all proof obligations and proofs are expressed in the same language. It is therefore the factory for this language that should be stored at the root of the proof file. The platform should always ensure that this factory is kept in sync with the corresponding proof obligation file.