Difference between revisions of "Generic Instantiation"

From Event-B
Jump to: navigation, search
m (Issues: Instantiation of Carrier Sets)
m (Issues: Instantiation of Carrier Sets)
Line 4: Line 4:
 
== Issues: Instantiation of Carrier Sets ==
 
== Issues: Instantiation of Carrier Sets ==
  
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>
+
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 <math>S</math>
  
 
<math>  S \neq \emptyset</math>
 
<math>  S \neq \emptyset</math>
Line 12: Line 12:
 
Both these axioms can be generated as theorems in the instantiating context which need to be proved.
 
Both these axioms can be generated as theorems in the instantiating context which need to be proved.
  
However, the second theorem can be proved if <code>S</code> is instantiated to another carrier set in the instantiating context.
+
However, the second theorem can be proved if <math>S</math> is instantiated to another carrier set in the instantiating context.
  
 
This could be a limitation of generic instantiation (<font color=red>Son: Is this a real limitation? To be discussed</font>) and may restrict the applicability of the approach. One should allow carrier sets to be instantiated to some set expressions which are not necessary carrier sets themselves.
 
This could be a limitation of generic instantiation (<font color=red>Son: Is this a real limitation? To be discussed</font>) and may restrict the applicability of the approach. One should allow carrier sets to be instantiated to some set expressions which are not necessary carrier sets themselves.
  
 
The issue, here is that this will definitely introduce unsoundness into the instantiation process.  An example is formula which are no longer well-defined, and the meaning operator such <code>id</code> or <code>prj1</code>, <code>prj2</code> has been changed (<font color=red>Son: Maybe some examples are needed</font>).
 
The issue, here is that this will definitely introduce unsoundness into the instantiation process.  An example is formula which are no longer well-defined, and the meaning operator such <code>id</code> or <code>prj1</code>, <code>prj2</code> has been changed (<font color=red>Son: Maybe some examples are needed</font>).

Revision as of 17:25, 26 March 2010

The initial proposal from Southampton is as follows. File:Proposal generic instantiation rodin.pdf.

Issues: Instantiation of Carrier Sets

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 <math>S</math>

<math> S \neq \emptyset</math>

<math>\forall x \qdot x \in S</math>

Both these axioms can be generated as theorems in the instantiating context which need to be proved.

However, the second theorem can be proved if <math>S</math> is instantiated to another carrier set in the instantiating context.

This could be a limitation of generic instantiation (Son: Is this a real limitation? To be discussed) and may restrict the applicability of the approach. One should allow carrier sets to be instantiated to some set expressions which are not necessary carrier sets themselves.

The issue, here is that this will definitely introduce unsoundness into the instantiation process. An example is formula which are no longer well-defined, and the meaning operator such id or prj1, prj2 has been changed (Son: Maybe some examples are needed).