Difference between revisions of "Generic Instantiation"
From Event-B
Jump to navigationJump to searchimported>Son m |
imported>Son |
||
| Line 3: | Line 3: | ||
== 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> | ||
| + | |||
| + | \math{S} | ||
Revision as of 16:09, 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 S
\math{S}
