File Root Separation
Situation before separation
Rodin
In Rodin elements hierarchy, there exist 4 element types, in the following order:
- database
- project
- file
- internal element
Every element contains elements of the next type, except for internal elements which can contain other internal elements. Among those 4 types, 2 parts can be distinguished. The first part consists in elements peculiar to Rodin platform, that exist independently of any language. Their role stands at Rodin platform level and there is no interest in adapting them to any other level. More concretely, their Java implementation is the same for every one of them. This is the case of databases and projects. The second part is made of language level elements. These can have several implementations corresponding to the various language elements. In Java, this means having several classes (and interfaces) that inherit (implement) these types. This is typically the case of internal elements.
So far, we did not mention files. Actually, they are situated in between. Whereas, by definition, they serve as data containers, Rodin files are also typed. Thus, in Event-B, the various components are implemented at file level rather than at internal elements level. Furthermore, files behave the same way as internal elements towards their children. Thereby, both can contain several elements.
This situation presents two main drawbacks. Firstly, the code is globally more complicated. Secondly, it prevents from creating files that contain pieces of code. For example, this is useful to implement the cut/copy/paste.
EventB
In Event-B, files have several declensions, all inheriting from IEventBFile:
- IContextFile: context component
- IMachineFil : machine component
- IPOFile: proof obligation
- IPRFile: proof file
- IPSFile: proof status
- ISCContextFile: static checker for context files
- ISCMachineFile: static checker for machine files
Internal elements are directly added to the files. Thus, variables, invariants, theorems... are all direct children of a machine.
Goal after separation
Rodin
Database and project must not change. The goal is to move the dividing line between Rodin elements and language elements. There remains a single file implementation, and it can no longer have several children as before. Each file has an only child that is the root of all the elements it contains. Files are differentiated according to their root rather than through inheritance. From this point, only internal elements depend on the language.
Event B
There remains only one single file. Previous file declensions are represented by internal elements that serve as root element. Just like files, Event-B root elements have a common type IEventBRoot.
Realization
As the modification has an impact on a large amount of code, realization is achieved 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 could then focus on introducing the root element without being disturbed by a lot of other errors, that a more important change would have caused.
At first, we've been modifying all tests that concerned affected packages:
- org.rodinp.core.test
- org.eventb.core.test
- org.eventb.ui.test
until there were no more type errors, then we changed the code so that all tests passed.
When we previously used the file to add elements, we now use its root element. Similarly, when making a distinction between file types, the root element is taken into account. For example, editors that were parameterized with the file type now are with the root type: EventBEditor<IContextFile> becomes EventBEditor<IContextRoot>.
Second step
In a second step we removed file types so as to keep only root element types. The file becomes a Rodin side element, it no longer contains any type information. This entailed changes in package interface 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 hereinafter (and conversely).
Encountered issues
Mixed informations
The main issues were encountered when both file and root informations were needed. A recurring example concerns file retrieval according to its type. Let's 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. The required information was contained in file types. When files no longer have a type, we do not directly have this information. It depends on the root.
No information about type
Also, we met problems in processings in which object type was unknown, as for delta computation. 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.
