L'amour des escargots, une spécification en B à passer à l'Atelier B !

L'amour des escargots

"Chez les escargots, un même individu possède les deux appareils reproducteurs mâle et femelle. Ce qui ne signifie pas que l'individu se féconde lui-même : tantôt femelle, tantôt mâle, il aura toujours recours à l'autre pour accomplir la fécondation. Cet hermaphrodisme vrai peut se rencontrer exceptionnellement chez l'homme qui présente plus fréquemment des cas de pseudo-hermaphrodisme dans lesquels l'apparence somatique d'un sexe recouvre la présence inexprimée de l'autre." (Luc Ferry, Jean-Didier Vincent, Qu'est-ce que l'homme, sur les fondamentaux de la biologie et de la philosophie, Odile Jacob, 2000, ISBN : 2-7381-0785-0)

MACHINE

                LesEscargots

SETS

                ESCARGOT; SEXE = {masc, fem}; ETAT = {vivant, dcd}

VARIABLES

escargots, étatEscargot, sexeDe, accouplements

DEFINITIONS

                mâles == sexeDe~ [{masc}];

                femelles == sexeDe~ [{fem}];

                couples == (mâles * femelles)

INVARIANT

                escargots <: amp="" escargot="" o:p="">

                étatEscargot : escargots --> ETAT &

                sexeDe : escargots --> SEXE &

                accouplements : seq (couples)

INITIALISATION

                 escargots, étatEscargot, sexeDe, accouplements := {}, {}, {}

OPERATIONS

                naissance (sex) =

                               PRE

                                               sex : SEXE & ESCARGOT - escargots /= {}

                               THEN

                                               ANY esc WHERE esc : (ESCARGOT - escargots)

                                                               THEN escargots := escargots \/ {esc} || sexeDe (esc) := sex END

                               END;

                                              

                changementDeSexe (esc) =

                               PRE       

                                               esc : escargots &

                                               étatEscargot (esc) = vivant

                               THEN

                                               IF sexeDe (esc) = masc THEN sexeDe(esc) := fem ELSE sexeDe (esc) := masc END

                               END;

                coït (mal, fem) =

                               PRE       

                                               étatEscargot (mal) = vivant & étatEscargot (fem) = vivant &

                                               mal : mâles & fem : femelles

                               THEN

                                               accouplements := accouplements <- mal=""> fem)

                               END

END