Improved WD Lemma Generation - Revision history

imported>Tommy: /* Improved Generation */

2012-06-19T09:43:19Z

Improved Generation

← Older revision		Revision as of 09:43, 19 June 2012
Line 45:		Line 45:
	To fix the issues shown in the above examples, we need that the tool produces a WD lemma equivalent (in the logical sense) to the predicate obtained through the <math>\mathcal{L}</math> operator and satisfying the following constraint : No sub-predicate subsumes another sub-predicate (exception : example C).		To fix the issues shown in the above examples, we need that the tool produces a WD lemma equivalent (in the logical sense) to the predicate obtained through the <math>\mathcal{L}</math> operator and satisfying the following constraint : No sub-predicate subsumes another sub-predicate (exception : example C).

	The constraint covers ~~both~~ examples A, B and D.		The constraint covers examples A, B and D.

	== Design for Improved Generation ==		== Design for Improved Generation ==

imported>Tommy: Fixed the link about WD

2012-06-01T09:03:45Z

Fixed the link about WD

← Older revision		Revision as of 09:03, 1 June 2012
Line 3:		Line 3:
	This page describes work done for optimising well-definedness lemmas generated by the Core Rodin platform.		This page describes work done for optimising well-definedness lemmas generated by the Core Rodin platform.

	The lemmas are generated according to the <math>\mathcal{L}</math> operator defined in [http://handbook.event-b.org/current/html/~~well_definedness~~.html Well-definedness in Event-B]. However, this operator being defined as a syntactic transformation, it sometimes generates lemmas that are unnecessarily complicated. We first give some motivating examples showing cases where this happens, then we describe what result shall be produced by the tool. Finally, we describe the design retained for development.		The lemmas are generated according to the <math>\mathcal{L}</math> operator defined in [http://handbook.event-b.org/current/html/mathematical_notation_introduction.html#well_definedness Well-definedness in Event-B]. However, this operator being defined as a syntactic transformation, it sometimes generates lemmas that are unnecessarily complicated. We first give some motivating examples showing cases where this happens, then we describe what result shall be produced by the tool. Finally, we describe the design retained for development.

	== Motivating Examples ==		== Motivating Examples ==

imported>Laurent: Work done

2012-06-01T08:36:33Z

Work done

← Older revision		Revision as of 08:36, 1 June 2012
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}

	This page describes work ~~in progress~~ for optimising well-definedness lemmas generated by the Core Rodin platform.		This page describes work done for optimising well-definedness lemmas generated by the Core Rodin platform.

	The lemmas are generated according to the <math>\mathcal{L}</math> operator defined in [http://handbook.event-b.org/current/html/well_definedness.html Well-definedness in Event-B]. However, this operator being defined as a syntactic transformation, it sometimes generates lemmas that are unnecessarily complicated. We first give some motivating examples showing cases where this happens, then we describe what result shall be produced by the tool. Finally, we describe the design retained for development.		The lemmas are generated according to the <math>\mathcal{L}</math> operator defined in [http://handbook.event-b.org/current/html/well_definedness.html Well-definedness in Event-B]. However, this operator being defined as a syntactic transformation, it sometimes generates lemmas that are unnecessarily complicated. We first give some motivating examples showing cases where this happens, then we describe what result shall be produced by the tool. Finally, we describe the design retained for development.
Line 54:		Line 54:
	All the classes created for Well-Definedness generation can be found in the package "''org.eventb.internal.core.ast.wd''".		All the classes created for Well-Definedness generation can be found in the package "''org.eventb.internal.core.ast.wd''".

	[[Category:Developer documentation]][[Category:Proof~~]][[Category:Work in progress~~]]		[[Category:Developer documentation]][[Category:Proof]]

imported>Ladenberger at 10:42, 27 October 2011

2011-10-27T10:42:59Z

← Older revision		Revision as of 10:42, 27 October 2011
Line 3:		Line 3:
	This page describes work in progress for optimising well-definedness lemmas generated by the Core Rodin platform.		This page describes work in progress for optimising well-definedness lemmas generated by the Core Rodin platform.

	The lemmas are generated according to the <math>\mathcal{L}</math> operator defined in [[Well-definedness in Event-B]]. However, this operator being defined as a syntactic transformation, it sometimes generates lemmas that are unnecessarily complicated. We first give some motivating examples showing cases where this happens, then we describe what result shall be produced by the tool. Finally, we describe the design retained for development.		The lemmas are generated according to the <math>\mathcal{L}</math> operator defined in [http://handbook.event-b.org/current/html/well_definedness.html Well-definedness in Event-B]. However, this operator being defined as a syntactic transformation, it sometimes generates lemmas that are unnecessarily complicated. We first give some motivating examples showing cases where this happens, then we describe what result shall be produced by the tool. Finally, we describe the design retained for development.

	== Motivating Examples ==		== Motivating Examples ==

imported>Desaperh at 12:38, 15 October 2010

2010-10-15T12:38:44Z

← Older revision		Revision as of 12:38, 15 October 2010
Line 51:		Line 51:
	The old mechanism for Well-Definedness lemma generation has been externalized using Design Pattern Visitor. This mechanism is still used to generate an unsimplified Well-Definedness lemma. To simplify this Well-Definedness lemma, we use the Design Pattern Visitor to create a new tree made up of predicates, implications, conjunctions and universal quantifiers, while traversing the whole AST. This tree will be simplified by removing redundant predicates and using optimizations, and will be used to build a simplified Well-Definedness lemma. This visitor will be applicable to all predicates.		The old mechanism for Well-Definedness lemma generation has been externalized using Design Pattern Visitor. This mechanism is still used to generate an unsimplified Well-Definedness lemma. To simplify this Well-Definedness lemma, we use the Design Pattern Visitor to create a new tree made up of predicates, implications, conjunctions and universal quantifiers, while traversing the whole AST. This tree will be simplified by removing redundant predicates and using optimizations, and will be used to build a simplified Well-Definedness lemma. This visitor will be applicable to all predicates.
	As some Well-Definedness lemmas will be simplified, some WD proofs will be broken.		As some Well-Definedness lemmas will be simplified, some WD proofs will be broken.

			All the classes created for Well-Definedness generation can be found in the package "''org.eventb.internal.core.ast.wd''".

	[[Category:Developer documentation]][[Category:Proof]][[Category:Work in progress]]		[[Category:Developer documentation]][[Category:Proof]][[Category:Work in progress]]

imported>Desaperh: /* Design for Improved Generation */

2010-10-15T12:35:40Z

Design for Improved Generation

← Older revision		Revision as of 12:35, 15 October 2010
Line 49:		Line 49:
	== Design for Improved Generation ==		== Design for Improved Generation ==

	To ~~improve the~~ Well-Definedness lemma, we use the Design Pattern Visitor to create a new tree made up of predicates, implications, conjunctions and universal quantifiers, while traversing the whole AST. This tree will be simplified by removing redundant predicates and using optimizations, and will be used to build a simplified Well-Definedness lemma. This visitor will be applicable to all predicates.		The old mechanism for Well-Definedness lemma generation has been externalized using Design Pattern Visitor. This mechanism is still used to generate an unsimplified Well-Definedness lemma. To simplify this Well-Definedness lemma, we use the Design Pattern Visitor to create a new tree made up of predicates, implications, conjunctions and universal quantifiers, while traversing the whole AST. This tree will be simplified by removing redundant predicates and using optimizations, and will be used to build a simplified Well-Definedness lemma. This visitor will be applicable to all predicates.
	As some Well-Definedness lemmas will be simplified, some WD proofs will be broken.		As some Well-Definedness lemmas will be simplified, some WD proofs will be broken.

	[[Category:Developer documentation]][[Category:Proof]][[Category:Work in progress]]		[[Category:Developer documentation]][[Category:Proof]][[Category:Work in progress]]

imported>Laurent: /* Design for Improved Generation */

2010-10-13T11:31:28Z

Design for Improved Generation

← Older revision		Revision as of 11:31, 13 October 2010
Line 49:		Line 49:
	== Design for Improved Generation ==		== Design for Improved Generation ==

	To improve the Well-Definedness lemma, we use the Design Pattern Visitor to create a new tree made up of predicates, implications, conjunctions and universal quantifiers , while traversing the whole AST. This tree will be simplified by removing redundant predicates and using optimizations, and will be used to build a simplified Well-Definedness lemma. This visitor will be applicable to all predicates.		To improve the Well-Definedness lemma, we use the Design Pattern Visitor to create a new tree made up of predicates, implications, conjunctions and universal quantifiers, while traversing the whole AST. This tree will be simplified by removing redundant predicates and using optimizations, and will be used to build a simplified Well-Definedness lemma. This visitor will be applicable to all predicates.
	As some Well-Definedness lemmas will be simplified, some WD proofs will be broken.		As some Well-Definedness lemmas will be simplified, some WD proofs will be broken.

	[[Category:Developer documentation]][[Category:Proof]][[Category:Work in progress]]		[[Category:Developer documentation]][[Category:Proof]][[Category:Work in progress]]

imported>Laurent: /* Example D */

2010-10-13T11:30:37Z

Example D

← Older revision		Revision as of 11:30, 13 October 2010
Line 39:		Line 39:


	<math> y = 1 \land x \div y = 2 \limp x \div y = 3 </math> will produce the well-definedness lemma <math> (y = 1 \limp \lnot y = 0) \land (y = 1 \land x \div y = 2 \limp \lnot y = 0 ) </math>. In this well-definedness lemma, the sub-predicate <math>y = 1 \land x \div y = 2 \limp \lnot y = 0 </math> is subsumed by the sub-predicate <math> y = 1 \limp \lnot y = 0 </math>. In the first implication, the consequent x \div y = 2 is unnecessary.		<math> y = 1 \land x \div y = 2 \limp x \div y = 3 </math> will produce the well-definedness lemma <math> (y = 1 \limp \lnot y = 0) \land (y = 1 \land x \div y = 2 \limp \lnot y = 0 ) </math>. In this well-definedness lemma, the sub-predicate <math>y = 1 \land x \div y = 2 \limp \lnot y = 0 </math> is subsumed by the sub-predicate <math> y = 1 \limp \lnot y = 0 </math>. In the first implication, the consequent <math>x \div y = 2</math> is unnecessary.

	== Improved Generation ==		== Improved Generation ==

imported>Laurent: /* Example C */

2010-10-13T11:30:01Z

Example C

← Older revision		Revision as of 11:30, 13 October 2010
Line 35:		Line 35:

	This issue will not be fixed by the improved generation.		This issue will not be fixed by the improved generation.


	=== Example D ===		=== Example D ===

imported>Desaperh at 14:23, 20 August 2010

2010-08-20T14:23:20Z

← Older revision		Revision as of 14:23, 20 August 2010
Line 44:		Line 44:
	== Improved Generation ==		== Improved Generation ==

	To fix the issues shown in the above examples, we need that the tool produces a WD lemma equivalent (in the logical sense) to the predicate obtained through the <math>\mathcal{L}</math> operator and satisfying the following ~~constraints~~:		To fix the issues shown in the above examples, we need that the tool produces a WD lemma equivalent (in the logical sense) to the predicate obtained through the <math>\mathcal{L}</math> operator and satisfying the following constraint : No sub-predicate subsumes another sub-predicate (exception : example C).
	# No sub-predicate subsumes another sub-predicate (exception : example C)
	.
	~~{{TODO\|Is there any other constraint to add?}}~~

	~~Constraint 1~~ covers both examples A, B and D.		The constraint covers both examples A, B and D.

	== Design for Improved Generation ==		== Design for Improved Generation ==