Generic Instantiation: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Laurent
mNo edit summary
imported>Asiehsalehi
No edit summary
 
(13 intermediate revisions by 3 users not shown)
Line 1: Line 1:
The initial proposal from Southampton is as follows.
Event-B lacks the ability to instantiate and reuse generic developments in other formal developments. We propose a way of instantiating generic models and extending the instantiation to a chain of refinements. We define sufficient proof obligations to ensure that the proofs associated to a generic development remain valid in an instantiated development thus avoiding re-proofs.  
[[Image:Proposal_generic_instantiation_rodin.pdf | Proposal for generic instantiation of machines]].


== Issues: Instantiation of Carrier Sets ==
The instances inherit properties from the generic development (pattern) and are parameterised by renaming/replacing those properties to specific instance element names. Proof obligations are generated to ensure that assumptions used in the pattern are satisfied in the instantiation. In that sense our approach avoids re-proof of pattern proof obligations in the instantiation. The reusability of a development is expressed by instantiating a development (pattern) according to a more specific problem.


Currently, the proposal mentions that the carrier sets can be instantiated with any set expressions (which contains existing carrier sets and constants). Besides the declared axioms in the development to be extended there are two ''hidden'' axioms for every carrier set <math>S</math>:
The proposal (from the University of Southampton) is as follows: [[Image:Generic Instantiation Proposal.pdf | Generic Instantiation Proposal]].


<math>  S \neq \emptyset</math>
A Generic Instantiation tool is developed for Event-B by the University of Southampton. See [http://wiki.event-b.org/index.php/Generic_Instantiation_Plug-in_User_Guide Generic Instantiation Plug-in User Guide].


<math>\forall x \qdot x \in S</math>
Another generic instantiation tool is developed by Hitachi Ltd. and ETH Zurich. See [http://wiki.event-b.org/index.php/Generic_Instantiation_User_Guide Generic Instantiation User Guide].


Both these axioms can be generated as theorems in the instantiating context which need to be proved.
The University of Southampton, Hitachi Ltd. and ETH Zurich are discussing on how to consolidate the work and merge the two plug-ins.


However, the second theorem can be proved only if <math>S</math> is instantiated with a type expression.
[[Category:Generic Instantiation Plug-in]]
 
[[Category:User documentation]]
This could be a limitation of generic instantiation (<font color=red>Son: Is this a real limitation? To be discussed</font>) and may restrict the applicability of the approach. One should allow carrier sets to be instantiated with some set expressions which are not necessary types themselves.
[[Category:Design]]
 
The issue, here is that this will definitely introduce unsoundness into the instantiation process.  Examples include when formula which are no longer well-defined; and/or the meaning operator such <code>id</code> or <code>prj1</code>, <code>prj2</code> has been changed (<font color=red>Son: Maybe some examples are needed</font>).
 
[[Category:Design proposal]]

Latest revision as of 15:23, 4 July 2013

Event-B lacks the ability to instantiate and reuse generic developments in other formal developments. We propose a way of instantiating generic models and extending the instantiation to a chain of refinements. We define sufficient proof obligations to ensure that the proofs associated to a generic development remain valid in an instantiated development thus avoiding re-proofs.

The instances inherit properties from the generic development (pattern) and are parameterised by renaming/replacing those properties to specific instance element names. Proof obligations are generated to ensure that assumptions used in the pattern are satisfied in the instantiation. In that sense our approach avoids re-proof of pattern proof obligations in the instantiation. The reusability of a development is expressed by instantiating a development (pattern) according to a more specific problem.

The proposal (from the University of Southampton) is as follows: File:Generic Instantiation Proposal.pdf.

A Generic Instantiation tool is developed for Event-B by the University of Southampton. See Generic Instantiation Plug-in User Guide.

Another generic instantiation tool is developed by Hitachi Ltd. and ETH Zurich. See Generic Instantiation User Guide.

The University of Southampton, Hitachi Ltd. and ETH Zurich are discussing on how to consolidate the work and merge the two plug-ins.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Generic_Instantiation&oldid=5336’