File Root Separation: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Nicolas
mNo edit summary
imported>Laurent
mNo edit summary
 
(3 intermediate revisions by 2 users not shown)
Line 1: Line 1:
=Situation before 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


==Rodin==
[[Image:element_avant_separation.png|right|350px|IRodinElement]]
[[Image:element_avant_separation.png|right|350px|IRodinElement]]


In Rodin elements hierarchy, there exist 4 element types, in the following order:
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.


* database
The last category (internal elements) corresponds to elements that are specific
* project
to a modeling notation.  These elements can have several implementations
* file
corresponding to various notation elements.  Also, these elements carry
* internal element
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.


Every element contains elements of the next type, except for internal elements which can contain other internal elements.
In the original database design, file elements are hybrid as they fall in both
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.
kinds: they have a resource counterpart (an Eclipse file) and can carry
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.
attributes (and be implemented by client-contributed Java classes).


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.
It was found out at the end of the Rodin project, that this design decision was
bad for several reasons:


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.
* it forced to distinguish between <tt>SCContextFile</tt> and <tt>SCInternalContext</tt> in static checked files


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


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.
=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.


=Goal after separation=
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.


==Rodin==
[[Image:element_apres_separation.png|right|350px|IRodinElement]]
[[Image:element_apres_separation.png|right|350px|IRodinElement]]


Database and project must not change. The goal is to move the dividing line between Rodin elements and language elements.
=Consequences for Event-B=
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.
In the original design of the event-B customisation of the Rodin database,
Files are differentiated according to their root rather than through inheritance.
files are represented by several Java intefaces, all inheriting from
From this point, only internal elements depend on the language.
<tt>IEventBFile</tt>:
* <tt>IContextFile</tt>: unchecked context file
* <tt>IMachineFile</tt> : unchecked machine file
* <tt>ISCContextFile</tt>: static checked context files
* <tt>ISCMachineFile</tt>: static checked machine files
* <tt>IPOFile</tt>: proof obligation file
* <tt>IPRFile</tt>: proof file
* <tt>IPSFile</tt>: proof status file


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


==Event B==
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 <tt>File</tt> with <tt>Root</tt>.  For instance, all
the elements of an event-B machine are children of an instance of
<tt>IMachineRoot</tt>.


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=
=Implementation Plan=


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


==First step==
==First Step==


Firstly, the root element is introduced while keeping file types. Adding children to files also remains possible.
Firstly, the root element is introduced while keeping file types.
Having this intermediate step where file types and root elements coexist allows to work on the modification without breaking the entire code.
Adding children to files also remains possible. Having this intermediate step
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.
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.


At first, we've been modifying all tests that concerned affected packages:
We start by modifiying all tests that concern affected packages:
* '''org.rodinp.core.test'''
* <tt>org.rodinp.core.test</tt>
* '''org.eventb.core.test'''
* <tt>org.eventb.core.test</tt>
* '''org.eventb.ui.test'''
* <tt>org.eventb.ui.test</tt>


until there were no more type errors, then we changed the code so that all tests passed.
until there is no more type-checking errors, then we change the code to make
the tests pass.


When we previously used the file to add elements, we now use its root element.
When a file is used to add elements, it is replaced by its root element.
Similarly, when making a distinction between file types, the root element is taken into account.
Similarly, distinctions based on file types are replaced by distinctions on
For example, editors that were parameterized with the file type now are with the root type: EventBEditor<IContextFile> becomes EventBEditor<IContextRoot>.
root element types. For instance, editors, that were parameterized with a file
type, take now a root element type parameter:
<tt>EventBEditor&lt;IContextFile&gt;</tt> becomes
<tt>EventBEditor&lt;IContextRoot&gt;</tt>.


==Second step==
==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.
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==
==Compatibility==


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




=Encountered issues=
=Issues Encountered=


==Mixed informations==
==Mixed Information==


The main issues were encountered when both file and root informations were needed.
The main issues we had to address happen when both file and root information
A recurring example concerns file retrieval according to its type. Let's consider the simple case of the project explorer.
were needed. A recurring example concerns file retrieval according to its
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.
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==
==No Information about Type==


Also, we met problems in processings in which object type was unknown, as for delta computation.
Also, we met problems in pieces of code where the element type is not known a
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.
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.


[[Category:Design]]
[[Category:Design]]
[[Category:Developer documentation]]

Latest revision as of 11:47, 29 January 2009

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
IRodinElement
IRodinElement

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.

IRodinElement
IRodinElement

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.

Retrieved from ‘https://wiki.event-b.org/index.php?title=File_Root_Separation&oldid=5255’