TP1LapinWinnie
Documentation de projet
i1b08a
6 Decembre 2006

1.	INTRODUCTION
La documentation est effectuée sur le projet : TP1LapinWinnie.

2.	STRUCTURE GENERALE
2.1.	Introduction

2.2.	Graphe de dépendance

2.3.	Métrique
Project status
 COMPONENT   	 TC   	 POG   	 Obv   	 nPO   	 nUn   	 %Pr   	 B0C   	  C    	 Ada   	 C++   	 HIA   	
 TP1LapinWinnie   	OK  	OK  	26  	11  	0  	100  	-  	 	 	 	 	
 TOTAL   	OK  	OK  	26  	11  	0  	100  	-  	OK  	OK  	OK  	OK  	

3.	DESCRIPTION DES COMPOSANTS
3.1.	Composant TP1LapinWinnie
3.1.1.	Présentation
Le composant traité dans ce paragraphe est : TP1LapinWinnie.

3.1.2.	Métrique
	TP1LapinWinnie AutoProved /hometu/etudiants/i1b08a/Romain/agl/TP1LapinWinnie/spec/TP1LapinWinnie.mch

     	 NbObv   	 NbPO   	 NbPRi   	 NbPRa   	 NbUn   	 %Pr   	
   Initialisation   	0  	3  	0  	3  	0  	100  	
   ajout_etudiant   	4  	1  	0  	1  	0  	100  	
   ajout_sport   	4  	1  	0  	1  	0  	100  	
   ajout_pratique   	3  	1  	0  	1  	0  	100  	
   supprimer_etudiant   	2  	2  	0  	2  	0  	100  	
   supprimer_sport   	2  	2  	0  	2  	0  	100  	
   supprimer_pratique   	3  	1  	0  	1  	0  	100  	
   Quel_sport   	4  	0  	0  	0  	0  	100  	
   Quels_etudiants   	4  	0  	0  	0  	0  	100  	
 TP1LapinWinnie   	26  	11  	0  	11  	0  	100  	

3.1.3.	Règles ajoutées à la preuve
Fichier /hometu/etudiants/i1b08a/Romain/agl/TP1LapinWinnie/bdp/TP1LapinWinnie.pmm non existant.

3.1.4.	Source B
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 a 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-1(ss)
	END
END

4.	DICTIONNAIRE	
...		a
	...	
		ajout_etudiant
		
defined in 		TP1LapinWinnie.mch
		
		operation name
		
		ajout_pratique
		
defined in 		TP1LapinWinnie.mch
		
		operation name
		
		ajout_sport
		
defined in 		TP1LapinWinnie.mch
		
		operation name
		
...		e
	...	
		ee
		
defined in 		TP1LapinWinnie.mch
		
		operation output parameter
		
modified in 		
TP1LapinWinnie.mch (Quels_etudiants)
		
		ee
		
defined in 		TP1LapinWinnie.mch
		
		operation input parameter
		
used in 		TP1LapinWinnie.mch (Quel_sport)
		
used in 		TP1LapinWinnie.mch (Quel_sport)
		
		ee
		
defined in 		TP1LapinWinnie.mch
		
		operation input parameter
		
used in 		TP1LapinWinnie.mch (supprimer_pratique)
		
used in 		TP1LapinWinnie.mch (supprimer_pratique)
		
		ee
		
defined in 		TP1LapinWinnie.mch
		
		operation input parameter
		
used in 		TP1LapinWinnie.mch (supprimer_etudiant)
		
used in 		TP1LapinWinnie.mch (supprimer_etudiant)
		
used in 		TP1LapinWinnie.mch (supprimer_etudiant)
		
		ee
		
defined in 		TP1LapinWinnie.mch
		
		operation input parameter
		
used in 		TP1LapinWinnie.mch (ajout_pratique)
		
used in 		TP1LapinWinnie.mch (ajout_pratique)
		
used in 		TP1LapinWinnie.mch (ajout_pratique)
		
		ee
		
defined in 		TP1LapinWinnie.mch
		
		operation input parameter
		
used in 		TP1LapinWinnie.mch (ajout_etudiant)
		
used in 		TP1LapinWinnie.mch (ajout_etudiant)
		
		etudiant
		
defined in 		TP1LapinWinnie.mch
		
		abstract variable
		
used in 		TP1LapinWinnie.mch (INVARIANT)
		
used in 		TP1LapinWinnie.mch (INVARIANT)
		
used in 		TP1LapinWinnie.mch (ajout_etudiant)
		
used in 		TP1LapinWinnie.mch (ajout_etudiant)
		
used in 		TP1LapinWinnie.mch (ajout_pratique)
		
used in 		TP1LapinWinnie.mch (supprimer_etudiant)
		
