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.

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.

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.

<formatting/presentation of this will be improved>

Record R Supertypes <null> --> Carrier Set R

Record S Supertypes R --> Constant S, Axiom S : POW(R)

Field f : F --> Constant f, Axiom f : R --> 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. Add fields and give them a type by entering an expression that evaluates to a set. (You can use records, fields, constants and sets in the expression).

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.

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 r1, belongs to myRecord which has a field myField : NAT then I could write in a predicate... myField(r1) > 5

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 Decomposition plug-in (Machines that use records can not be decomposed).
• Records may have, at most, one supertype.
• Records may only have records as supertypes (not carrier sets)
• There is 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.