Scenarios for Merging Proofs

This page is a first tentative to describe the scenario that a merge tool will have to face.

Proof structure

With respect to the merging objective, a proof is made of:

1. a component name,
2. a unique identifier inside that component, which is same as the PO identifier,
3. a proof tree, either manual or automatic,
4. a proof status (PO discharged or not by the proof tree)
5. a PO sequent

Rodin database implementation

Each component

compname

is associated with:

• a
  compname.bpr
  file, which contains the proof trees associated with each PO (1/, 2/ and 3/ before).
• a
  compname.bps
  file, which contains the proof status associated with each PO (2/, 5/ and 3/ - discharged or not, manual or automatic)
• a
  compname.bpo
  file, which contains the PO (1/ and 2/ + PO content).

Merging scenarios

Simple scenarios (need database evolution)

While discussing about the merge topic, it appears that another wanted and related feature is multi-proof database, where the

compname.bpr

file contains not only the current proof (called main proof), but also all the proof that weere once used to proof the po.

Complicated scenarios

Those scenarios are kept for reference PO being uniquely identified, it may be enough to consider a merge taking place PO by PO.

In the following we call L the local database/user/branch, O the other database/user/branch and A the database which reflects the common state from which L and O have departed (A, for ancestor). We also consider L and O as being symmetrical (and thus we won't describe symmetrical scenarios).

The table hereafter described the envisioned use case.

n°	A st	L st	O st	A ma	L ma	O ma	PO L	PO O	PR L	PR O	Actions
1	-	nok	nok	-	-	-	=A	/=A	-	-	get PR O (O model has changed)
2	nok	nok	nok	-	-	-	=A	=A	/=A	=A	get PR L (L has perhaps tried a demo)
3	nok	nok	nok	-	-	-	=A	=A	/=A	/=A	ask user (both PR changed)
4	nok	nok	nok	-	-	-	=A	=A	=A	=A	get PR L (or O, no difference)
5	nok	ok	nok	-	-	-	-	-	-	-	get PR L
6	nok	ok	ok	-	-	-	=A	/=A	-	-	get PR O, (O model has changed)
7	nok	ok	ok	-	-	-	=A	=A	-	-	ask user (both demo are ok)
8	nok	ok	ok	-	-	-	=A	=A	-	-	ask user (both model have changed)
9	ok	nok	nok	-	-	-	=A	=A	/=A	-	get PR A (model has not changed and was proved)
10	ok	nok	nok	-	-	-	=A	=A	=A	=A	get PR A (model has not changed and was proved)
11	ok	ok	nok	-	-	-	=A	=A	-	-	get PR L (no model has changed)
12	ok	ok	nok	-	ma	au	=A	/=A	-	-	get PR L (O model has changed but L had a manual proof)
13	ok	ok	nok	-	au	ma	=A	/=A	-	-	get PR O (O model has changed and has a manual proof)
14	ok	ok	nok	-	ma	ma	=A	/=A	-	/=A	get PR O (O model has changed and has a new manual proof)
15	ok	ok	nok	-	ma	ma	=A	/=A	-	=A	get PR O (O model has changed)
16	ok	ok	nok	-	au	au	=A	/=A	-	-	get PR O (O model has changed)
17	ok	ok	nok	-	ma	au	/=A	/=A	-	-	get PR L (both model changed but L had a manual proof)
18	ok	ok	nok	-	ma	ma	/=A	/=A	-	-	ask user (both model changed with manual proof)
19	ok	ok	nok	-	au	au	/=A	/=A	-	-	ask user (both model changed with manual proof)

X st: (ok,nok) proof status for X (A,O or L)

X ma: (manual, automatic) manual status for X (A,O or L)

PO X: po changes for X compare to others user/branch

PR X: proof change for X, compared to others user/branch

User interactions

When asked, the user should be able to compare...

External Links

• org.eclipse.compare.example.xml
• xml diff GUI example