Difference between revisions of "Proof Purger Interface"

From Event-B
Jump to navigationJump to search
imported>Nicolas
(New page: ==Purpose== Proofs are stored in proof files. But it can happen quite often that proof obligations disappear, leaving unnecessary proofs in files. The purpose of the proof purger is to al...)
 
imported>Ladenberger
 
(8 intermediate revisions by 4 users not shown)
Line 1: Line 1:
 
==Purpose==
 
==Purpose==
  
Proofs are stored in proof files. But it can happen quite often that proof obligations disappear, leaving unnecessary proofs in files. The purpose of the proof purger is to allow the user to get rid of these proofs.
+
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 "Purge Proofs..." item.
+
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 unused proofs in the selection.
+
Firstly, the proof purger tries to find obsolete proofs in the selection. If
If none are found, a message will appear telling that no proof needs to be purged.
+
no obsolete proof is found, a message will pop up telling that no proof needs
Else, a new window will show the result.
+
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 unused 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.
+
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.
  
Once the selection has been decided, clicking the "Delete" button will actually delete selected proofs from proof files.
+
[[Category:User documentation]]
Files becoming empty will be deleted as well.
+
[[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 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 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

SelectProofsToDelete.jpg

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