Difference between revisions of "Generic Instantiation"
From Event-B
Jump to navigationJump to searchimported>Asiehsalehi (Replaced content with "The initial proposal from Southampton is as follows. Proposal for generic instantiation of machines. [[Category:Des...") |
imported>Asiehsalehi |
||
| 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. | |
| − | |||
| + | The proposal (from University of Southampton) is as follows. | ||
| + | [[Image:Generic Instantiation Proposal.pdf | Generic Instantiation Proposal]]. | ||
| − | + | [[Category:Design]] | |
| − | [[Category:Design | ||
Revision as of 17:50, 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.
