imported>Tommy |
imported>Andy |
| Line 1: |
Line 1: |
| − | The UI in Rodin 2.x contains an extension point <tt>org.eventb.ui.editorItems</tt> that groups the both following information: | + | == The Theory Plug-in == |
| − | *the definition of elements and attributes and their hierarchy,
| + | The theory plug-in is used to add mathematical extensions to Rodin. The theories are created, and deployed, and can then be used in any models in the workspace. When dealing with implementation level models, such as in Tasking Event-B, we need to consider how to translate newly added types and operators into code. We have augmented the theory interface with a Translation Rules section. This enables a user to define translation rules that map Event-B formulas to code. |
| − | *the information needed to correctly display these elements in the various editors and UI components.
| + | === Translation Rules=== |
| | + | Figure 1 shows the interface, and some translations rules of the mapping to Ada. |
| | | | |
| − | It appears obvious that the first information should be defined from an extension that belongs to the Database.
| + | <div id="fig:Translation Rules"> |
| − | To fullfil the above statement, the current extension point <tt>org.eventb.ui.editorItems</tt> should be split in two.
| + | <br/> |
| | + | [[Image:TheoryCGRules.png|center||caption text]] |
| | + | <center>'''Figure 1''': Translation Rules</center> |
| | + | <br/> |
| | + | </div> |
| | | | |
| − | = Behaviour =
| + | The translation rules are templates used for pattern matching. The meta-variables are defined and typed, and used in the rules. Event-B expressions and predicates are defined on the left hand side of the rule, and the code to be output (as text) appears on the right hand side of the matching rule. |
| − | | |
| − | | |
| − | = Proposal =
| |
| − | | |
| − | == Hierarchy between elements ==
| |
| − | | |
| − | The part concerning element definition and hierarchy will go to a dedicated extension point in the database.<br> | |
| − | Here is the definition of such an extension point : org.rodinp.core.dataModel ??? or org.rodinp.core.internalElementHierarchy ???
| |
| − | | |
| − | Configuration Markup:
| |
| − | <!ELEMENT extension ((childRelation | attributeRelation | autoNaming)+)>
| |
| − | <!ATTLIST extension
| |
| − | point CDATA #REQUIRED
| |
| − | id CDATA #IMPLIED
| |
| − | name CDATA #IMPLIED
| |
| − | >
| |
| − |
| |
| − | <!ELEMENT elementRelationship (childType)+>
| |
| − | <!ATTLIST elementRelationship
| |
| − | parentTypeId CDATA #REQUIRED
| |
| − | >
| |
| − | parentTypeId - Element type of the parent, must be the unique ID of a Rodin internal element type (see extension point org.rodinp.core.internalElementTypes).
| |
| − |
| |
| − | <!ELEMENT childType EMPTY>
| |
| − | <!ATTLIST childType
| |
| − | typeId CDATA #REQUIRED
| |
| − | implicitChildProvider CDATA #IMPLIED
| |
| − | >
| |
| − | typeId - Element type of the child, must be the unique ID of a Rodin internal element type (see extension point org.rodinp.core.internalElementTypes).
| |
| − |
| |
| − | <!ELEMENT attributeRelationship (attributeType)+>
| |
| − | <!ATTLIST attributeRelationship
| |
| − | elementTypeId CDATA #REQUIRED
| |
| − | >
| |
| − | elementTypeId - Element type of the element, must be the unique ID of a Rodin internal element type (see extension point org.rodinp.core.internalElementTypes).
| |
| − |
| |
| − | <!ELEMENT attributeType EMPTY>
| |
| − | <!ATTLIST attributeType
| |
| − | typeId CDATA #REQUIRED
| |
| − | class CDATA #REQUIRED
| |
| − | >
| |
| − | Describes how to graphically display a Rodin attribute of type boolean.
| |
| − |
| |
| − | attributeTypeId - Id of the Rodin attribute type to which this description applies (see extension point org.rodinp.core.attributeTypes).
| |
| − |
| |
| − | <!ELEMENT autoNaming EMPTY>
| |
| − | <!ATTLIST autoNaming
| |
| − | elementTypeId CDATA #REQUIRED
| |
| − | attributeDescriptionId CDATA #REQUIRED
| |
| − | namePrefix CDATA #REQUIRED
| |
| − | >
| |
| − | Describes how to automatically name an element. The autoNaming definition is unique for a given element type.
| |
| − |
| |
| − | elementTypeId - Element type of the element, must be the unique ID of a Rodin internal element type (see extension point org.rodinp.core.internalElementTypes).
| |
| − | namePrefix - default prefix to name the element
| |
| − |
| |
| − | | |
| − | *The part concerning how to display elements and UI related info will stay in the editorItems extension point and shall point to an element definitions and hierachy.
| |
| − | | |
| − | = Some identified difficulties =
| |
| − | | |
| − | == Initialization of elements from non UI components ==
| |
| − | | |
| − | The following ElementDescRegistry method, shows the dependency between an element creation and the initialization of its attributes with default values.
| |
| − | | |
| − | public <T extends IInternalElement> T createElement(
| |
| − | final IInternalElement root, IInternalElement parent,
| |
| − | final IInternalElementType<T> type, final IInternalElement sibling)
| |
| − | throws RodinDBException {
| |
| − | final T newElement = parent.createChild(type, sibling, null);
| |
| − | final IAttributeDesc[] attrDesc = getAttributes(type);
| |
| − | for (IAttributeDesc desc : attrDesc) {
| |
| − | desc.getManipulation().setDefaultValue(newElement, null);
| |
| − | }
| |
| − | return newElement;
| |
| − | }
| |
| − | | |
| − | The protocol shall be changed to take into account this initialization.
| |
| − | Doing the initialization the org.eventb.core level possible by registering a special "attribute initializer".
| |
| − | ----
| |
| − | | |
| − | The proposal should concern :
| |
| − | - Relationship declaration (new extension point)
| |
| − | - API to test these relations and traverse them
| |
| − | - Enforcement of the authorized relations when modifying the DB
| |
| − | - Behaviour while loading a file (including a file with invalid parent-child relations occurrences)
| |
| − | - What about the compatibilty with the file upgrade mechanism?
| |
| − | | |
| − | [[Category:Design_proposal]]
| |
The Theory Plug-in
The theory plug-in is used to add mathematical extensions to Rodin. The theories are created, and deployed, and can then be used in any models in the workspace. When dealing with implementation level models, such as in Tasking Event-B, we need to consider how to translate newly added types and operators into code. We have augmented the theory interface with a Translation Rules section. This enables a user to define translation rules that map Event-B formulas to code.
Translation Rules
Figure 1 shows the interface, and some translations rules of the mapping to Ada.
Figure 1: Translation Rules
The translation rules are templates used for pattern matching. The meta-variables are defined and typed, and used in the rules. Event-B expressions and predicates are defined on the left hand side of the rule, and the code to be output (as text) appears on the right hand side of the matching rule.
