Generic Instantiation: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Asiehsalehi No edit summary |
imported>Asiehsalehi No edit summary |
||
| Line 1: | Line 1: | ||
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. | 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 proposal (from University of Southampton) is as follows | The proposal (from University of Southampton) is as follows: [[Image:Generic Instantiation Proposal.pdf | Generic Instantiation Proposal]]. | ||
[[Image:Generic Instantiation Proposal.pdf | Generic Instantiation Proposal]]. | |||
A Generic Instantiation tool is developed for Event-B. See the [http://wiki.event-b.org/index.php/Generic_Instantiation_Plug-in_User_Guide Generic Instantiation Plug-in User Guide] page for Generic Instantiation Plug-in User Guide. | A Generic Instantiation tool is developed for Event-B. See the [http://wiki.event-b.org/index.php/Generic_Instantiation_Plug-in_User_Guide Generic Instantiation Plug-in User Guide] page for Generic Instantiation Plug-in User Guide. | ||
[[Category:Design]] | [[Category:Design]] | ||
Revision as of 17:55, 4 December 2012
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 proposal (from University of Southampton) is as follows: File:Generic Instantiation Proposal.pdf.
A Generic Instantiation tool is developed for Event-B. See the Generic Instantiation Plug-in User Guide page for Generic Instantiation Plug-in User Guide.
