Difference between revisions of "Teamwork Requirements"

From Event-B
Jump to navigationJump to search
imported>Colin
(New page: ''' Requirements for an Event-B Teamwork Plug-in. == Navigator pop-up menu == A pop-up menu should be provided in the Event-B navigator for Machine and Context model elements. (currently ...)
 
imported>Felix-loesch
Line 3: Line 3:
 
== Navigator pop-up menu ==
 
== Navigator pop-up menu ==
 
A pop-up menu should be provided in the Event-B navigator for Machine and Context model elements. (currently the menu is only available on Files).
 
A pop-up menu should be provided in the Event-B navigator for Machine and Context model elements. (currently the menu is only available on Files).
 +
 +
== Merging of proof files ==
 +
It would be great if two people work independtly on different proofs that the discharged proof obligations could be merged. A first version of
 +
proof merging could restrict the use to cases in which the machine / contexts have not changed.

Revision as of 09:56, 22 October 2009

Requirements for an Event-B Teamwork Plug-in.

Navigator pop-up menu

A pop-up menu should be provided in the Event-B navigator for Machine and Context model elements. (currently the menu is only available on Files).

Merging of proof files

It would be great if two people work independtly on different proofs that the discharged proof obligations could be merged. A first version of proof merging could restrict the use to cases in which the machine / contexts have not changed.