D32 Provers - Revision history

imported>Tommy: /* Overview */

2011-01-27T15:25:18Z

Overview

← Older revision		Revision as of 15:25, 27 January 2011
Line 2:		Line 2:
	Concerning Rodin's provers the following contributions have been made:		Concerning Rodin's provers the following contributions have been made:
	* Jann Röder (ETH Zurich) has developed a relevance filter plug-in. The plug-in provides a proof tactic that first removes hypotheses from a given sequent according to several heuristics. The tactic then inputs the reduced sequent to one or several of Rodin's external provers (PP, newPP, ML). Jann Röder carried out experiments using Event-B models from different domains and observed that his tactic significantly increases the number of proof obligations proved automatically.		* Jann Röder (ETH Zurich) has developed a relevance filter plug-in. The plug-in provides a proof tactic that first removes hypotheses from a given sequent according to several heuristics. The tactic then inputs the reduced sequent to one or several of Rodin's external provers (PP, newPP, ML). Jann Röder carried out experiments using Event-B models from different domains and observed that his tactic significantly increases the number of proof obligations proved automatically.
	* Matthias Schmalz (ETH Zurich) formally expressed the theoretical foundations of Event-B's logic. "Event-B's logic" stands for the formalism in which, e.g., guards, invariants, axioms, and theorems are expressed, and proof obligations are expressed and proved. He provides a rigorous specification of syntax, semantics, proofs, theories, and mathematical extensions <ref name="mathext">http://wiki.event-b.org/index.php/D32_Mathematical_Extensions</ref> in one document. The document encompasses a small theory "Core", proves "Core"'s soundness, and shows how to define the remaining operators, types, and binders available in Rodin using mathematical extensions. The document thus provides a proof calculus for Event-B that is sound by construction, and a methodology for reasoning about the soundness of Event-B proof rules within Event-B. The document also allows users to look-up definitions of predefined operators and binders, answering questions like "what is the meaning of <math>x \div y</math> if <math>x</math> or <math>y</math> is negative". For developers, it sheds some light on intricate questions concerning partial functions, e.g., why it is sound to rewrite <math>x \in \{y \mid \varphi(y)\}</math> to <math>\varphi(x)</math> but unsound (in general) to rewrite <math>\varphi(x)</math> to <math>x \in \{y \mid \varphi(y)\}</math>.		* Matthias Schmalz (ETH Zurich) formally expressed the theoretical foundations of Event-B's logic. "Event-B's logic" stands for the formalism in which, e.g., guards, invariants, axioms, and theorems are expressed, and proof obligations are expressed and proved. He provides a rigorous specification of syntax, semantics, proofs, theories, and mathematical extensions <ref name="mathext">http://wiki.event-b.org/index.php/D32_Mathematical_Extensions</ref> in one document. The document encompasses a small theory "Core", proves "Core"'s soundness, and shows how to define the remaining operators, types, and binders available in Rodin using mathematical extensions. The document thus provides a proof calculus for Event-B that is sound by construction, and a methodology for reasoning about the soundness of Event-B proof rules within Event-B. The document also allows users to look-up definitions of predefined operators and binders, answering questions like "what is the meaning of <math>x \div y</math> if <math>x</math> or  <math>y</math>  is negative". For developers, it sheds some light on intricate questions concerning partial functions, e.g., why it is sound to rewrite <math>x \in \{y \mid \varphi(y)\}</math> to  <math>\varphi(x)</math> but unsound (in general) to rewrite  <math>\varphi(x)</math> to <math>x \in \{y \mid \varphi(y)\}</math>.
	* Systerel improved the support for well-definedness in the sequent prover. The new implementation generates much smaller well-definedness predicates and new automated tactics have been added to discharge most of the well-definedness subgoals, thus rendering well-definedness almost transparent to the end-user.		* Systerel improved the support for well-definedness in the sequent prover. The new implementation generates much smaller well-definedness predicates and new automated tactics have been added to discharge most of the well-definedness subgoals, thus rendering well-definedness almost transparent to the end-user.

imported>Tommy at 15:23, 27 January 2011

2011-01-27T15:23:11Z

