D23 Improvements to Existing Provers - Revision history

imported>Laurent: /* Motivations */

2010-01-27T11:41:42Z

Motivations

← Older revision		Revision as of 11:41, 27 January 2010
Line 27:		Line 27:
	* Reducing proof storage space.		* Reducing proof storage space.
	: Big proof files are difficult to handle, on the one hand by the Rodin platform (slow access), and on the other hand by users (project sharing).		: Big proof files are difficult to handle, on the one hand by the Rodin platform (slow access), and on the other hand by users (project sharing).
	: The [http://wiki.event-b.org/index.php/Proof_Purger_Interface proof purging] and [http://wiki.event-b.org/index.php/Proof_Simplification proof simplifying] mechanisms have been implemented to address this ~~problem~~.		: The [http://wiki.event-b.org/index.php/Proof_Purger_Interface proof purging] and [http://wiki.event-b.org/index.php/Proof_Simplification proof simplifying] mechanisms have been implemented to address this issue.
	* Facilitating manual proof review or reuse.		* Facilitating manual proof review or reuse.
	: The [http://wiki.event-b.org/index.php/Proof_Skeleton_View proof skeleton view] allows to quickly browse through a proof. : Moreover, the provided copy/paste feature makes it possible to reuse a stored proof into a new proof.		: The [http://wiki.event-b.org/index.php/Proof_Skeleton_View proof skeleton view] allows to quickly browse through a proof. : Moreover, the provided copy/paste feature makes it possible to reuse a stored proof into a new proof.

imported>Laurent: /* Motivations */

2010-01-27T11:38:37Z

Motivations

← Older revision		Revision as of 11:38, 27 January 2010
Line 22:		Line 22:
	The motivations for improvements to existing provers can be summarized as follows:		The motivations for improvements to existing provers can be summarized as follows:
	* Reducing proving time and effort.		* Reducing proving time and effort.
	: New proof rules, both manual and automatic (e.g.., [http://www.cs.cmu.edu/afs/cs/academic/class/15671-f95/www/handouts/proof/node1.html One point rule], arithmetic rules), have been added to discharge more ~~proofs~~ easily.		: New proof rules, both manual and automatic (e.g.., [http://www.cs.cmu.edu/afs/cs/academic/class/15671-f95/www/handouts/proof/node1.html One point rule], arithmetic rules), have been added to discharge more proof obligations more easily.
	* Reflecting corrections in prover implementations.		* Reflecting corrections in prover implementations.
	: The [http://wiki.event-b.org/index.php/Versioned_Reasoners reasoners] are versioned. A reasoner implementation may indeed evolve in time (bug fixes, modifications of the behaviour, etc), even after the old implementation has been used to prove a model. This may lead to potential issues when trying to reuse or replay proofs serialized by the old reasoner implementation. Such problems are solved through the reasoner versioning mechanism.		: The [http://wiki.event-b.org/index.php/Versioned_Reasoners reasoners] are versioned. A reasoner implementation may indeed evolve in time (bug fixes, modifications of the behaviour, etc), even after the old implementation has been used to prove a model. This may lead to potential issues when trying to reuse or replay proofs serialized by the old reasoner implementation. Such problems are solved through the reasoner versioning mechanism.

imported>Laurent: /* Motivations */

2010-01-27T11:38:03Z

Motivations

← Older revision		Revision as of 11:38, 27 January 2010
Line 22:		Line 22:
	The motivations for improvements to existing provers can be summarized as follows:		The motivations for improvements to existing provers can be summarized as follows:
	* Reducing proving time and effort.		* Reducing proving time and effort.
	: New proof rules, manual and automatic (eg., [http://www.cs.cmu.edu/afs/cs/academic/class/15671-f95/www/handouts/proof/node1.html One point rule], arithmetic rules~~, etc~~), have been added to discharge more proofs easily.		: New proof rules, both manual and automatic (e.g.., [http://www.cs.cmu.edu/afs/cs/academic/class/15671-f95/www/handouts/proof/node1.html One point rule], arithmetic rules), have been added to discharge more proofs easily.
	* Reflecting corrections in prover implementations.		* Reflecting corrections in prover implementations.
	: The [http://wiki.event-b.org/index.php/Versioned_Reasoners reasoners] are versioned. A reasoner implementation may indeed evolve in time (bug fixes, modifications of the behaviour, etc), even after the old implementation has been used to prove a model. This may lead to potential issues when trying to reuse or replay proofs serialized by the old reasoner implementation. Such problems are solved through the reasoner versioning mechanism.		: The [http://wiki.event-b.org/index.php/Versioned_Reasoners reasoners] are versioned. A reasoner implementation may indeed evolve in time (bug fixes, modifications of the behaviour, etc), even after the old implementation has been used to prove a model. This may lead to potential issues when trying to reuse or replay proofs serialized by the old reasoner implementation. Such problems are solved through the reasoner versioning mechanism.

imported>Pascal: /* Motivations */

2010-01-27T09:39:39Z

Motivations

← Older revision		Revision as of 09:39, 27 January 2010
Line 20:		Line 20:
	= Motivations =		= Motivations =

	~~Areas of improvement~~ for provers can be summarized as follows:		The motivations for improvements to existing provers can be summarized as follows:
	* Reducing proving time and effort.		* Reducing proving time and effort.
	: New proof rules.		: New proof rules, manual and automatic (eg., [http://www.cs.cmu.edu/afs/cs/academic/class/15671-f95/www/handouts/proof/node1.html One point rule], arithmetic rules, etc), have been added to discharge more proofs easily.
	* Reflecting prover ~~implementation corrections~~.		* Reflecting corrections in prover implementations.
	: ~~Reasoner~~ versioning.		: The [http://wiki.event-b.org/index.php/Versioned_Reasoners reasoners] are versioned. A reasoner implementation may indeed evolve in time (bug fixes, modifications of the behaviour, etc), even after the old implementation has been used to prove a model. This may lead to potential issues when trying to reuse or replay proofs serialized by the old reasoner implementation. Such problems are solved through the reasoner versioning mechanism.
	* Reducing proof storage space.		* Reducing proof storage space.
	: ~~Proof purging~~.		: Big proof files are difficult to handle, on the one hand by the Rodin platform (slow access), and on the other hand by users (project sharing).
	: ~~Proof~~ simplifying.		: The [http://wiki.event-b.org/index.php/Proof_Purger_Interface proof purging] and [http://wiki.event-b.org/index.php/Proof_Simplification proof simplifying] mechanisms have been implemented to address this problem.
	* Facilitating manual proof review or reuse.		* Facilitating manual proof review or reuse.
	: ~~Proof~~ skeleton view.		: The [http://wiki.event-b.org/index.php/Proof_Skeleton_View proof skeleton view] allows to quickly browse through a proof. : Moreover, the provided copy/paste feature makes it possible to reuse a stored proof into a new proof.
	: ~~Copy~~ / paste ~~of partial proofs~~.		* Improving prover API.
	* ~~Prover~~ API ~~evolution~~.		: The [http://wiki.event-b.org/index.php/New_Tactic_Providers tactic provider API] has been made more flexible to facilitate tactic contributions.
	: ~~New~~ tactic provider API.

	= Choices / Decisions =		= Choices / Decisions =

imported>Pascal: /* Planning */

2010-01-08T11:44:20Z

Planning

← Older revision		Revision as of 11:44, 8 January 2010
Line 79:		Line 79:

	In the third year of DEPLOY, most effort in the proving area will be put into:		In the third year of DEPLOY, most effort in the proving area will be put into:
	: ~~better~~ management of well-definedness conditions,		: - Better management of well-definedness conditions.
	: ~~improvement~~ to the rule based prover,		: - Improvement to the rule based prover.
	: ~~bridging~~ the gap with external SMT solvers,		: - Bridging the gap with external SMT solvers.
	: ~~supporting~~ mathematical extensions in proofs.		: - Supporting mathematical extensions in proofs.

	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Pascal: /* Available Documentation */

2010-01-08T11:29:00Z

Available Documentation

← Older revision		Revision as of 11:29, 8 January 2010
Line 62:		Line 62:
	The following pages give useful information about prover improvements:		The following pages give useful information about prover improvements:
	* Prover Rules		* Prover Rules
	: See [http://wiki.event-b.org/index.php/Inference_Rules ~~http://wiki.event-b.org/index.php/Inference_Rules~~].		: See [http://wiki.event-b.org/index.php/Inference_Rules Inference Rules].
	: See [http://wiki.event-b.org/index.php/All_Rewrite_Rules ~~http://wiki.event-b.org/index.php/All_Rewrite_Rules~~].		: See [http://wiki.event-b.org/index.php/All_Rewrite_Rules All Rewrite Rules].
	* Proof Skeleton View		* Proof Skeleton View
	: See [http://wiki.event-b.org/index.php/Proof_Skeleton_View ~~http://wiki.event-b.org/index.php/Proof_Skeleton_View~~].		: See [http://wiki.event-b.org/index.php/Proof_Skeleton_View Proof Skeleton View].
	* Proof Purger		* Proof Purger
	: See [http://wiki.event-b.org/index.php/Proof_Purger_Interface ~~http://wiki.event-b.org/index.php/Proof_Purger_Interface~~].		: See [http://wiki.event-b.org/index.php/Proof_Purger_Interface Proof Purger Interface].
	* Prover API evolution		* Prover API evolution
	: See [http://wiki.event-b.org/index.php/New_Tactic_Providers ~~http://wiki.event-b.org/index.php/New_Tactic_Providers~~].		: See [http://wiki.event-b.org/index.php/New_Tactic_Providers New Tactic Providers].
	* Versioned Reasoners		* Versioned Reasoners
	: See [http://wiki.event-b.org/index.php/Versioned_Reasoners ~~http://wiki.event-b.org/index.php/Versioned_Reasoners~~].		: See [http://wiki.event-b.org/index.php/Versioned_Reasoners Versioned Reasoners].

	= Planning =		= Planning =

imported>Pascal: /* Planning */

2010-01-08T11:22:23Z

Planning

← Older revision		Revision as of 11:22, 8 January 2010
Line 76:		Line 76:

	The above mentioned improvements were made available since release 1.1 of the platform:		The above mentioned improvements were made available since release 1.1 of the platform:
	: [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 ~~Release_Notes~~]		: [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release Notes]

	In the third year of DEPLOY, most effort in the proving area will be put into:		In the third year of DEPLOY, most effort in the proving area will be put into:

imported>Pascal: /* Planning */

2010-01-08T11:22:14Z

Planning

← Older revision		Revision as of 11:22, 8 January 2010
Line 76:		Line 76:

	The above mentioned improvements were made available since release 1.1 of the platform:		The above mentioned improvements were made available since release 1.1 of the platform:
	: [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes ~~http://wiki~~.~~event-b.org/index.php/Rodin_Platform_1.1_Release_Notes~~]		: [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release_Notes]

	In the third year of DEPLOY, most effort in the proving area will be put into:		In the third year of DEPLOY, most effort in the proving area will be put into:

imported>Pascal: /* Choices / Decisions */

2010-01-08T11:21:46Z

Choices / Decisions

← Older revision		Revision as of 11:21, 8 January 2010
Line 43:		Line 43:
	based prover, developed by University of Southampton. This API extension was		based prover, developed by University of Southampton. This API extension was
	fully designed and discussed through the Rodin wiki.		fully designed and discussed through the Rodin wiki.
	: See [http://wiki.event-b.org/index.php/New_Tactic_Providers ~~http://wiki.event-b.org/index.php/New_Tactic_Providers~~].		: See [http://wiki.event-b.org/index.php/New_Tactic_Providers New Tactic Providers].

	Following to the detection of incorrect proof rules implemented in the tool, a		Following to the detection of incorrect proof rules implemented in the tool, a

imported>Laurent: Heavy editing of the page

2010-01-07T09:41:59Z

Heavy editing of the page

← Older revision		Revision as of 09:41, 7 January 2010
Line 1:		Line 1:
	= Overview =		= Overview =

	~~All along~~ the ~~lifecycle~~ of the ~~provers~~, ~~the following improvements can be achieved by:~~		Proving is at the core of the Rodin methodology. Therefore, it was no surprise
	* Adding new useful proof rules (to prove sequents that ~~are hard to prove or even not provable at all).~~		that both industrial and academic users reported a lot of feedback on this
	* Correcting bugs in implementations of existing proof rules.		topic. This feedback was provided either by mail or though the SourceForge
	* Implementing new tools to help the ~~user to do proofs.~~		trackers.
	* Evolving the prover API to fit with the needs of prover plug-in developers.

	~~Part~~ of ~~implemented rules~~ and ~~user interface features come from user feedback~~, ~~mainly through SourceForge feature requests. SourceForge bugs are also~~ an ~~important source~~ of ~~input~~ for ~~corrections~~.		Based on this feedback, several actions were taken to improve the existing
			tooling for both automated and interactive proving. Some consisted in
			improving existing tools, while others needed a full design and development of
			new tools (especially for visualizing and managing proofs). Finally, an
			extension of the proving framework API as been realised to allow for the
			development of new plug-ins (such as the rule based prover).

			Systerel has been in charge of existing prover improvements, with support from
			ETH Zurich. The evolution of the API has been designed in close collaboration
			with University of Southampton.

	~~Systerel is in charge of existing prover improvements. University of Southampton gave feedback for the definition of prover API evolution.~~

	= Motivations =		= Motivations =
Line 21:		Line 28:
	: Proof purging.		: Proof purging.
	: Proof simplifying.		: Proof simplifying.
	~~: Non textual database storage.~~
	* Facilitating manual proof review or reuse.		* Facilitating manual proof review or reuse.
	: Proof skeleton view.		: Proof skeleton view.
	: Copy / paste ~~from skeleton to edited proof~~.		: Copy / paste of partial proofs.
	* Prover API evolution.		* Prover API evolution.
	: New tactic provider API.		: New tactic provider API.
Line 30:		Line 36:
	= Choices / Decisions =		= Choices / Decisions =

	~~A problem showed up while trying to implement a new~~ proof ~~rule~~ (~~substitution of the domain of a total function~~). ~~It required~~ to ~~make a reasoner able~~ to ~~propose several substitutions~~ for ~~the same function~~. ~~More generally, the problem~~ was ~~to parameterize how a given rule shall~~ be ~~applied~~, ~~depending on a user choice among various possible applications. Each choice should be displayed~~ in the ~~popup list in interactive proving.~~		The proving API one year ago asked that available proof commands would be
	~~Before the improvement~~, ~~a given reasoner could only propose one application. Thus, we had to define a new, more general, API. At the same time, the~~ University of Southampton was ~~working on Rule-Based Provers~~ and ~~they were also meeting difficulties dealing with~~ the ~~old API~~.		completely determined statically (at application startup). This decision had
	~~We then started a discussion in order to define a new API that would address everyone's needs. Proposals were made on a wiki page (~~[http://wiki.event-b.org/index.php/New_Tactic_Providers http://wiki.event-b.org/index.php/New_Tactic_Providers]) ~~until it reached a stable state~~.		to be revised to allow for dynamically contributed proof commands. This change
			was required not only for regular rules where several options could be
			considered based on available hypotheses, but also for plugging in the rule
			based prover, developed by University of Southampton. This API extension was
			fully designed and discussed through the Rodin wiki.
			: See [http://wiki.event-b.org/index.php/New_Tactic_Providers http://wiki.event-b.org/index.php/New_Tactic_Providers].

			Following to the detection of incorrect proof rules implemented in the tool, a
			complete review of all proof rules and their implementation has been carried
			out. Moreover, a review procedure has been defined to lower the risk that such
			glitches happen again in the future. Also, the decision to develop a rule
			based prover (where rules must be formally proved before being used) will
			provide greater confidence in the correctness of the prover.

	~~During~~ the ~~last DEPLOY workshop (October 2009)~~, ~~the idea arose to change proof storage means in order to enlighten~~ proof files~~, which~~ can grow very large ~~with current XML~~ Rodin database ~~storage~~. ~~Possible solutions are~~ to be investigated.		In the current setting, proof files can grow very large (in the order of tens
			of megabytes). This is partly caused by the usage of the Rodin database
			mechanism for storing proofs in XML files. At the last DEPLOY workshop
			(October 2009), several other options have been discussed to reduce this memory
			footprint. This issue is beging further investigated.

	= Available Documentation =		= Available Documentation =
Line 55:		Line 77:
	The above mentioned improvements were made available since release 1.1 of the platform:		The above mentioned improvements were made available since release 1.1 of the platform:
	: [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes]		: [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes]

			In the third year of DEPLOY, most effort in the proving area will be put into:
			: better management of well-definedness conditions,
			: improvement to the rule based prover,
			: bridging the gap with external SMT solvers,
			: supporting mathematical extensions in proofs.

	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]