D23 Pattern Plug-in - Revision history

imported>Pascal: /* Planning */

2010-01-27T14:43:16Z

Planning

imported>Afuerst at 14:41, 27 January 2010

2010-01-27T14:41:14Z

← Older revision		Revision as of 14:41, 27 January 2010
Line 62:		Line 62:

	The current version has been passed to interested partners for evaluation. The Date for the missing functionalities being implemented in the plug-in depends on the		The current version has been passed to interested partners for evaluation. The Date for the missing functionalities being implemented in the plug-in depends on the
	responses of the evaluators and their need of having those functionalities.		responses of the evaluators and their need of having those functionalities available.
	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Afuerst at 14:38, 27 January 2010

2010-01-27T14:38:58Z

@@ Line 43: / Line 43: @@
 The pattern tool is available as an external plug-in for Rodin release 1.1 and above.
 :See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release Notes] and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].
 [[Category:D23 Deliverable]]

imported>Pascal: /* Choices / Decisions */

2010-01-26T15:38:17Z

Choices / Decisions

← Older revision		Revision as of 15:38, 26 January 2010
Line 24:		Line 24:

	= Choices / Decisions =		= Choices / Decisions =
	*To support the developer and guide him through the ~~hole~~ pattern process we designed a plug-in providing a graphical wizard that consists in several pages, one for each major step.		*To support the developer and guide him through the whole pattern process, we designed a plug-in providing a graphical wizard that consists in several pages, one for each major step.

	*It was desired to have direct access to the pattern plug-in in form of an API in addition to the wizard. This enables other Rodin developers to use the pattern plug-in programmatically. For this, the first version of the plug-in was revised by having the generation apart from the pure graphical interface.		*It was desired to have direct access to the pattern plug-in in form of an API in addition to the wizard. This enables other Rodin developers to use the pattern plug-in programmatically. For this, the first version of the plug-in was revised by having the generation apart from the pure graphical interface.

imported>Pascal: /* Planning */

2010-01-08T11:44:55Z

Planning

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

	The pattern tool is available as an external plug-in for Rodin release 1.1 and above.		The pattern tool is available as an external plug-in for Rodin release 1.1 and above.
	:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release Notes]		:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release Notes] and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].
	:and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].
	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Pascal: /* Planning */

2010-01-08T11:35:16Z

Planning

← Older revision		Revision as of 11:35, 8 January 2010
Line 42:		Line 42:

	The pattern tool is available as an external plug-in for Rodin release 1.1 and above.		The pattern tool is available as an external plug-in for Rodin release 1.1 and above.
	:See [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~~]		:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release Notes]
	:and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes ~~http://wiki~~.~~event-b.org/index.php/Rodin_Platform_1.2_Release_Notes~~].		:and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].
	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Pascal: /* Available Documentation */

2010-01-08T11:34:48Z

Available Documentation