← Older revision		Revision as of 15:23, 27 January 2011
Line 2:		Line 2:
	Concerning Rodin's provers the following contributions have been made:		Concerning Rodin's provers the following contributions have been made:
	* Jann Röder (ETH Zurich) has developed a relevance filter plug-in. The plug-in provides a proof tactic that first removes hypotheses from a given sequent according to several heuristics. The tactic then inputs the reduced sequent to one or several of Rodin's external provers (PP, newPP, ML). Jann Röder carried out experiments using Event-B models from different domains and observed that his tactic significantly increases the number of proof obligations proved automatically.		* Jann Röder (ETH Zurich) has developed a relevance filter plug-in. The plug-in provides a proof tactic that first removes hypotheses from a given sequent according to several heuristics. The tactic then inputs the reduced sequent to one or several of Rodin's external provers (PP, newPP, ML). Jann Röder carried out experiments using Event-B models from different domains and observed that his tactic significantly increases the number of proof obligations proved automatically.
	* Matthias Schmalz (ETH Zurich) formally expressed the theoretical foundations of Event-B's logic. "Event-B's logic" stands for the formalism in which, e.g., guards, invariants, axioms, and theorems are expressed, and proof obligations are expressed and proved. He provides a rigorous specification of syntax, semantics, proofs, theories, and ~~[[D32 Mathematical Extensions\|~~mathematical extensions]] in one document. The document encompasses a small theory "Core", proves "Core"'s soundness, and shows how to define the remaining operators, types, and binders available in Rodin using mathematical extensions. The document thus provides a proof calculus for Event-B that is sound by construction, and a methodology for reasoning about the soundness of Event-B proof rules within Event-B. The document also allows users to look-up definitions of predefined operators and binders, answering questions like "what is the meaning of <math>x \div y</math> if <math>x</math> or <math>y</math> is negative". For developers, it sheds some light on intricate questions concerning partial functions, e.g., why it is sound to rewrite <math>x \in \{y \mid \varphi(y)\}</math> to <math>\varphi(x)</math> but unsound (in general) to rewrite <math>\varphi(x)</math> to <math>x \in \{y \mid \varphi(y)\}</math>.		* Matthias Schmalz (ETH Zurich) formally expressed the theoretical foundations of Event-B's logic. "Event-B's logic" stands for the formalism in which, e.g., guards, invariants, axioms, and theorems are expressed, and proof obligations are expressed and proved. He provides a rigorous specification of syntax, semantics, proofs, theories, and mathematical extensions <ref name="mathext">http://wiki.event-b.org/index.php/D32_Mathematical_Extensions</ref> in one document. The document encompasses a small theory "Core", proves "Core"'s soundness, and shows how to define the remaining operators, types, and binders available in Rodin using mathematical extensions. The document thus provides a proof calculus for Event-B that is sound by construction, and a methodology for reasoning about the soundness of Event-B proof rules within Event-B. The document also allows users to look-up definitions of predefined operators and binders, answering questions like "what is the meaning of <math>x \div y</math> if <math>x</math> or <math>y</math> is negative". For developers, it sheds some light on intricate questions concerning partial functions, e.g., why it is sound to rewrite <math>x \in \{y \mid \varphi(y)\}</math> to <math>\varphi(x)</math> but unsound (in general) to rewrite <math>\varphi(x)</math> to <math>x \in \{y \mid \varphi(y)\}</math>.
	* Systerel improved the support for well-definedness in the sequent prover. The new implementation generates much smaller well-definedness predicates and new automated tactics have been added to discharge most of the well-definedness subgoals, thus rendering well-definedness almost transparent to the end-user.		* Systerel improved the support for well-definedness in the sequent prover. The new implementation generates much smaller well-definedness predicates and new automated tactics have been added to discharge most of the well-definedness subgoals, thus rendering well-definedness almost transparent to the end-user.

