#349 Partial bijection

[Tomas]

Support also Partial bijection: S ⤗ T (S >+>> T)

S ⤗ T = S ⤔ T ∩ S ⤀ T

Partial bijection represents 1..1 → 0..1 relation and is Surjective, Injective, Functional but not Total (in comparison to Bijection, which is also Total and represents the 1..1 → 1..1 relation).

The support shall also be extended to the iUML-B Classdiagram (generator component).

[Laurent Voisin]

Dear Tomas, please take care that partial bijection is part of classical B (the B method) but has been dropped in Event-B. This operator is thus not supported by the core of Rodin. You always can use its converse which is a total injection and is usually simpler to grasp (feels more natural).

[Tomas]

In my case the Event-B code is generated from the iUML-B Classdiagrams and the partial bijection would be useful to represent the 1..1 → 0..1 relation. Currently (total) bijection is generated in this case which is simply wrong.

Of course, the Event-B generator may treat this case as an exception and generate some kind of compound relation, but this would break the symmetry and would be difficult to comprehend in case of further model treatment (reasoning, animation etc.)

The (re-)introduction of partial bijection is the simplest solution for such use cases.

[Laurent Voisin]

There is no need to use a compound relation but rather to generate the opposite relation which is a total injection. However, I do not understand you use case, you cannot create a partial bijection for 1..1 → 0..1.

[Tomas]

For the practical purposes it is important that the generated relation is not only equivalent in the mathematical sense, but has also the same meaning as the original association. This is not true for the opposite relation as the domain and range are swapped. Therefore having a partial bijection would be beneficial as it would make Event-B models closer to the domain models (expressed using iUMLB Classdiagrams).

[Colin Snook]

Hi Tomas,

i agree the iUML-B generation is wrong for 1..1 --> 0..1 associations.. but i think it is generating a partial surjection. Anyway, please could you raise a ticket on the iUML-B tracker (which is also under the tickets menu here).

Thanks for spotting it

Colin

[Tomas]

You are correct, currently a parial surjection is generated (same as for 1..n → 0..1 association). See: #21 Wrong relation for the 1..1 → 0..1 associations

[Laurent Voisin]

Tomas, if you call your relation foo and want to generate "foo: S >+>> T" (partial bijection), you can instead generate "foo~ : T >-> S" which is strictly equivalent. There is no need to change the relation, just to generate the predicate on its converse.