Records Extension

This page is under development. It is intended to be a user oriented manual for using records in Event-B. This page should be read in conjunction with the Structured Types page which gives a more theoretical description of the origin of the Records extension.

Introduction

The Event-B mathematical language currently does not support a syntax for the direct definition of structured types such as records or class structures. The Records Extension introduces a new modelling construct to provide a notion of structured types in Event-B Contexts.

Currently, structured variables are not supported. Variables that are typed as an instance of a record type can be thought of as identifying a particular record value. Hence it is not possible to vary an individual field, the variable must be assigned a complete new record value instance. To vary an individual field this new record value instance can be selected to have the same field value for every other field.)

UI Extensions

The Event-B editor is extended to include two new top level clauses. These are Record Declarations and Record Extensions.

Records (or sub-records) are introduced in the Record Declarations clause. Records that are introduced here without a Supertypes clause are equivalent to carrier sets. Those that have a Supertypes clause are equivalent to constants that are a subset of the referenced (i.e. subtyped) record or carrier set.

Record Extensions may only add new fields to a record that has previously been declared in a Record Declaration. The extended record is referenced in an 'extends' clause.

Record Declaration clause also contains a toggle button to control the record's closure property. A closed record cannot be subtyped by other records or extended by record extensions.

The Event-B navigator is extended to show a new node Records. Under this node are listed the records and records extensions in the Context. Record Extensions are displayed as the name of the extended record appended with a + sign. Each record or record extension can be expanded to show the owned fields. (Note that this list is not cumulative, only the new fields are shown). (Currently in the Navigator, the Records node is shown as the first item in the Context whereas eleswhere it appears between carrier sets and constants. This is due to a limitation in the Rodin tool extension facilities).

The Outline panel shows the records followed by record extensions as a plain list without the Records node. Again, the record or record extension can be expanded to show the fields.

In all cases, the icon used for a record reflects its equivalence. That is, if it does not have a supertypes clause, it is displayed with the same icon as a carrier set. otherwise it is displayed with the same icon as a constant.

Semantics of Records

The semantics of Records are given by their translation into 'pure' Event-B. This translation is performed by extensions to the static checker which generates a 'checked context' (.BCC file) containing pure Event-B from an unchecked (.BUC file) containing record elements. Hence the translated Event-B is not visible to the user.

$\textbf{ RECORD}~~~~ R$	$\textbf{~~SET}~~~~ R$
$\textbf{ RECORD}~~~~ R, ~~~~\textbf{SUPERTYPE}~~~~ S ~~~~$	$\textbf{~~CONSTANT}~~~~ R , ~~~~\textbf{AXIOM}~~~~ R \in \pow (S) ~~~~$
$\textbf{ FIELD}~~~~ f \in F$	$\textbf{~~CONSTANT}~~~~ f , ~~~~\textbf{AXIOM}~~~~ f \in R \rightarrow F ~~~~$

[It may be instructive to open the *.bcc file with a text editor to examine the generated carrier sets, constants, and axioms]

Usage

First define Records in the Record Declarations section. Some of these can subtype others but you need at least one that is not a subset, i.e. has no supertypes. Note that we decided not to allow records to subtype or extend Carrier Sets, but you can do the equivalent by defining a record without any fields and subtyping/extending that. To be correctly static-checked record definitions must be in order of their referencing i.e. a subtype record would follow a supertype record which it references (to know about its type). In opposite case static checker will show a typing problem.

Add fields and give them a type by entering an expression that evaluates to a set. Note that this expression must be a basic type expression. You can use records, constants and sets in the expression.

After a record is defined it can be declared as closed using a toggle button in its Record Declaration clause. When record is closed it cannot be subtyped or extended anymore. Another effect of closing a record is that additional axioms are generated for it in the checked context. These include a closure axiom, a make-function for the record and an update-function for each of its fields (also for derived fields from supertype records). Another axiom — feasibility axiom — is generated for every record independent of its closure attribute.

For Record Extensions just select the record you want to add new fields to from the drop down list and then add the new fields. Only open (not closed) records can be extended, although the drop down list contains all the declared records.

You can refer to records and fields in axioms/theorems. E.g., you could define a constant to be an instance of a record. In all cases you can refer to records and fields in the current or visible abstract (extended*) contexts.

You use fields as if they were functions (which is what they are in the checked context).

e.g. if $r$ belongs to $myRecord$ which has a field, $myField \in \nat$ then I could write in a predicate $myField(r) > 5$.

Proving With Records

The prover will refer to records as sets and constants, and to fields as constants. Therefore for proving you may need to be aware of this.

Axioms that are automatically generated for typing records and their fields will have automatically generated labels and these may be referenced in the prover interface.

The automatically generated labels use an easy to interpret format:

• Subtype Record typing axioms are in the format <recordName>.type<d> (where d is a decimal digit appended to ensure there are no name clashes)
• Field typing axioms are in the format <recordName>.<fieldName>.type<d> (where d is a decimal digit appended to ensure there are no name clashes)

Other axioms use record and field labels in their labelling, which leads to a longer and slightly confusing but still interpretable format:

• Feasibility axioms are in the format <recordName>.feasibility (or <recordName>.feasibility.ext<n> in case of record extensions)
• Closure axioms are in the format <recordName>.closure
• Make function's 1st axiom (function's typing) is in the format <recordName>.make.axm1
• Make function's 2nd axiom (for each field) is in the format <recordName>.<fieldName>.make.axm2
• Update function's 1st axiom (record field update function's typing) is in the format <recordName>.<fieldName>.update.axm1
• Update function's 2nd axiom (equivalence to record construction with a specific value of updated field) is in the format <recordName>.<fieldName>.update.axm2

Current Limitations

• Records are not supported by the Camille text editor (see warning below)
• Records are not supported by the Pretty print facility
• Records are not supported by the Synthesis view facility
• Records are not supported by the EventB2Latex plug-in
• Records are not supported by the Refactoring plug-in
• Records are partially supported by the Decomposition plug-in (Machines that use records can be decomposed, but the Context that contains the record cannot).
• Records may have, at most, one supertype.
• Records may only have records as supertypes (not carrier sets)
• There is no finalisation of a record - hence make functions are not supported

Warning

Records are not supported in the Camille text editor. Editing a context that contains records with the Camille editor may result in the Records being lost.