Rodin Handbook





 

3.4.7 Purging 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 has been worked out, obsolete proofs (i.e., 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.

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

Consequently, after a lot of model editing, more and more obsolete proofs are stored in proof files.

3.4.7.2 Selecting purge input

In any view, right-clicking an Event-B project or file will display a popup menu with a Purge Proofs... option. 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 proofs are found, a message will pop up informing the user that no proof needs to be purged. Otherwise, a new window will pop up displaying a list of all POs that are considered obsolete, i.e. all proofs that exist in some proof file and but no longer correspond to any concrete project or file.

3.4.7.3 Choosing proofs to delete

\includegraphics{img/reference/ref_10_proof_purger.png}
Figure 3.51: Proof Purger Selection Window

For the moment, nothing has been erased. The new window (see Figure 3.51) shows obsolete proofs and allows the user to choose among them and select the ones which 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, hit the Delete button to actually delete the selected proofs from the proof files. Files that become empty will be deleted as well.

3.4.7.4 Caution

Proof purging should not be performed on models that are not in a stable state. For instance, it should not be applied to a model that has some errors or warnings issued by the type checker. This is because if there are errors and warnings, not all proof obligations are generated. Therefore, some proofs may have been considered wrongly as obsolete.