Scenarios for Merging Proofs: Difference between revisions
imported>Mathieu m Add a table describing the envisionned cases |
imported>Ladenberger |
||
| (17 intermediate revisions by 2 users not shown) | |||
| Line 3: | Line 3: | ||
With respect to the merging objective, a proof is made of: | With respect to the merging objective, a proof is made of: | ||
# a component name, | # a component name, | ||
# a unique identifier inside that component, which is same as the [ | # a unique identifier inside that component, which is same as the [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/generated_proof_obligations.html PO] identifier, | ||
# a proof tree, either manual or automatic, | # a proof tree, either manual or automatic, | ||
# a proof status (PO discharged or not by the proof tree) | # a proof status (PO discharged or not by the proof tree, in fact implemented with a ''confidence'' value: 1000 => proved, 500 => review, <500 => unproved) | ||
# a PO [ | # a PO [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/sequents.html sequent] | ||
== Rodin database implementation == | == Rodin database implementation == | ||
| Line 13: | Line 13: | ||
* a {{file|compname.bps}} file, which contains the proof status associated with each PO (2/, 5/ and 3/ - discharged or not, manual or automatic) | * a {{file|compname.bps}} file, which contains the proof status associated with each PO (2/, 5/ and 3/ - discharged or not, manual or automatic) | ||
* a {{file|compname.bpo}} file, which contains the PO (1/ and 2/ + PO content). | * a {{file|compname.bpo}} file, which contains the PO (1/ and 2/ + PO content). | ||
== Proof reuse == | |||
Rodin is able, actually with a bit of work, to provide a ''reuse'' mechanism. This mechanism would allow to check, without replaying, that a proof tree will cleanly discharge a PO. | |||
Having this mechanism at hand is very useful, as it allows the person doing the merge to take its decision without knowing the content of the old {{file|.bps}} and {{file|.bpo}} files. Only the {{file|.bpr}} files and the {{file|.bpo}} obtained after having merged the model are used. | |||
== Merging scenarios == | == Merging scenarios == | ||
PO being uniquely identified, it may be enough to consider a merge taking place PO by PO. | 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 | 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 standing for ancestor). We also consider ''L'' and ''O'' as being symmetrical (and thus we won't describe symmetrical 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 {{file|compname.bpr}} file contains not only the current proof (called ''main proof''), but also all the proof trees that were once used to prove the PO (the set of those proof trees is called ''proof history''). | |||
Once both ''multi-proof database'' and ''proof reuse'' are implemented, the merge process for the proofs may be the following one: | |||
# [[Requirements for merging models|merge the model]] (machines and context) | |||
# build new ''proof history'' as the union of ''proof histories'' from ''O'' and ''L' plus, say ''L'' ''main proof'' | |||
# build the ''main proof'' with the ''O main proof'' | |||
Those steps do not need user interacions. | |||
The person doing the merge may then review the proofs that do not replay, and see if one of the history proof tree may help (steps which may also be automated with the help of ''proof reuse'' feature). | |||
=== Complicated scenarios === | |||
{{Hidden begin|title=Complicated scenarios}} | |||
''Those scenarios are kept for reference only'' | |||
The table hereafter described the envisioned use cases. | |||
{{SimpleHeader}} | {{SimpleHeader}} | ||
!n° !! A st !! L st |!!O st !! A ma !! L ma !! O ma !! PO L !! PO O !! PR L !! PR O !! Actions | !n° !! A st !! L st |!!O st !! A ma !! L ma !! O ma !! PO L !! PO O !! PR L !! PR O !! Actions | ||
| Line 65: | Line 86: | ||
:'''PO X''': po changes for X compare to others user/branch | :'''PO X''': po changes for X compare to others user/branch | ||
:'''PR X''': proof change for X, compared to others user/branch | :'''PR X''': proof change for X, compared to others user/branch | ||
A prototype that implement a simpler policy (get ''other'' except if local has a successful manual proof) is being developed at http://bitbucket.org/matclab/proofmerge/. | |||
{{Hidden end}} | |||
== User interactions == | |||
In the context of [[#Simple scenarios (need database evolution)|simple scenarios]], no user interactions is requested from user. | |||
The only interaction envisioned is done after the merge, and is related to digging into [[proof history]] | |||
== VCS interactions == | |||
With respect to the action of merging the proof, the only interaction with VCS, is the ability to retrieve ''local'', ''other'' and ''ancestors'' {{file|.bpr}} files. | |||
It is a very common requirement, which is certainly fulfilled by every descent VCS. | |||
[[Category:Design proposal]] | [[Category:Design proposal]] | ||
Latest revision as of 10:34, 27 October 2011
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:
- a component name,
- a unique identifier inside that component, which is same as the PO identifier,
- a proof tree, either manual or automatic,
- a proof status (PO discharged or not by the proof tree, in fact implemented with a confidence value: 1000 => proved, 500 => review, <500 => unproved)
- a PO sequent
Rodin database implementation
Each component
is associated with:
- a compname.bprfile, which contains the proof trees associated with each PO (1/, 2/ and 3/ before).
- a compname.bpsfile, which contains the proof status associated with each PO (2/, 5/ and 3/ - discharged or not, manual or automatic)
- a compname.bpofile, which contains the PO (1/ and 2/ + PO content).
Proof reuse
Rodin is able, actually with a bit of work, to provide a reuse mechanism. This mechanism would allow to check, without replaying, that a proof tree will cleanly discharge a PO.
Having this mechanism at hand is very useful, as it allows the person doing the merge to take its decision without knowing the content of the old
and
files. Only the
files and the
obtained after having merged the model are used.
Merging scenarios
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 standing for ancestor). We also consider L and O as being symmetrical (and thus we won't describe symmetrical 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
file contains not only the current proof (called main proof), but also all the proof trees that were once used to prove the PO (the set of those proof trees is called proof history).
Once both multi-proof database and proof reuse are implemented, the merge process for the proofs may be the following one:
- merge the model (machines and context)
- build new proof history as the union of proof histories from O and L' plus, say L main proof
- build the main proof with the O main proof
Those steps do not need user interacions.
The person doing the merge may then review the proofs that do not replay, and see if one of the history proof tree may help (steps which may also be automated with the help of proof reuse feature).
Complicated scenarios
User interactions
In the context of simple scenarios, no user interactions is requested from user.
The only interaction envisioned is done after the merge, and is related to digging into proof history
VCS interactions
With respect to the action of merging the proof, the only interaction with VCS, is the ability to retrieve local, other and ancestors
files.
It is a very common requirement, which is certainly fulfilled by every descent VCS.
