How To Evolve Reasoners - Revision history

imported>Ladenberger: /* See Also */

2011-10-27T10:29:57Z

imported>Nicolas: /* Versions and Levels */

2010-11-30T16:44:26Z

Versions and Levels

← Older revision		Revision as of 16:44, 30 November 2010
Line 36:		Line 36:

	A new level is created using a new reasoner, that extends the behaviour of the existing one. In practice, as is done by AutoRewrites and AutoRewritesL1, the various reasoners can use the behaviour of a third class (AutoRewriterImpl in this case), which is itself parameterized by the level. It means that the code for additional matches is conditioned by the actual level (not executed for level 0, executed for level 1 and more).		A new level is created using a new reasoner, that extends the behaviour of the existing one. In practice, as is done by AutoRewrites and AutoRewritesL1, the various reasoners can use the behaviour of a third class (AutoRewriterImpl in this case), which is itself parameterized by the level. It means that the code for additional matches is conditioned by the actual level (not executed for level 0, executed for level 1 and more).

			To summarize:
			* Reasoner versions:
			: when a bug is fixed in a reasoner, its version shall be increased so that all POs that could use the faulty version are checked again with the fixed version at the next build.
			: It is OK to add more functionality to a reasoner, that is process more cases than before (e.g., accept new inputs or new sequents). There is no need to change the reasoner version in this case, as it is fully backward compatible.

			* Reasoner level:
			: when one wants to change the behaviour of a reasoner (for instance, the former behaviour was correct but not optimal), a new level of the reasoner shall be created. Levels are just a matter of convention, in fact each level is a reasoner by itself. However, levels share a large code basis to avoid copy-pasted code. It is very important to retain the original level, so that existing proofs do not get broken.

	== How to decide what to do ==		== How to decide what to do ==

imported>Nicolas: /* Versions and Levels */

2010-11-25T14:32:49Z

Versions and Levels

← Older revision		Revision as of 14:32, 25 November 2010
Line 35:		Line 35:
	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 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.		A new level is created using a new reasoner, that extends the behaviour of the existing one. In practice, as is done by AutoRewrites and AutoRewritesL1, the various reasoners can use the behaviour of a third class (AutoRewriterImpl in this case), which is itself parameterized by the level. It means that the code for additional matches is conditioned by the actual level (not executed for level 0, executed for level 1 and more).

	== How to decide what to do ==		== How to decide what to do ==

imported>Nicolas: /* Versions and Levels */

2010-11-25T11:18:20Z

Versions and Levels

@@ Line 18: / Line 18: @@
 == Versions and Levels ==
-{{TODO}}
+Roughly speaking:
 == How to decide what to do ==

imported>Nicolas: First version, incomplete

2010-11-24T17:24:15Z

First version, incomplete

New page

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 ==

{{TODO}}

== How to decide what to do ==

{{TODO|make a decision tree and describe precisely what to do and how to proceed}}

== See Also ==

* [[Versioned_Reasoners| Versioned Reasoners]]
* [[Reasoners]]

← Older revision		Revision as of 10:29, 27 October 2011
Line 52:		Line 52:

	* [[Versioned_Reasoners\| Versioned Reasoners]]		* [[Versioned_Reasoners\| Versioned Reasoners]]
	* [[Reasoners]]		* [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/reasoners.html Reasoners]