Proof Purger Interface: Difference between revisions
imported>Mathieu m Use some typesetting template |
imported>Ladenberger No edit summary |
||
| (6 intermediate revisions by 4 users not shown) | |||
| Line 1: | Line 1: | ||
==Purpose== | ==Purpose== | ||
Proofs are stored in proof files. | Proofs are stored in proof files. Each time a new proof obligation is generated | ||
by the tool, a corresponding (initially empty) proof is created. However, | |||
proofs are never removed automatically by the Rodin platform. As time passes | |||
and a model is worked out, obsolete proofs (e.g., proofs that do not have a | |||
corresponding proof obligation anymore) accumulate and clutter proof files. | |||
The purpose of the proof purger is to allow the user to delete obsolete proofs. | |||
==Why proofs become obsolete== | |||
Proof obligations are named after the main elements related to it, such as | |||
events and invariants. Therefore, each time such an element is renamed | |||
manually, the corresponding proof obligations get a new name. However, the | |||
existing proof is not renamed, and a new proof gets created with the new name. | |||
Therefore, after a lot of model editing, there are more and more obsolete | |||
proofs stored in proof files. | |||
==Selecting purge input== | ==Selecting purge input== | ||
In any view, right-clicking an Event-B project or file will display a popup menu, containing a {{menu|Purge Proofs...}} | In any view, right-clicking an Event-B project or file will display a popup | ||
If several files or projects (or both) are selected, purging will apply to all of them. | menu, containing a {{menu|Purge Proofs...}} entry. If several files or projects | ||
(or both) are selected, purging will apply to all of them. | |||
Firstly, the proof purger tries to find | Firstly, the proof purger tries to find obsolete proofs in the selection. If | ||
no obsolete proof is found, a message will pop up telling that no proof needs | |||
to be purged. Otherwise, a new window will pop up displaying a list of all POs | |||
that are considered obsolete, that is all proofs that exist in some proof file | |||
and that do not have any corresponding proof obligation. | |||
==Choosing proofs to delete== | ==Choosing proofs to delete== | ||
| Line 16: | Line 35: | ||
[[Image:selectProofsToDelete.jpg]] | [[Image:selectProofsToDelete.jpg]] | ||
For the moment, nothing has been erased. The new window shows | For the moment, nothing has been erased. The new window shows obsolete proofs | ||
and offers to choose among them which ones should be deleted. One may wish to | |||
keep some of them, knowing they might be useful in the future. | |||
Once the selection has been decided, clicking the {{button|Delete}} button will | |||
actually delete selected proofs from proof files. Files becoming empty will be | |||
deleted as well. | |||
==Caution== | |||
Proof purging shall not be performed on models that are not in a stable state. | |||
For instance, it should not be applied to a model that bears some errors or | |||
warnings issued by the type checker. This is because, in case of errors and | |||
warnings, it can happen that not all proof obligations are generated. | |||
Therefore, some proofs could be considered wrongly as obsolete. | |||
[[Category:User documentation]] | [[Category:User documentation]] | ||
[[Category:Proof]] | |||
Latest revision as of 10:20, 27 October 2011
Purpose
Proofs are stored in proof files. Each time a new proof obligation is generated by the tool, a corresponding (initially empty) proof is created. However, proofs are never removed automatically by the Rodin platform. As time passes and a model is worked out, obsolete proofs (e.g., proofs that do not have a corresponding proof obligation anymore) accumulate and clutter proof files.
The purpose of the proof purger is to allow the user to delete obsolete proofs.
Why proofs become obsolete
Proof obligations are named after the main elements related to it, such as events and invariants. Therefore, each time such an element is renamed manually, the corresponding proof obligations get a new name. However, the existing proof is not renamed, and a new proof gets created with the new name.
Therefore, after a lot of model editing, there are more and more obsolete proofs stored in proof files.
Selecting purge input
In any view, right-clicking an Event-B project or file will display a popup menu, containing a entry. If several files or projects (or both) are selected, purging will apply to all of them.
Firstly, the proof purger tries to find obsolete proofs in the selection. If no obsolete proof is found, a message will pop up telling that no proof needs to be purged. Otherwise, a new window will pop up displaying a list of all POs that are considered obsolete, that is all proofs that exist in some proof file and that do not have any corresponding proof obligation.
Choosing proofs to delete
For the moment, nothing has been erased. The new window shows obsolete proofs and offers to choose among them which ones should be deleted. One may wish to keep some of them, knowing they might be useful in the future.
Once the selection has been decided, clicking the button will actually delete selected proofs from proof files. Files becoming empty will be deleted as well.
Caution
Proof purging shall not be performed on models that are not in a stable state. For instance, it should not be applied to a model that bears some errors or warnings issued by the type checker. This is because, in case of errors and warnings, it can happen that not all proof obligations are generated. Therefore, some proofs could be considered wrongly as obsolete.