Line 23:		Line 23:
	Therefore we have devised a rigorous specification document for the logic of Event-B <ref name="eblogic">[ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/698.pdf M. Schmalz. The logic of Event-B. Technical Report 698, ETH Zurich, Switzerland, 2010.]</ref>.		Therefore we have devised a rigorous specification document for the logic of Event-B <ref name="eblogic">[ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/698.pdf M. Schmalz. The logic of Event-B. Technical Report 698, ETH Zurich, Switzerland, 2010.]</ref>.

	~~[[D32 Mathematical Extensions\|~~Mathematical extensions]] play an important role in avoiding unsoundness, because they allow the user to define new operators, binders, types, and inference and rewrite rules in a soundness preserving fashion.		Mathematical extensions<ref name="mathext">http://wiki.event-b.org/index.php/D32 Mathematical_Extensions</ref> play an important role in avoiding unsoundness, because they allow the user to define new operators, binders, types, and inference and rewrite rules in a soundness preserving fashion.
	The specification document <ref name="eblogic"/> also devises the theoretical foundations of mathematical extensions.		The specification document <ref name="eblogic"/> also devises the theoretical foundations of mathematical extensions.
	Note that mathematical extensions are well-understood for, e.g., HOL<ref>M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge University Press, 1993.</ref>, but the extension methods for HOL cannot be straightforwardly adopted for Event-B because of Event-B's [[Well-~~definedness in Event~~-B~~\|well-definedness]]~~ mechanism and non-standard term rewriting.		Note that mathematical extensions are well-understood for, e.g., HOL<ref>M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge University Press, 1993.</ref>, but the extension methods for HOL cannot be straightforwardly adopted for Event-B because of Event-B's well-definedness <ref name="WD">http://wiki.event-b.org/index.php/Well-definedness_in_Event-B</ref> mechanism and non-standard term rewriting.

	== Improved WD Support ==		== Improved WD Support ==
Line 86:		Line 86:
	* The internals of the relevance filter plug-in and the process of fine tuning are documented in J. Röder's Master thesis.<ref name="jannThesis"/>		* The internals of the relevance filter plug-in and the process of fine tuning are documented in J. Röder's Master thesis.<ref name="jannThesis"/>
	* A rigorous specification of Event-B's logic (for Rodin developers) and a reference document containing the definitions of built-in symbols (for Rodin developers and users) can be found in "The logic of Event-B" report.<ref name="eblogic"/>		* A rigorous specification of Event-B's logic (for Rodin developers) and a reference document containing the definitions of built-in symbols (for Rodin developers and users) can be found in "The logic of Event-B" report.<ref name="eblogic"/>
	* The specification of the [[Improved_WD_Lemma_Generation]] is available from the Rodin Wiki.		* The specification of the Improved WD Lemma Generation <ref name=wdgen">http://wiki.event-b.org/index.php/Improved_WD_Lemma_Generation</ref> is available from the Rodin Wiki.

	= Planning =		= Planning =

imported>Tommy: /* Overview */

2011-01-24T13:45:08Z

Overview