← Older revision		Revision as of 11:34, 8 January 2010
Line 37:		Line 37:
	Besides the documents mentioned above focusing on the theory there also exists a wiki page that is more tool related.		Besides the documents mentioned above focusing on the theory there also exists a wiki page that is more tool related.

	:See [http://wiki.event-b.org/index.php/Pattern ~~http://wiki.event-b.org/index.php/~~Pattern] for a short overview of the idea of patterns in Event-B and stepwise instructions for both developers interested in using the wizard and those more thrilled by APIs.		:See [http://wiki.event-b.org/index.php/Pattern Pattern] for a short overview of the idea of patterns in Event-B and stepwise instructions for both developers interested in using the wizard and those more thrilled by APIs.

	= Planning =		= Planning =

imported>Pascal: /* Typos */

2009-12-04T11:13:38Z

Typos

← Older revision		Revision as of 11:13, 4 December 2009
Line 15:		Line 15:
	*Reusing solutions to problems:		*Reusing solutions to problems:

	:Usually there is more than one solution to a problem. But not every solution is of equal quality. There are solutions that are especially easy, elegant or short. For a lot of problems there is a best practice to solve it. Having a pattern consisting this "best" solution one does not have to bother finding it ever again.		:Usually there is more than one solution to a problem. But not every solution is of equal quality. There are solutions that are especially easy, elegant or short. For a lot of problems there is a best practice to solve it. Having a pattern consisting in this "best" solution one does not have to bother finding it ever again.

	*Reusing proofs:		*Reusing proofs:

	:As mentioned above, the pattern approach is able ~~of generating~~ a refinement that is correct by construction. This is possible because the construction of the refinement leads to the same proof obligations as in the pattern. Since they are proved in the pattern there is no need do the same proof steps in the current development again. Reusing proofs, especially manual discharged proof obligations, saves a lot of time for the developer. The drawback reflects in the effort to match the pattern with the problem before a refinement can be generated. But this effort can be minimised by a tool that does as many steps as possible automatically or at least supports the developer wherever user interaction is required.		:As mentioned above, the pattern approach is able to generate a refinement that is correct by construction. This is possible because the construction of the refinement leads to the same proof obligations as in the pattern. Since they are proved in the pattern there is no need do the same proof steps in the current development again. Reusing proofs, especially manual discharged proof obligations, saves a lot of time for the developer. The drawback reflects in the effort to match the pattern with the problem before a refinement can be generated. But this effort can be minimised by a tool that does as many steps as possible automatically or at least supports the developer wherever user interaction is required.

	Case studies showed also another motivation ~~for having~~ a tool. Using the pattern approach without tool support, especially the generation of the refinement, is time consuming and error prone. In this last step in the whole procedure, basically two machines are merged by copying and pasting elements. This often leads to name clashes where a developer can easily loose track. Having a tool checking for possible name clashes in advance can avoid a lot of confusion.		Case studies showed also another motivation to have such a tool. Using the pattern approach without tool support, especially the generation of the refinement, is time consuming and error prone. In this last step in the whole procedure, basically two machines are merged by copying and pasting elements. This often leads to name clashes where a developer can easily loose track. Having a tool checking for possible name clashes in advance can avoid a lot of confusion.

	= Choices / Decisions =		= Choices / Decisions =
	*To support the developer and guide him through the hole pattern process we designed a plug-in providing a graphical wizard that consists of several pages, one for each major step.		*To support the developer and guide him through the hole pattern process we designed a plug-in providing a graphical wizard that consists in several pages, one for each major step.

	*It was desired to have direct access to the pattern plug-in in form of an API in addition to the wizard. This enables other Rodin developers to use the pattern plug-in ~~programatically~~. For this, the first version of the plug-in was revised by having the generation apart from the pure graphical interface.		*It was desired to have direct access to the pattern plug-in in form of an API in addition to the wizard. This enables other Rodin developers to use the pattern plug-in programmatically. For this, the first version of the plug-in was revised by having the generation apart from the pure graphical interface.

	*In order to speed up the process, all required Event-B element of the involved machines are collected in a central data object. Certain elements are contained in more than one list dependent to their attributes (e.g. a matched and renamed event).		*In order to speed up the process, all required Event-B element of the involved machines are collected in a central data object. Certain elements are contained in more than one list dependent to their attributes (e.g. a matched and renamed event).

imported>Afuerst at 14:23, 25 November 2009

2009-11-25T14:23:58Z

imported>Afuerst at 16:03, 24 November 2009

2009-11-24T16:03:35Z

← Older revision		Revision as of 16:03, 24 November 2009
Line 1:		Line 1:
	= Overview =		= Overview =
	The pattern plug-in enables an Event-B developer to make advantage of former models and their refinements. The refinement, which can be seen as the solution to the problem encountered in the abstraction, can be reused if the abstracted problem is similar to a part of the problem at hand. We call such reusable models to be patterns and since they are just regular models every model can be a pattern in principle. There is only a limit in terms of usability that correlates with the specificity of the model.		The pattern plug-in enables an Event-B developer to make advantage of former models and their refinements.

	As mentioned above, the problem at hand (or at least part of it) has to be similar to pattern we want to use. To ensure this similarity the developer has to match the pattern with the problem at hand. After a successful matching of the models the solution ~~(refinement~~) of the pattern can be incorporated into the problem at hand ~~which~~ leads to a refinement of this model that is correct by construction. In other words, a new refinement of the problem at hand can be generated which includes the achievements of the pattern and is correct without proving any proof obligation.		A refinement can also be seen as the solution to the problem encountered in the abstraction. One can make use of such a solution if the solved problem appears in current development. Instead of solving the problem again we directly use the already known solution. Certainly, we have to show that our current problem (or at least part of it) is the same as the solved problem.

			We refer to such a reusable model containing a certain solution to a problem as a pattern. Since these patterns are just regular models every model can be a pattern in principle. There is only a limit in terms of usability that correlates with the specificity of the model (solved problem).

			As mentioned above, the problem at hand (or at least part of it) has to be similar to the pattern we want to use. To ensure this similarity the developer has to match the pattern with the problem at hand. After a successful matching of the models (problems) the refinement (solution) of the pattern can be incorporated into the problem at hand. This leads to a refinement of this model that is correct by construction. In other words, a new refinement of the problem at hand can be generated which includes the achievements of the pattern and is correct without proving any proof obligation.

	= Motivations =		= Motivations =
	The idea of patterns and their usage is described in every detail in the Master Thesis [http://e-collection.ethbib.ethz.ch/view/eth:41612 "Design Patterns in Event-B and Their Tool Support“]. This approach follows the earlier proposal of Jean-Raymond Abrial and Thai Son Hoang stated in the paper [http://www.springerlink.com/content/d088h53531x7226j "Using Design Patterns in Formal Methods: An Event-B Approach"].		The idea of patterns and their usage is described in every detail in the Master Thesis [http://e-collection.ethbib.ethz.ch/view/eth:41612 "Design Patterns in Event-B and Their Tool Support“]. This approach follows the earlier proposal of Jean-Raymond Abrial and Thai Son Hoang stated in the paper [http://www.springerlink.com/content/d088h53531x7226j "Using Design Patterns in Formal Methods: An Event-B Approach"].

	~~The advantage of the pattern approach lies in the "recycling" of proofs~~. Reusing ~~proofs, especially manual discharged proof obligations, saves a lot of time for the developer. The drawback reflects in the effort~~ to match the pattern with the problem before a refinement can be generated. But this effort can be minimised by a tool that does as many steps as possible automatically or at least supports the developer wherever user interaction is required.		There are two main motivations to use patterns.

			*Reusing solutions to problems:

	Case studies ~~of using~~ the pattern approach without tool support ~~showed that~~ especially the generation of the refinement is time consuming and error prone. ~~This~~ last step in ~~which~~ basically two machines are merged by copying and pasting elements often leads to name clashes where a developer can easily loose track. Having a tool checking for possible name clashes in advance can avoid a lot of confusion.		:Usually there is more than one solution to a problem. But not every solution is of equal quality. There are solutions that are especially easy, elegant or short. For a lot of problems there is a best practice to solve it. Having a pattern consisting this "best" solution one does not have to bother again finding it.

			*Reusing proofs:

			:As mentioned above, the pattern approach is able of generating a refinement that is correct by construction. This is possible because the constructing of the refinement leads to the same proof obligations as in the pattern. Since they are proved in the pattern there is no need do the same proof steps in the current development again. Reusing proofs, especially manual discharged proof obligations, saves a lot of time for the developer. The drawback reflects in the effort to match the pattern with the problem before a refinement can be generated. But this effort can be minimised by a tool that does as many steps as possible automatically or at least supports the developer wherever user interaction is required.

			Case studies showed also another motivation for having a tool. Using the pattern approach without tool support, especially the generation of the refinement, is time consuming and error prone. In this last step in the whole procedure, basically two machines are merged by copying and pasting elements. This often leads to name clashes where a developer can easily loose track. Having a tool checking for possible name clashes in advance can avoid a lot of confusion.

	= Choices / Decisions =		= Choices / Decisions =
Line 16:		Line 28:
	*It was desired to have direct access to the pattern plug-in in form of an API in addition to the wizard. This enables other Rodin developers to use the pattern plug-in programatically. For this the first version of the plug-in was revised by having the generation apart from the pure graphical interface.		*It was desired to have direct access to the pattern plug-in in form of an API in addition to the wizard. This enables other Rodin developers to use the pattern plug-in programatically. For this the first version of the plug-in was revised by having the generation apart from the pure graphical interface.

	*In order to speed up the process, all required Event-B element of the involved machines are collected in a data object. Certain elements are contained in more than one list dependent to their attributes (e.g. a matched and renamed event).		*In order to speed up the process, all required Event-B element of the involved machines are collected in a central data object. Certain elements are contained in more than one list dependent to their attributes (e.g. a matched and renamed event).

			*The correctness of the matching, which is checking the syntactical equality of the matched elements (guards, actions) is left to the developer for the moment. The automation of this was postponed to a later version as it appears to us as a minor point.

	*~~Having complementary lists in~~ the ~~data object such as matched and not~~-~~matched events and~~ in ~~addition~~ a ~~combination containing all events~~ is ~~surely redundant. On~~ the ~~other hand, does it prevent countless iterations and checks that would be needed~~ to ~~keep~~ the ~~wizard up-to-date?~~		*As the pattern plug-in is in a pre-release phase, there is an option to generate the proof obligation in order to control the generation.

	= Available Documentation =		= Available Documentation =

← Older revision		Revision as of 14:43, 27 January 2010
Line 43:		Line 43:
	The pattern tool is available as an external plug-in for Rodin release 1.1 and above.		The pattern tool is available as an external plug-in for Rodin release 1.1 and above.
	:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release Notes] and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].		:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release Notes] and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].


	The current version of the pattern plug-in covers the following functionalities:		The current version of the pattern plug-in covers the following functionalities:
	* Interactive guidance for matching the variables		* Interactive guidance for matching the variables.
	* Interactive guidance for matching the events and their parameters, guards and actions		* Interactive guidance for matching the events and their parameters, guards and actions.
	* Collecting the seen contexts in order to enable the user to match the carrier sets and constants		* Collecting the seen contexts in order to enable the user to match the carrier sets and constants.
	* Checking for name clashes and proposing possible renaming		* Checking for name clashes and proposing possible renaming.
	* Detection of disappearing variables that have to be replaced		* Detection of disappearing variables that have to be replaced.
	* Detection of disappearing parameters that have to be replaced		* Detection of disappearing parameters that have to be replaced.
	* Generation of the new machine file		* Generation of the new machine file.


	Desired functionalities that are missing in the current version:		Desired functionalities that are missing in the current version:
	* Automated syntactical check of the matched elements		* Automated syntactical check of the matched elements.
	* Automated extraction of the glueing invariants to find the replacement for disappearing variables		* Automated extraction of the glueing invariants to find the replacement for disappearing variables.
	* Automated extraction of the witnesses to find the replacement for disappearing parameters		* Automated extraction of the witnesses to find the replacement for disappearing parameters.

			The current version has been passed to interested partners for evaluation. The date for the missing functionalities being implemented in the plug-in will depend on the responses of the evaluators and their need of having those functionalities available.

	~~The current version has been passed to interested partners for evaluation. The Date for the missing functionalities being implemented in the plug-in depends on the~~
	~~responses of the evaluators and their need of having those functionalities available.~~
	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

