Difference between revisions of "Generic Instantiation"

From Event-B
Jump to: navigation, search
m
Line 3: Line 3:
 
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 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 University of Southampton) is as follows: [[Image:Generic Instantiation Proposal.pdf | Generic Instantiation Proposal]].
+
The proposal (from the University of Southampton) is as follows: [[Image:Generic Instantiation Proposal.pdf | Generic Instantiation Proposal]].
  
A Generic Instantiation tool is developed for Event-B. See [http://wiki.event-b.org/index.php/Generic_Instantiation_Plug-in_User_Guide Generic Instantiation Plug-in User Guide].
+
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].
  
 
Another generic instantiation tool is developed by Hitachi Ltd. and ETH Zurich [http://wiki.event-b.org/index.php/Generic_Instantiation_User_Guide Generic Instantiation User Guide].
 
Another generic instantiation tool is developed by Hitachi Ltd. and ETH Zurich [http://wiki.event-b.org/index.php/Generic_Instantiation_User_Guide Generic Instantiation User Guide].
 
[[Category:Design]]
 
[[Category:Design]]

Revision as of 15:01, 18 February 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 Generic Instantiation User Guide.