← Older revision		Revision as of 13:45, 24 January 2011
Line 2:		Line 2:
	Concerning Rodin's provers the following contributions have been made:		Concerning Rodin's provers the following contributions have been made:
	* Jann Röder (ETH Zurich) has developed a relevance filter plug-in. The plug-in provides a proof tactic that first removes hypotheses from a given sequent according to several heuristics. The tactic then inputs the reduced sequent to one or several of Rodin's external provers (PP, newPP, ML). Jann Röder carried out experiments using Event-B models from different domains and observed that his tactic significantly increases the number of proof obligations proved automatically.		* Jann Röder (ETH Zurich) has developed a relevance filter plug-in. The plug-in provides a proof tactic that first removes hypotheses from a given sequent according to several heuristics. The tactic then inputs the reduced sequent to one or several of Rodin's external provers (PP, newPP, ML). Jann Röder carried out experiments using Event-B models from different domains and observed that his tactic significantly increases the number of proof obligations proved automatically.
	* Matthias Schmalz (ETH Zurich) ~~has worked out~~ the theoretical foundations of Event-B's logic. "Event-B's logic" stands for the formalism in which, e.g., guards, invariants, axioms, and theorems are expressed, and proof obligations are expressed and proved. He provides a rigorous specification of syntax, semantics, proofs, theories, and [[D32 Mathematical Extensions\|mathematical extensions]] in one document. The document encompasses a small theory "Core", proves "Core"'s soundness, and shows how to define the remaining operators, types, and binders available in Rodin using mathematical extensions. The document thus provides a proof calculus for Event-B that is sound by construction, and a methodology for reasoning about the soundness of Event-B proof rules within Event-B. The document also allows users to look-up definitions of predefined operators and binders, answering questions like "what is the meaning of <math>x \div y</math> if <math>x</math> or <math>y</math> is negative". For developers, it sheds some light on intricate questions concerning partial functions, e.g., why it is sound to rewrite <math>x \in \{y \mid \varphi(y)\}</math> to <math>\varphi(x)</math> but unsound (in general) to rewrite <math>\varphi(x)</math> to <math>x \in \{y \mid \varphi(y)\}</math>.		* Matthias Schmalz (ETH Zurich) formally expressed the theoretical foundations of Event-B's logic. "Event-B's logic" stands for the formalism in which, e.g., guards, invariants, axioms, and theorems are expressed, and proof obligations are expressed and proved. He provides a rigorous specification of syntax, semantics, proofs, theories, and [[D32 Mathematical Extensions\|mathematical extensions]] in one document. The document encompasses a small theory "Core", proves "Core"'s soundness, and shows how to define the remaining operators, types, and binders available in Rodin using mathematical extensions. The document thus provides a proof calculus for Event-B that is sound by construction, and a methodology for reasoning about the soundness of Event-B proof rules within Event-B. The document also allows users to look-up definitions of predefined operators and binders, answering questions like "what is the meaning of <math>x \div y</math> if <math>x</math> or <math>y</math> is negative". For developers, it sheds some light on intricate questions concerning partial functions, e.g., why it is sound to rewrite <math>x \in \{y \mid \varphi(y)\}</math> to <math>\varphi(x)</math> but unsound (in general) to rewrite <math>\varphi(x)</math> to <math>x \in \{y \mid \varphi(y)\}</math>.
	* Systerel improved the support for well-definedness in the sequent prover. The new implementation generates much smaller well-definedness predicates and new automated tactics have been added to discharge most of the well-definedness subgoals, thus rendering well-definedness almost transparent to the end-user.		* Systerel improved the support for well-definedness in the sequent prover. The new implementation generates much smaller well-definedness predicates and new automated tactics have been added to discharge most of the well-definedness subgoals, thus rendering well-definedness almost transparent to the end-user.

imported>Wohuai at 08:18, 14 January 2011

2011-01-14T08:18:28Z

