Difference between revisions of "How To Evolve Reasoners"

From Event-B
Jump to navigationJump to search
imported>Nicolas
m (First version, incomplete)
 
imported>Nicolas
Line 18: Line 18:
 
== Versions and Levels ==
 
== Versions and Levels ==
  
{{TODO}}
+
Roughly speaking:
 +
{| class="wikitable"
 +
| levels
 +
| <math>\rel</math>
 +
| backward compatible changes
 +
|-
 +
| versions
 +
| <math>\rel</math>
 +
| non backward compatible changes
 +
|}
 +
 
 +
Backward compatibility here is to be understood as: if the previous implementation can be applied to a sequent, then the new implementation can be applied seamlessly to the same sequent.
 +
 
 +
That is, given the same input, if the previous implementation succeeds and produces an output (a proof rule), then the new implementation also succeeds and produces exactly the same output (in particular the same antecedents, goal and needed hypotheses).
 +
 
 +
A new version is made through the <code>IVersionedReasoner</code> interface, by either starting to implement it (returning version 0) if the previous reasoner was not versioned, or incrementing the version.
 +
 
 +
A new level is created using a new reasoner, that extends the behaviour of the existing one.
  
 
== How to decide what to do ==
 
== How to decide what to do ==

Revision as of 11:18, 25 November 2010

A reasoner implementation is not necessarily frozen code. It may evolve in time, to fix bugs or modify the behaviour, or to match additional proof rules, even after the old implementation was used to prove models. This leads to various issues, from unexpected proving failures to global prover unsoundness.

This is why successive implementations of a reasoner have to be distinguished, so that proofs using older implementations get detected by the tool as broken.

But a reasoner evolution is sometimes conservative and does not require to consider proofs broken if they use the implementation of the reasoner prior to the evolution.

In order to deal with these various cases, notions of version and level have been defined.

This page is dedicated to explaining these notions and describing exactly what to do to keep the prover sound.

What happens if I do nothing ?

The consequences of doing nothing besides functional code changes entails that proofs made using old reasoner implementation will be left unnoticed. Thus, if we clean a project in order to update proof statuses, these proofs will be considered reusable (in the sense of org.eventb.core.seqprover.ProverLib.isProofReusable() ) and their status will be left unchanged, i.e potentially discharged even if the new reasoner implementation would fail where the older succeeded. But if we make a replay on these proofs, the new reasoner implementation will be used and the correct status will be found.

So we get a difference between reusability and replayability, which makes the prover globally unstable and potentially unsound.

Versions and Levels

Roughly speaking:

levels \rel backward compatible changes
versions \rel non backward compatible changes

Backward compatibility here is to be understood as: if the previous implementation can be applied to a sequent, then the new implementation can be applied seamlessly to the same sequent.

That is, given the same input, if the previous implementation succeeds and produces an output (a proof rule), then the new implementation also succeeds and produces exactly the same output (in particular the same antecedents, goal and needed hypotheses).

A new version is made through the IVersionedReasoner interface, by either starting to implement it (returning version 0) if the previous reasoner was not versioned, or incrementing the version.

A new level is created using a new reasoner, that extends the behaviour of the existing one.

How to decide what to do

TODO: make a decision tree and describe precisely what to do and how to proceed

See Also