Generic Instantiation: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Son
imported>Asiehsalehi
No edit summary
 
(26 intermediate revisions by 4 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 to any set expressions (which contains existing carrier sets and constants). Beside the declared axioms in the development to be extended there are two ''hidden'' axioms about a carrier set <code>S<code>
The proposal (from the University of Southampton) is as follows: [[Image:Generic Instantiation Proposal.pdf | Generic Instantiation Proposal]].


\math{S}
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. See [http://wiki.event-b.org/index.php/Generic_Instantiation_User_Guide 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.
 
[[Category:Generic Instantiation Plug-in]]
[[Category:User documentation]]
[[Category:Design]]

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’