← Older revision		Revision as of 08:18, 14 January 2011
Line 13:		Line 13:
	Several heuristics for selecting relevant hypotheses have been proposed in the literature<ref>[http://www.cs.manchester.ac.uk/~hoderk/sine K. Hoder. SUMO infernce engine.]</ref><ref>J. Meng and L. C. Paulson. Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic, 7(1);41-57, 2009.</ref><ref>A. Roederer, Y. Puzis, and G. Sutcliffe. Divvy: an atp meta-system based on axiom relevance ordering. In CADE, pages 157-162, 2009.</ref><ref>G. Sutcliffe and Y. Puzis. SRASS - a semantic relevance axiom selection system. In CADE, pages 295-310, 2007.</ref>.		Several heuristics for selecting relevant hypotheses have been proposed in the literature<ref>[http://www.cs.manchester.ac.uk/~hoderk/sine K. Hoder. SUMO infernce engine.]</ref><ref>J. Meng and L. C. Paulson. Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic, 7(1);41-57, 2009.</ref><ref>A. Roederer, Y. Puzis, and G. Sutcliffe. Divvy: an atp meta-system based on axiom relevance ordering. In CADE, pages 157-162, 2009.</ref><ref>G. Sutcliffe and Y. Puzis. SRASS - a semantic relevance axiom selection system. In CADE, pages 295-310, 2007.</ref>.
	The relevance filter plug-in implements these and other heuristics, and provides a default configuration that has been shown to be almost optimal on a given collection of models		The relevance filter plug-in implements these and other heuristics, and provides a default configuration that has been shown to be almost optimal on a given collection of models
	from different domains<ref name="jannThesis">[http://n.ethz.ch/~~~roederja~~/~~download/thesis.pdf~~ J. Röder. Relevance filters for Event-B. Master Thesis, ETH Zurich, 2010.]</ref>. The relevance filter plug-in has also significantly increased the number of automatically discharged proof obligations on models of deployment partners, which had not been used for fine tuning the heuristics.		from different domains<ref name="jannThesis">[http://e-collection.ethbib.ethz.ch/view/eth:2278?q=event-b J. Röder. Relevance filters for Event-B. Master Thesis, ETH Zurich, 2010.]</ref>. The relevance filter plug-in has also significantly increased the number of automatically discharged proof obligations on models of deployment partners, which had not been used for fine tuning the heuristics.

	== Foundations of Event-B's Logic ==		== Foundations of Event-B's Logic ==

imported>Tommy: /* Available Documentation */

2010-12-21T13:18:22Z

Available Documentation

← Older revision		Revision as of 13:18, 21 December 2010
Line 85:		Line 85:

	* The internals of the relevance filter plug-in and the process of fine tuning are documented in J. Röder's Master thesis.<ref name="jannThesis"/>		* The internals of the relevance filter plug-in and the process of fine tuning are documented in J. Röder's Master thesis.<ref name="jannThesis"/>
	* A rigorous specification of Event-B's logic (for Rodin developers) and a reference document containing the definitions of built-in symbols (for Rodin developers and users) can be found in "The logic of Event-B" report.<ref name="eblogic"/>.		* A rigorous specification of Event-B's logic (for Rodin developers) and a reference document containing the definitions of built-in symbols (for Rodin developers and users) can be found in "The logic of Event-B" report.<ref name="eblogic"/>
	* The specification of the [[Improved_WD_Lemma_Generation]] is available from the Rodin Wiki.		* The specification of the [[Improved_WD_Lemma_Generation]] is available from the Rodin Wiki.

imported>Tommy: /* Available Documentation */

2010-12-21T13:18:08Z

Available Documentation

← Older revision		Revision as of 13:18, 21 December 2010
Line 85:		Line 85:

	* The internals of the relevance filter plug-in and the process of fine tuning are documented in J. Röder's Master thesis.<ref name="jannThesis"/>		* The internals of the relevance filter plug-in and the process of fine tuning are documented in J. Röder's Master thesis.<ref name="jannThesis"/>
	* A rigorous specification of Event-B's logic (for Rodin developers) and a reference document containing the definitions of built-in symbols (for Rodin developers and users) can be found in <ref name="eblogic"/>.		* A rigorous specification of Event-B's logic (for Rodin developers) and a reference document containing the definitions of built-in symbols (for Rodin developers and users) can be found in "The logic of Event-B" report.<ref name="eblogic"/>.
	* The specification of the [[Improved_WD_Lemma_Generation]] is available from the Rodin Wiki.		* The specification of the [[Improved_WD_Lemma_Generation]] is available from the Rodin Wiki.

imported>Tommy: /* Available Documentation */

2010-12-21T13:17:04Z

Available Documentation

← Older revision		Revision as of 13:17, 21 December 2010
Line 84:		Line 84:
	= Available Documentation =		= Available Documentation =

	* The internals of the relevance filter plug-in and the process of fine tuning are documented in <ref name="jannThesis"/>.		* The internals of the relevance filter plug-in and the process of fine tuning are documented in J. Röder's Master thesis.<ref name="jannThesis"/>
	* A rigorous specification of Event-B's logic (for Rodin developers) and a reference document containing the definitions of built-in symbols (for Rodin developers and users) can be found in <ref name="eblogic"/>.		* A rigorous specification of Event-B's logic (for Rodin developers) and a reference document containing the definitions of built-in symbols (for Rodin developers and users) can be found in <ref name="eblogic"/>.
	* The specification of the [[Improved_WD_Lemma_Generation]] is available from the Rodin Wiki.		* The specification of the [[Improved_WD_Lemma_Generation]] is available from the Rodin Wiki.

imported>Tommy: /* Choices / Decisions */

2010-12-21T13:14:42Z

Choices / Decisions

← Older revision		Revision as of 13:14, 21 December 2010
Line 45:		Line 45:
	= Choices / Decisions =		= Choices / Decisions =

	~~'''~~ Relevance Filtering ~~'''~~		== Relevance Filtering ==
	The relevance filter heuristics we have considered do not work out of the box - their parameters need to be carefully adjusted.		The relevance filter heuristics we have considered do not work out of the box - their parameters need to be carefully adjusted.
	The major design decision concerned how to carry out the process of fine tuning.		The major design decision concerned how to carry out the process of fine tuning.
Line 57:		Line 57:
	We observed that the final filter configuration significantly increases the number of automatically discharged proof obligations among the validation benchmark in comparison to not using relevance filtering.		We observed that the final filter configuration significantly increases the number of automatically discharged proof obligations among the validation benchmark in comparison to not using relevance filtering.

	~~'''~~ Foundations of Event-B's Logic ~~'''~~		== Foundations of Event-B's Logic ==
	The major design decision concerned the logic in which the semantics of Event-B's logic is formalized.		The major design decision concerned the logic in which the semantics of Event-B's logic is formalized.
	We experimented with ZF set theory and HOL. Finally, we decided to define semantics in terms of a (shallow) embedding into HOL, because that allows us to carry out vast parts of our soundness proofs using Isabelle/HOL<ref>T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - a proof assistant for higher-order logic. LNCS 2283, 2002.</ref>. In the long term, the embedding allows us		We experimented with ZF set theory and HOL. Finally, we decided to define semantics in terms of a (shallow) embedding into HOL, because that allows us to carry out vast parts of our soundness proofs using Isabelle/HOL<ref>T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - a proof assistant for higher-order logic. LNCS 2283, 2002.</ref>. In the long term, the embedding allows us
Line 64:		Line 64:
	Other design decisions, e.g., concerning terminology, are discussed in <ref name="eblogic"/>.		Other design decisions, e.g., concerning terminology, are discussed in <ref name="eblogic"/>.

	~~'''~~ Improved WD Support ~~'''~~		== Improved WD Support ==

	To improve generated WD lemmas, the generating algorithm has not been changed		To improve generated WD lemmas, the generating algorithm has not been changed

imported>Tommy: /* Motivations */

2010-12-21T13:13:59Z

Motivations

← Older revision		Revision as of 13:13, 21 December 2010
Line 7:		Line 7:
	= Motivations =		= Motivations =

	~~'''~~Relevance Filtering~~'''~~		== Relevance Filtering ==

	Rodin's external provers (PP, newPP, and sometimes also ML) tend to perform poorly in the presence of irrelevant hypotheses.		Rodin's external provers (PP, newPP, and sometimes also ML) tend to perform poorly in the presence of irrelevant hypotheses.
Line 15:		Line 15:
	from different domains<ref name="jannThesis">[http://n.ethz.ch/~roederja/download/thesis.pdf J. Röder. Relevance filters for Event-B. Master Thesis, ETH Zurich, 2010.]</ref>. The relevance filter plug-in has also significantly increased the number of automatically discharged proof obligations on models of deployment partners, which had not been used for fine tuning the heuristics.		from different domains<ref name="jannThesis">[http://n.ethz.ch/~roederja/download/thesis.pdf J. Röder. Relevance filters for Event-B. Master Thesis, ETH Zurich, 2010.]</ref>. The relevance filter plug-in has also significantly increased the number of automatically discharged proof obligations on models of deployment partners, which had not been used for fine tuning the heuristics.

	~~'''~~Foundations of Event-B's Logic~~'''~~		== Foundations of Event-B's Logic ==

	As Rodin is used to develop safety critical systems, bugs in Rodin's theorem prover constitute a serious problem.		As Rodin is used to develop safety critical systems, bugs in Rodin's theorem prover constitute a serious problem.
Line 27:		Line 27:
	Note that mathematical extensions are well-understood for, e.g., HOL<ref>M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge University Press, 1993.</ref>, but the extension methods for HOL cannot be straightforwardly adopted for Event-B because of Event-B's [[Well-definedness in Event-B\|well-definedness]] mechanism and non-standard term rewriting.		Note that mathematical extensions are well-understood for, e.g., HOL<ref>M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge University Press, 1993.</ref>, but the extension methods for HOL cannot be straightforwardly adopted for Event-B because of Event-B's [[Well-definedness in Event-B\|well-definedness]] mechanism and non-standard term rewriting.

	~~'''~~Improved WD Support~~'''~~		== Improved WD Support ==

	When the user enters an expression or predicate that is possibly ill-defined		When the user enters an expression or predicate that is possibly ill-defined

imported>Tommy: /* References */

2010-12-21T11:06:27Z

References

← Older revision		Revision as of 11:06, 21 December 2010
Line 96:		Line 96:
	a link-up between Rodin and Isabelle/HOL makes these solvers also available to Rodin.		a link-up between Rodin and Isabelle/HOL makes these solvers also available to Rodin.

	=== References ===		== References ==
	<references/>		<references/>

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]