File Root Separation

Motivation

The Rodin database is a tree whose nodes are called Rodin elements. These elements are organized in four categories:

• database root
• project
• file
• internal element

The first two categories (database root and project) correspond to elements that exist independently of any modeling notation. These elements are the Rodin counterpart of resources that populate the Eclipse workspace.

The last category (internal elements) corresponds to elements that are specific to a modeling notation. These elements can have several implementations corresponding to various notation elements. Also, these elements carry attributes that have a semantic defined by the notation that they implement. Clients can define specialised Java interfaces and classes for representing these internal elements in memory.

In the original database design, file elements are hybrid as they fall in both kinds: they have a resource counterpart (an Eclipse file) and can carry attributes (and be implemented by client-contributed Java classes).

It was found out at the end of the Rodin project, that this design decision was bad for several reasons:

• it forced to distinguish between SCContextFile and SCInternalContext in static checked files

• it prevented the introduction of database snippets (that is file-like temporary elements that would reside only in memory).

New Database Design

In the new database design, file elements are now like database and project elements. They just correspond to Eclipse resources and cannot be tailored to any notation.

The link between files and internal elements is done through a root element. A root element is an internal element whose parent is a file. A file contains exactly one root element. All other internal elements contained within a file are then descendants of its root element.

Consequences for Event-B

In the original design of the event-B customisation of the Rodin database, files are represented by several Java intefaces, all inheriting from IEventBFile:

• IContextFile: unchecked context file
• IMachineFile : unchecked machine file
• ISCContextFile: static checked context files
• ISCMachineFile: static checked machine files
• IPOFile: proof obligation file
• IPRFile: proof file
• IPSFile: proof status file

Internal elements are direct children of these files. For instance, variables, invariants, events, etc. are all direct children of a machine.

After the Rodin database is changed, no difference is made any more between event-B files. All usage of event-B files should be replaced by use of the corresponding event-B roots. These interfaces are named the same as the former file interfaces, replacing File with Root. For instance, all the elements of an event-B machine are children of an instance of IMachineRoot.

Implementation Plan

As the modification has an impact on a large amount of code, it has been implemented in two steps.

First Step

Firstly, the root element is introduced while keeping file types. Adding children to files also remains possible. Having this intermediate step where file types and root elements coexist allows to work on the modification without breaking the entire code. We can then focus on introducing the root element without being disturbed by a lot of other errors, that a more important change would have caused.

We start by modifiying all tests that concern affected packages:

• org.rodinp.core.test
• org.eventb.core.test
• org.eventb.ui.test

until there is no more type-checking errors, then we change the code to make the tests pass.

When a file is used to add elements, it is replaced by its root element. Similarly, distinctions based on file types are replaced by distinctions on root element types. For instance, editors, that were parameterized with a file type, take now a root element type parameter: EventBEditor<IContextFile> becomes EventBEditor<IContextRoot>.

Second Step

Secondly, all remaining references to file types are replaced by root element types. Files become pure Rodin elements, they no longer contain any type information. This entailes changes in package interfaces and data saving.

Compatibility

Obviously enough, the modification did not bring any compatibility problem with projects. Projects created with a version anterior to the separation remain compatible with those created after (and conversely).

Issues Encountered

Mixed Information

The main issues we had to address happen when both file and root information were needed. A recurring example concerns file retrieval according to its type. Let us consider the simple case of the project explorer. For a given project, it displays files by distinguishing machines and contexts. Before the separation, retrieving context children and machine children was enough to populate the project explorer. The required information was contained in file types. When files no longer have a type, we do not directly have this information. We had to retrieve the type of the root element file to know its precise contents.

No Information about Type

Also, we met problems in pieces of code where the element type is not known a priori, for instance during delta processing. Deltas give the difference between two database snapshots. In this case, before the separation, we were only expecting a file, no matter if the processing was to be made on the "file" or on the "internal element" part. During the modification, it became quite hard to guess which object was retrieved.