used in 		TP1LapinWinnie.mch (supprimer_etudiant)
		
modified in 		TP1LapinWinnie.mch (INITIALISATION)
		
modified in 		TP1LapinWinnie.mch (ajout_etudiant)
		
modified in 		TP1LapinWinnie.mch (supprimer_etudiant)
		
...		E
	...	
		ETUDIANT
		
defined in 		TP1LapinWinnie.mch
		
		set
		
used in 		TP1LapinWinnie.mch (INVARIANT)
		
used in 		TP1LapinWinnie.mch (ajout_etudiant)
		
...		I
	...	
		INITIALISATION
		
defined in 		TP1LapinWinnie.mch
		
		builtin
		
...		p
	...	
		pratique
		
defined in 		TP1LapinWinnie.mch
		
		abstract variable
		
used in 		TP1LapinWinnie.mch (INVARIANT)
		
used in 		TP1LapinWinnie.mch (ajout_pratique)
		
used in 		TP1LapinWinnie.mch (ajout_pratique)
		
used in 		TP1LapinWinnie.mch (supprimer_etudiant)
		
used in 		TP1LapinWinnie.mch (supprimer_sport)
		
used in 		TP1LapinWinnie.mch (supprimer_pratique)
		
used in 		TP1LapinWinnie.mch (supprimer_pratique)
		
used in 		TP1LapinWinnie.mch (Quel_sport)
		
used in 		TP1LapinWinnie.mch (Quel_sport)
		
used in 		TP1LapinWinnie.mch (Quels_etudiants)
		
used in 		TP1LapinWinnie.mch (Quels_etudiants)
		
modified in 		TP1LapinWinnie.mch (INITIALISATION)
		
modified in 		TP1LapinWinnie.mch (ajout_pratique)
		
modified in 		TP1LapinWinnie.mch (supprimer_pratique)
		
...		Q
	...	
		Quel_sport
		
defined in 		TP1LapinWinnie.mch
		
		operation name
		
		Quels_etudiants
		
defined in 		TP1LapinWinnie.mch
		
		operation name
		
...		s
	...	
		sport
		
defined in 		TP1LapinWinnie.mch
		
		abstract variable
		
used in 		TP1LapinWinnie.mch (INVARIANT)
		
used in 		TP1LapinWinnie.mch (INVARIANT)
		
used in 		TP1LapinWinnie.mch (ajout_sport)
		
used in 		TP1LapinWinnie.mch (ajout_sport)
		
used in 		TP1LapinWinnie.mch (ajout_pratique)
		
used in 		TP1LapinWinnie.mch (supprimer_sport)
		
used in 		TP1LapinWinnie.mch (supprimer_sport)
		
modified in 		TP1LapinWinnie.mch (INITIALISATION)
		
modified in 		TP1LapinWinnie.mch (ajout_sport)
		
modified in 		TP1LapinWinnie.mch (supprimer_sport)
		
...		S
	...	
		SPORT
		
defined in 		TP1LapinWinnie.mch
		
		set
		
used in 		TP1LapinWinnie.mch (INVARIANT)
		
used in 		TP1LapinWinnie.mch (ajout_sport)
		
...		s
	...	
		ss
		
defined in 		TP1LapinWinnie.mch
		
		operation input parameter
		
used in 		TP1LapinWinnie.mch (Quels_etudiants)
		
used in 		TP1LapinWinnie.mch (Quels_etudiants)
		
		ss
		
defined in 		TP1LapinWinnie.mch
		
		operation output parameter
		
modified in 		TP1LapinWinnie.mch (Quel_sport)
		
		ss
		
defined in 		TP1LapinWinnie.mch
		
		operation input parameter
		
used in 		TP1LapinWinnie.mch (supprimer_sport)
		
used in 		TP1LapinWinnie.mch (supprimer_sport)
		
used in 		TP1LapinWinnie.mch (supprimer_sport)
		
		ss
		
defined in 		TP1LapinWinnie.mch
		
		operation input parameter
		
used in 		TP1LapinWinnie.mch (ajout_pratique)
		
used in 		TP1LapinWinnie.mch (ajout_pratique)
		
		ss
		
defined in 		TP1LapinWinnie.mch
		
		operation input parameter
		
used in 		TP1LapinWinnie.mch (ajout_sport)
		
used in 		TP1LapinWinnie.mch (ajout_sport)
		
		supprimer_etudiant
		
defined in 		TP1LapinWinnie.mch
		
		operation name
		
		supprimer_pratique
		
defined in 		TP1LapinWinnie.mch
		
		operation name
		
		supprimer_sport
		
defined in 		TP1LapinWinnie.mch
		
		operation name
		
...		T
	...	
		TP1LapinWinnie
		
defined in 		TP1LapinWinnie.mch
		
		machine name