Difference between revisions of "Proof Dependencies and Reasoner Conflicts"
From Event-B
Jump to navigationJump to searchimported>Nicolas m (New page: Until Rodin 2.1, proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for conflicts in rea...) |
imported>Nicolas m |
||
| Line 1: | Line 1: | ||
Until Rodin 2.1, proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for conflicts in reasoner versions. | Until Rodin 2.1, proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for conflicts in reasoner versions. | ||
Hence the idea of integrating reasoners in proof dependencies and have them processed the same way as other proof dependency components, that are stored in the root element of the proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation. | Hence the idea of integrating reasoners in proof dependencies and have them processed the same way as other proof dependency components, that are stored in the root element of the proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation. | ||
| + | |||
| + | {{TODO|Document proof storage}} | ||
Revision as of 12:46, 1 June 2011
Until Rodin 2.1, proof status is determined from proof dependencies on the one hand and a proof skeleton on the other hand. The skeleton is entirely visited, searching for conflicts in reasoner versions. Hence the idea of integrating reasoners in proof dependencies and have them processed the same way as other proof dependency components, that are stored in the root element of the proofs to allow for quick access. This improves performances in updating proof statuses, which is by far the most time-consuming build operation.
TODO: Document proof storage
