Menu

#700 Renaming makes all proofs automatic

3.1
open
nobody
5
2013-11-13
2013-11-13
No

When renaming an event, all proof obligations get marked automatic even if they were initially manual. However, if one cleans the project afterwards, the manual proofs recover their original status (i.e., are no longer automatic).

To reproduce this bug, start with a vanilla Rodin 2.8 and install the Renaming plugin (Utilities > Renaming Refactory 1.2.2 from the Rodin update site). Then import the attached project. It contains proof "m/evt2/inv1/INV" which is manual.

In the Event-B explorer, select the evt event and click "Refactory…" then type evt2 and click Next twice, then Finish. The proof becomes automated. It should have stayed manual.

1 Attachments

Discussion


Log in to post a comment.

MongoDB Logo MongoDB