MACHINE
        TP1LapinWinnie
SETS
        ETUDIANT ; SPORT
ABSTRACT_VARIABLES
        etudiant , sport , pratique
INVARIANT
        etudiant <: ETUDIANT &
        sport <: SPORT &
        pratique : etudiant --> sport
INITIALISATION
        etudiant , sport , pratique := {} , {} , {}
OPERATIONS
ajout_etudiant ( ee , ss ) =
        PRE
                ee : ETUDIANT - etudiant &
                ss : sport
        THEN
                etudiant := etudiant \/ { ee } ||
                pratique := pratique \/ { ee |-> ss }
        END ;
ajout_sport ( ss ) =
        PRE
                ss : SPORT - sport
        THEN
                sport := sport \/ { ss }
        END ;

supprimer_etudiant ( ee ) =
        PRE
                ee : etudiant
        THEN
                pratique := { ee } <<| pratique ||
                etudiant := etudiant - { ee }
        END ;
supprimer_sport ( ss ) =
        PRE
                ss : sport &
                ss /: ran ( pratique )
        THEN
                sport := sport - { ss }
        END ;
ss <-- Quel_sport ( ee ) =
        PRE
                ee : dom ( pratique )
        THEN
                ss := pratique ( ee )
        END ;
ee <-- Quels_etudiants ( ss ) =
        PRE
                ss : ran ( pratique )
        THEN
                ee := pratique ~ ( ss )
        END
END