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}]

Les relations familiales sur l'Atelier B

J'ai proposé aux étudiants d'utiliser l'Atelier B. Un (au moins, ouf ! je n'ai pas perdu mon temps) a entré la spec et ses définitions. Il a ajouté l'initialisation. Il a pu "passer le type check". Bien. Mais l'Atelier n'a pu prouver l'initialisation.
Lecture de l'obligation de preuve (Proof Obligation, PO) :
Invariant & Initialisation => {} <: PERSONNE
L'Atelier B écrit même l'invariant et l'initialisation. Partie de l'invariant on trouve que PERSONNE est un ensemble non vide et fini. Il dit tout !

Où est l'erreur ?

SETS
PERSONNE
...
hommes <: PERSONNE &
femmes <: PERSONNE &
hommes \/ femmes = PERSONNE &
hommes /\ femmes = {}

Or dans l'initialisation, on trouve :
hommes := {} || femmes := {}
ce qui fait que
hommes \/ femmes = {}
et que PERSONNE = {}

Mais l'Atelier B connaît la définition des SETS (ensembles finis et NON VIDES)

Il ne peut prouver que PERSONNE est à la fois VIDE et NON VIDE.

Ce n'est pas négociable !

Alors monsieur, on fait quoi ?

SETS
PERSONNE
...
humains <: PERSONNE &
hommes <: PERSONNE &
hommes <: humains &
femmes <: PERSONNE &
femmes <: humains &
hommes \/ femmes = humains &
hommes /\ femmes = {}