|
|
| (11 intermediate revisions by 2 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 with any set expressions (which contains existing carrier sets and constants).
| | The proposal (from the University of Southampton) is as follows: [[Image:Generic Instantiation Proposal.pdf | Generic Instantiation Proposal]]. |
|
| |
|
| However, besides the declared axioms in the development to be extended there are two ''implicit'' axioms for every carrier set <math>S</math>:
| | 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]. |
| # ''non-emptiness'': <math> S \neq \emptyset</math>
| |
| # ''maximality'': <math>\forall x \qdot x \in S</math>
| |
|
| |
|
| There are two ways to tackle these implicit axioms:
| | 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]. |
| # Restrict instantiation of carrier sets to type expressions
| |
| # Allow for general instantiation with some additions
| |
|
| |
|
| In the first option, a carrier set can only be instantiated with an expression denoting a type. This can be syntactically verified. The advantage of this solution is that the two axioms are then verified implicitly, because any type expression satisfies these two axioms. Moreover, as type expressions are the only expressions that can satisfy both axioms, this is the only option which is viable if we are to consider that these two axioms must be fulfilled by an instantiation.
| | The University of Southampton, Hitachi Ltd. and ETH Zurich are discussing on how to consolidate the work and merge the two plug-ins. |
|
| |
|
| The second option consists in relaxing the conditions for generic instantiation by dropping the second implicit axiom (maximality). Then, a carrier set could be instantiated by any expression that denotes a non-empty set. However, dropping maximality does not come without strong consequences, because it is the justification for the type inference used in event-B:
| | [[Category:Generic Instantiation Plug-in]] |
| | | [[Category:User documentation]] |
| For instance, les us consider a context declaring a carrier set <math>S</math>, a constant <math>c</math> and the ''theorem'' <math>c\in S</math>. This context does not contain any axiom, but <math>c</math> is typed by inference in the theorem. This context can easily be proved as the theorem can be deduced from typing. Then, this context could be instantiated by taking:
| | [[Category:Design]] |
| :<math>S\bcmeq 1\upto2</math>
| |
| :<math>c\bcmeq 3</math>
| |
| which would bring the instantiated ''theorem'' <math>3\in 1\upto2</math> which is obviously false.
| |
| | |
| Consequently, if we drop the maximality axiom, we have to generate additional proof obligations for showing that every instantiation of a constant belongs to the instantiation of its type.
| |
| | |
| However, there are more general issues. If a context contains theorem
| |
| :<math>\forall x\qdot x\in S</math>
| |
| then using the same instantiation for <math>S</math> as above, one would obtain the instantiated ''theorem''
| |
| :<math>\forall x\qdot x\in 1\upto2</math> | |
| which is also wrong. To mitigate this issue, all quantifications occurring in the initial context would need to be complemented by adding typing predicates for every quantified variables. For instance, the theorem above would be rewritten as
| |
| :<math>\forall x\qdot x\in S \limp x\in S</math>
| |
| where we have added a typing predicate on the left-hand side of implication.
| |
| | |
| Similar issues happen for generic operators such as identity, where types need again to be explicited before instantiation (e.g., <math>\id</math> would become <math>S\domres \id</math>).
| |
| | |
| All this can be implemented in a tool, but it can be deceptive to users as the instantiated context can become quite different from the original context (when a lot of typing predicates and expressions have been added automatically by the instantiation plug-in).
| |
| | |
| In retrospect, the first option (instantiation only by type expressions) does not introduce any loss of generality. If one has a context with a carrier set <math>S</math> and wants to instantiate this carrier set with an arbitrary expression, it is always possible to modify the context by introducing an additional constant <math>s</math> and replace all (implicit or explicit) occurrences of <math>S</math> by <math>s</math>. This would be done in a manner similar to all the adjustments proposed for the second option above. However, all these adjustments would be made under the control of proof, rather than performed by a tool. Moreover, the user would have the opportunity to see exactly the consequences of replacing the carrier set by the constant and adjusting his model consequently. Finally, the advantage of the first option is that it keeps instantiation very simple, both for implementation in tools and for explaining how it works to prospective users.
| |
| | |
| [[Category:Design proposal]] | |
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.
