MACHINE
	TP1LapinWinnie
SETS
	ETUDIANT;SPORT
VARIABLES
	etudiant,sport,pratique
INVARIANT
	etudiant <: ETUDIANT &
	sport <: SPORT &
	pratique : etudiant +-> sport
INITIALISATION
	etudiant,sport,pratique := {},{},{}
OPERATIONS
ajout_etudiant(ee)=
	PRE
		ee : ETUDIANT - etudiant
	THEN
		etudiant := etudiant \/ {ee}
	END;
ajout_sport(ss)=
	PRE
		ss : SPORT - sport	 
	THEN
		sport := sport \/ {ss}
	END;
ajout_pratique(ee,ss)=
	PRE
		ee : etudiant &
		ss: sport &
		ee /: dom(pratique)
	THEN
		pratique := pratique \/ {ee |-> ss}
	END;
supprimer_etudiant(ee)=
	PRE
		ee : etudiant &
		ee /: dom(pratique)
	THEN
		etudiant := etudiant - {ee}
	END;
supprimer_sport(ss)=
	PRE
		ss : sport &
		ss /: ran(pratique)
	THEN
		sport := sport - {ss}
	END;
supprimer_pratique(ee)=
	PRE
		ee : dom(pratique)
	THEN
		pratique := {ee} <<|pratique
	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