Generic Instantiation
From Event-B
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 Atomicity Decomposition Plug-in User Guide page for Generic Instantiation Plug-in User Guide.
