mardi 20 janvier 2015

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

Aucun commentaire:

 
Site Meter