diff --git a/RapportStage.tex b/RapportStage.tex
index 59e195c..e9b9256 100644
--- a/RapportStage.tex
+++ b/RapportStage.tex
@@ -258,11 +258,46 @@
 			Il peut sembler au premier abord qu'il manque à cette définition des \eng{test sets} une façon de définir la constructabilité d'un objet et certains nom d'attributs sans en préciser l'ordre. Cependant, avec un test simple, si l'on peut construire et accéder à un certain attribut \fj{field} sur un type \fj{C}, Si l'objet est constructible, c'est à dire qu'il existe une expression \fj{new C(new P1($e_1$),...,new Pn($e_n$))}, alors on peut créer pour chaque nom de classe \fj{Pk} des paramètres une sous-classe \fj{Pk\_k} (les \fj{Pk} pouvaient se confondre, mais les \fj{Pk\_k} sont tous distincts). Alors la construction suivante renverra une valeur de type \fj{PP\_k}, et on aura ainsi accès à l'indice du paramètre constructeur de l'attribut \fj{field}.
 			\[\fj{new C(new P1_1($e_1$),new P2_2($e_2$),...,new Pn_n($e_n$)).field}\]
 			
-			La troisième règle permet d'éviter les définitions implicites, en suivant la convention du papier original \cite{fjdef}. On peut dans tous les cas rajouter pour une classe \fj{C} non définie une ligne de la forme \fj{C \{\}}
+			La troisième règle permet d'éviter les définitions implicites, en suivant la convention du papier original \cite{fjdef}. On peut dans tous les cas rajouter pour une classe \fj{C} non définie une ligne de la forme \fj{C \{\}}.
+			
+			Nous allons aussi considérer uniquement les \eng{test interface} pour lesquelles il existe au moins une \eng{class table} les implémentant. Cela impose certaines règles, notamment que l'opération $\subclass$ induite puisse créer un bon ordre, mais d'autres contraintes plus complèxes à exprimer apparaîssent, nous n'allons pas chercher à les exprimer ici, mais vous trouverez des exemples de telles class tables en \autoref{fig:tiUnsolvable}
+			
+			\begin{figure}
+				\begin{center}
+					\begin{tabular}{ccc}
+						\begin{fjlisting}[width=.3\textwidth]
+							\begin{multicols}{2}
+							A \{\}\\
+							B \{\}\\
+							C \{\}\\
+							A <: B\\
+							B <: C\\
+							C <: A
+							\end{multicols}
+						\end{fjlisting}
+						&
+						\begin{fjlisting}[width=.2\textwidth]
+							A \{\}\\
+							B \{A f\}\\
+							C ()\\
+							C <: B
+						\end{fjlisting}
+						&
+						\begin{fjlisting}[width=.3\textwidth]
+							A \{\}\\
+							B \{A f\}\\
+							C (A f1, A f2)\\
+							C <: B
+						\end{fjlisting}
+					\end{tabular}
+				\end{center}
+				\label{fig:tiUnsolvable}
+				\caption{Exemples de \textit{test interfaces} implémentés par aucune \textit{class table}}
+			\end{figure}
 			
 			\paragraph{Opérateur d'implémentation}
 			
-			Nous allons maintenant définir un opérateur \enquote{d'implémentation} noté $\triangleright$, qui décrit l'idée qu'une class table $\mathcal{A}$ implémente une \enquote{test interface}, c'est à dire qu'elle vérifie toutes les contraintes que cette dernière impose. Les règles d'inférence définissant la relation sur les \eng{test interface rules} sont définies \autoref{fig:tiDefImpl}. On indique ensuite que $\mathcal{A} \triangleright \mathfrak{T}$ lorsque pour toute règle $TR\in\mathfrak{T}$, $\mathcal{A}\triangleright TR$ 
+			Nous allons maintenant définir un opérateur \enquote{d'implémentation} noté $\triangleright$, qui décrit l'idée qu'une class table $\mathcal{A}$ implémente une \enquote{test interface}, c'est à dire qu'elle vérifie toutes les contraintes que cette dernière impose. Les règles d'inférence définissant la relation sur les \eng{test interface rules} sont définies \autoref{fig:tiDefImpl}. On indique ensuite que $\mathcal{A} \triangleright \mathfrak{T}$ lorsque pour toute règle $TR\in\mathfrak{T}$, $\mathcal{A}\triangleright TR$.
 			
 			\begin{figure}
 				\ttfamily
@@ -271,20 +306,28 @@
 					\begin{center}
 					\begin{tabular}{cr}
 						\infer
-							{\mathcal{A} \triangleright \left[\fj{C : D m($\overline{\texttt{E}}$)}\right]}
-							{\operatorname{mtype}_\mathcal{A}(\fj{m},\fj{C}) = \fj{$\overline{\texttt{E}}$} \rightarrow \fj{D}}
+							{\mathcal{A} \triangleright \left[\fj{C : G m($\overline{\texttt{F}}$)}\right]}
+							{
+								\operatorname{mtype}_\mathcal{A}(\fj{m},\fj{C}) = \fj{$\overline{\texttt{E}}$} \rightarrow \fj{H}
+								\quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}}
+								\quad \fj{H}\subclass_\mathcal{A}\fj{G}
+							}	
 						&\newtag{\textrm{\textsc{(TRI-Meth)}}}{rule:tri:method}\\[1em]
 						
 						\infer
 							{\mathcal{A} \triangleright \left[\fj{ C \{ $\overline{\texttt{E}}\;\overline{\texttt{f}}$\}}\right]}
-							{\overline{\fj{E}}\;\overline{\fj{f}} \subset \operatorname{fields}_\mathcal{A}(C)}
+							{
+								\overline{\fj{F}}\;\overline{\fj{f}} \subset \operatorname{fields}_\mathcal{A}(C)
+								\quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}}
+							}
 						&\newtag{\textrm{\textsc{(TRI-Attr)}}}{rule:tri:attributes}\\[1em]
 						
 						\infer
 							{\mathcal{A} \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]}
 							{\exists \overline{\fj{f'}}\quad
 								\overline{\fj{f0}} = \overline{\fj{f}}+\overline{\fj{f'}} \land
-							\overline{\fj{E}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)
+							\overline{\fj{F}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)
+							\quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}}
 							}
 						&\newtag{\textrm{\textsc{(TRI-Cstr)}}}{rule:tri:constructor}\\[1em]
 						
@@ -300,7 +343,105 @@
 				\label{fig:tiDefImpl}
 			\end{figure}
 			
+			L'implémentation a été choisie la plus large possible, par exemple, une méthode \fj{C.m} typée par $\fj{Object} \rightarrow \fj{Number}$ implémentera une règle $\left[\fj{C : Int m(A)}\right]$. En effet, cette construction n'a pas pour objectif d'étudier le \emph{typage} de Featherweight Java, mais bien son \emph{fonctionnement}.
+			
 		\subsection{Définition du typage et d'un premier préordre}
+		
+			Maintenant, nous allons définir le typage d'expressions dans une \eng{test interface}. L'opérateur de typage sera noté $\Vdash$ pour la différencier de celle définie dans Featherweight Java, notée $\vdash$. Une expression sera sera typée sous une \eng{test interface} $\mathfrak{T}$, une \eng{class table} $\mathcal{A}$ et un environnement de typage $\Gamma$.
+			
+			Pour simplifier les définitions, nous allons rajouter une nouvelle application $\operatorname{construct}$ en plus des applications $\operatorname{fields}$, $\operatorname{mtype}$ et $\operatorname{mbody}$ qui sont définies dans le papier original, et que nous allons aussi surcharger. Maintenant, ces fonctions \enquote{recherchent} à la fois dans la \eng{class table} et dans la \eng{test interface}. Les définitions étendues sont présentées \autoref{fig:typops}.
+			
+			
+			\begin{figure}
+				\ttfamily
+				\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
+					\begin{center}
+					\begin{tabular}{c@{\hskip 6em}l}
+						\infer
+							{\operatorname{construct}(\fj{C}) = \overline{\fj{D}}}
+							{\fj{class C\{C($\overline{\texttt{D}}\;\overline{\texttt{f}}$)\{...\} ... \}}\in \mathcal{A}}
+						& \newtag{\textrm{\textsc{LTi-Cstr}}}{rule:lti-construct}\\[1em]
+						\infer
+							{\operatorname{construct}(\fj{C}) = \overline{\fj{D}}}
+							{\left[\fj{C($\overline{\texttt{D}}\;\overline{\texttt{?f}}$)}\right] \in \mathfrak{T}}
+						& \newtag{\textrm{\textsc{LCt-Cstr}}}{rule:lct-construct}\\[1em]
+						\infer
+							{\operatorname{fields}(\fj{C}) = \overline{\fj{D}}\;\overline{\fj{f}} + \bigcup_{C \subclass E}\operatorname{fields}(\fj{E})}
+							{\left[\fj{ C \{ $\overline{\texttt{D}}\;\overline{\texttt{f}}$\}}\right] \in \mathfrak{T}}
+						& \newtag{\textrm{\textsc{LTi-Attr}}}{rule:lti-fields}\\[1em]
+						\infer
+							{\operatorname{fields}(\fj{C}) = \underbrace{\overline{\fj{D}}\;\overline{\fj{f}}}_{\text{\textrm{\fj{f} défini}}} + \bigcup_{C \subclass E}\operatorname{fields}(\fj{E})}
+							{\left[\fj{ C ( $\overline{\texttt{D}}\;\overline{\texttt{f}}$)}\right] \in \mathfrak{T}}
+						& \newtag{\textrm{\textsc{LTi-AttrC}}}{rule:lti-fields2}\\[1.5em]
+						\infer
+							{\operatorname{fields}(\fj{C}) = \overline{\fj{D}}\;\overline{\fj{f}} + \bigcup_{C \subclass E}\operatorname{fields}(\fj{E})}
+							{\fj{class C \{$\overline{\texttt{D}}\;\overline{\texttt{f}}$; ...\}} \in \mathcal{A}}
+						& \newtag{\textrm{\textsc{LCt-Attr}}}{rule:lct-fields}\\[1em]
+						\infer
+							{\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}}
+							{\left[\fj{ C : E m( $\overline{\texttt{D}}$)}\right] \in \mathfrak{T}}
+						& \newtag{\textrm{\textsc{LTi-MethC}}}{rule:lti-method}\\[1em]
+						\infer
+							{\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}}
+							{\fj{class C \{...; E m($\overline{\texttt{D}}\;\overline{\texttt{x}}$)\}} \in \mathcal{A}}
+						& \newtag{\textrm{\textsc{LCt-Meth}}}{rule:lct-method}\\[1em]
+						\infer
+							{\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}}
+							{\operatorname{mtype}(\fj{m},\fj{C0}) = \overline{\fj{D}}\rightarrow\fj{E}\quad \fj{C} \subclass \fj{C0}}
+						& \newtag{\textrm{\textsc{LUp-Meth}}}{rule:lup-method}
+					\end{tabular}
+					\end{center}
+				\end{tcolorbox}
+				\rmfamily
+				$\subclass$ dénote ici la cloture transitive et réflexive de l'union des relations $<:$ sur $\mathfrak{T}$ et $extends$ dans $\mathcal{A}$.
+				
+				\caption{Opérateurs supplémentaires pour le typage}
+				\label{fig:typops}
+			\end{figure}
+		
+			Grâce à ces méthodes, nous pouvons réutiliser les règles de typage de Featherweight Java à l'identique, qui sont rappelées \autoref{fig:typti}. Nous avons enlevé la règle de typage \textsc{T-SCast} qui autorisait les casts \enquote{stupides}, entre deux types qui n'étaient pas parents l'un de l'autre.
+			
+			Nous vérifions aussi évidement la \eng{class table} $\mathcal{A}$, en vérifiant que le corps de chaque méthode est bien typé par le type attendu dans la méthode, que les champs de la \eng{class table} ne contredisent pas la \eng{test interface}. Les seules contradictions sont grammaticales si l'on a déjà vérifié que les applications $\operatorname{fields}$, $\operatorname{construct}$ et $\operatorname{mtype}$ n'étaient pas redéfinies ou ma définies.
+			
+			\begin{figure}
+				\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
+					\def\arraystretch{1.5}
+					\begin{tabular}{c@{\hskip 2em}l}
+						\infer
+							{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}
+							{\fj{x} \in \Gamma}
+						& \newtag{\textrm{\textsc{TI-Var}}}{rule:ti:variable}
+						\\[3ex]
+						\infer
+							{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{e.f} : \fj{E}}
+							{\mathfrak{T},\mathcal{A},\Gamma \Vdash e : \fj{C} \quad \fj{E}\;\fj{f} \in \operatorname{fields}(\fj{C})}
+						& \newtag{\textrm{\textsc{TI-Field}}}{rule:ti:field}
+						\\[3ex]
+						\infer
+							{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{e.m($\overline{\texttt{e'}}$)} : \fj{R}}
+							{\begin{array}{c}\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{e} : \fj{C} \quad \mathfrak{T},\mathcal{A},\Gamma \Vdash \overline{\fj{e'}} : \overline{\fj{E}} \\[-1.4ex] \overline{\fj{E}} \subclass \overline{\fj{G}} \quad \operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{G}} \rightarrow \fj{R} \end{array}}
+						& \newtag{\textrm{\textsc{TI-Invk}}}{rule:ti:invoke}
+						\\[3ex]
+						\infer
+							{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{new D(}\overline{\fj{e}}\fj{)} : \fj{D}}
+							{\mathfrak{T},\mathcal{A},\Gamma \Vdash \overline{\fj{e}} : \overline{\fj{E}} \quad \overline{\fj{E}} \subclass \overline{\fj{G}} \quad \operatorname{constructor}(\fj{D}) = \overline{\fj{G}}}
+						& \newtag{\textrm{\textsc{TI-New}}}{rule:ti:new}
+						\\[3ex]
+						\infer
+							{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{(D)e} : \fj{D}}
+							{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{e} : \fj{C} \quad \fj{C} \subclass \fj{D}}
+						& \newtag{\textrm{\textsc{TI-DCast}}}{rule:ti:downCast}
+						\\[3ex]
+						\infer
+							{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{(D)e} : \fj{D}}
+							{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{e} : \fj{C} \quad \fj{D} \subclass \fj{C} \quad \fj{C} \neq \fj{D}}
+						& \newtag{\textrm{\textsc{TI-UCast}}}{rule:ti:upCast}
+					\end{tabular}
+				\end{tcolorbox}
+				\caption{Typage des expressions avec une \eng{test interface} et une \eng{class table}}
+				\label{fig:typti}
+			\end{figure}
+			
 																						
 		\subsection{Renforcage de ce préordre avec les valeurs infinies}
 		
@@ -315,7 +456,7 @@
 	\section{Conclusion}
 	
 		
-	\newpage
+	\clearpage
 	\section{Bibliographie}
 	\printbibliography