Retour sur les hommes et les femmes

Toujours notre (en fait un exo traité par J.R. Abrial dans The B-Book, Cambridge University Press) exo Relations familiales.

On pouvait spécifier

SETS
SEXE = {masc, fem}
VARIABLES
aPourSexe, ...
INVARIANT
&
aPourSexe : PERSONNE +-> SEXE
DEFINITIONS
hommes == aPourSexe~[{masc}];
femmes == aPourSexe~[{fem}]