← Older revision		Revision as of 14:23, 25 November 2009
Line 2:		Line 2:
	The pattern plug-in enables an Event-B developer to make advantage of former models and their refinements.		The pattern plug-in enables an Event-B developer to make advantage of former models and their refinements.

	A refinement can also be seen as the solution to the problem encountered in the abstraction. One can make use of such a solution if the solved problem appears in current development. Instead of solving the problem again we directly use the already known solution. Certainly, we have to show that our current problem (or at least part of it) is the same as the solved problem.		A refinement can also be seen as the solution to the problem encountered in the abstraction. One can make use of such a solution if the solved problem appears in the current development. Instead of solving the problem again we directly use the already known solution. Certainly, we have to show that our current problem (or at least part of it) is the same as the solved problem.

	We refer to such a reusable model containing a certain solution to a problem as a pattern. Since these patterns are just regular models every model can be a pattern in principle. There is only a limit in terms of usability that correlates with the specificity of the model (solved problem).		We refer to such a reusable model containing a certain solution to a problem as a pattern. Since these patterns are just regular models every model can be a pattern in principle. There is only a limit in terms of usability that correlates with the specificity of the model (solved problem).
Line 15:		Line 15:
	*Reusing solutions to problems:		*Reusing solutions to problems:

	:Usually there is more than one solution to a problem. But not every solution is of equal quality. There are solutions that are especially easy, elegant or short. For a lot of problems there is a best practice to solve it. Having a pattern consisting this "best" solution one does not have to bother ~~again~~ finding it.		:Usually there is more than one solution to a problem. But not every solution is of equal quality. There are solutions that are especially easy, elegant or short. For a lot of problems there is a best practice to solve it. Having a pattern consisting this "best" solution one does not have to bother finding it ever again.

	*Reusing proofs:		*Reusing proofs:

	:As mentioned above, the pattern approach is able of generating a refinement that is correct by construction. This is possible because the ~~constructing~~ of the refinement leads to the same proof obligations as in the pattern. Since they are proved in the pattern there is no need do the same proof steps in the current development again. Reusing proofs, especially manual discharged proof obligations, saves a lot of time for the developer. The drawback reflects in the effort to match the pattern with the problem before a refinement can be generated. But this effort can be minimised by a tool that does as many steps as possible automatically or at least supports the developer wherever user interaction is required.		:As mentioned above, the pattern approach is able of generating a refinement that is correct by construction. This is possible because the construction of the refinement leads to the same proof obligations as in the pattern. Since they are proved in the pattern there is no need do the same proof steps in the current development again. Reusing proofs, especially manual discharged proof obligations, saves a lot of time for the developer. The drawback reflects in the effort to match the pattern with the problem before a refinement can be generated. But this effort can be minimised by a tool that does as many steps as possible automatically or at least supports the developer wherever user interaction is required.

	Case studies showed also another motivation for having a tool. Using the pattern approach without tool support, especially the generation of the refinement, is time consuming and error prone. In this last step in the whole procedure, basically two machines are merged by copying and pasting elements. This often leads to name clashes where a developer can easily loose track. Having a tool checking for possible name clashes in advance can avoid a lot of confusion.		Case studies showed also another motivation for having a tool. Using the pattern approach without tool support, especially the generation of the refinement, is time consuming and error prone. In this last step in the whole procedure, basically two machines are merged by copying and pasting elements. This often leads to name clashes where a developer can easily loose track. Having a tool checking for possible name clashes in advance can avoid a lot of confusion.
Line 26:		Line 26:
	*To support the developer and guide him through the hole pattern process we designed a plug-in providing a graphical wizard that consists of several pages, one for each major step.		*To support the developer and guide him through the hole pattern process we designed a plug-in providing a graphical wizard that consists of several pages, one for each major step.

	*It was desired to have direct access to the pattern plug-in in form of an API in addition to the wizard. This enables other Rodin developers to use the pattern plug-in programatically. For this the first version of the plug-in was revised by having the generation apart from the pure graphical interface.		*It was desired to have direct access to the pattern plug-in in form of an API in addition to the wizard. This enables other Rodin developers to use the pattern plug-in programatically. For this, the first version of the plug-in was revised by having the generation apart from the pure graphical interface.

	*In order to speed up the process, all required Event-B element of the involved machines are collected in a central data object. Certain elements are contained in more than one list dependent to their attributes (e.g. a matched and renamed event).		*In order to speed up the process, all required Event-B element of the involved machines are collected in a central data object. Certain elements are contained in more than one list dependent to their attributes (e.g. a matched and renamed event).