Generic Instantiation

From Event-B
Revision as of 17:11, 26 March 2010 by Son (talk | contribs) (Issues: Instantiation of Carrier Sets)
Jump to: navigation, search

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<code>

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

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