Past Developments: Difference between revisions
imported>Laurent |
imported>Laurent →Deploy Tasks: Moved completed items for the core platform |
||
| Line 14: | Line 14: | ||
==== Mathematical Language V2 ==== | ==== Mathematical Language V2 ==== | ||
[[Changes to the Mathematical Language of Event-B]] and the corresponding [[Mathematical_Language_Evolution_Design|design]] documentation. | |||
[[Predicate_Variables_Extension|Predicate variables extension]] | |||
[[Mathematical_extensions|Proposals for mathematical extensions]] | |||
The generation of well-definedness lemmas has been improved: [[Improved_WD_Lemma_Generation| Improved WD lemma generation]]. | |||
==== Rodin Index Manager ==== | ==== Rodin Index Manager ==== | ||
| Line 21: | Line 26: | ||
{{details|Rodin Index Design|Rodin index design}} | {{details|Rodin Index Design|Rodin index design}} | ||
The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them. | The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them. | ||
==== New Tactic Providers ==== | |||
[[Systerel]] was in charge of this task. | |||
{{details|New Tactic Providers|New Tactic Providers}} | |||
The purpose is to give more flexibility to tactic providers by allowing them to provide as many tactic applications as they will for a given proof node, even they apply to the same predicate and at the same position. | |||
==== Generated Model Elements ==== | |||
[[Systerel]] is in charge of this task. | |||
Elements of a model can be tagged as generated by a tool, in order to prevent the end-user from directly editing them (and their descendants). | |||
{{details|Generated Model Elements|Generated Model Elements}} | |||
== Exploratory Tasks == | == Exploratory Tasks == | ||
Revision as of 13:43, 31 March 2011
This page sum up the developments recently done around or for the Rodin Platform, which are integrated or compatibles with the last platform revision.
Deploy Tasks
The following tasks were planned at some stage of the Deploy project.
Core Platform
Undo / Redo for editors
- See also: Undo/Redo design
Systerel is in charge of this task.
The goal of this task is to implement an undo/redo feature for editing actions.
This feature is now part of Rodin v0.9.0.
Mathematical Language V2
Changes to the Mathematical Language of Event-B and the corresponding design documentation.
Proposals for mathematical extensions
The generation of well-definedness lemmas has been improved: Improved WD lemma generation.
Rodin Index Manager
Systerel is in charge of this task.
- For more details on Rodin index design, see Rodin Index Design.
The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.
New Tactic Providers
Systerel was in charge of this task.
- For more details on New Tactic Providers, see New Tactic Providers.
The purpose is to give more flexibility to tactic providers by allowing them to provide as many tactic applications as they will for a given proof node, even they apply to the same predicate and at the same position.
Generated Model Elements
Systerel is in charge of this task. Elements of a model can be tagged as generated by a tool, in order to prevent the end-user from directly editing them (and their descendants).
- For more details on Generated Model Elements, see Generated Model Elements.
Exploratory Tasks
One Single View
Maria Husmann was in charge of this exploratory work during her internship at Systerel.
- For more details on Single View Design, see Single View Design.
The goal of this project was to present everything in a single view in Rodin. So the user do not have to switch perspectives.
This work has been integrated into Rodin 0.9.2.
Plug-ins
Requirement Management Plug-in
Michael at Düsseldorf is in charge of the Requirements Management Plug-in.
- See also: Requirements Management Plug-in and Requirements Tutorial
This plug-in allows:
- Requirements to be edited in a set of documents (independently from Rodin)
- Requirements to be viewed within Rodin
- Individual Requirements to be linked to individual Event-B-Entities
- A basic completion test to be performed
