Modification du début du vendredi

RapportStage.tex

@@ -441,6 +441,37 @@
 				\caption{Typage des expressions avec une \eng{test interface} et une \eng{class table}}
 				\label{fig:typti}
 			\end{figure}
+		
+			Nous allons maintinant vérifier la définition de cette opération de typage $\Vdash$ en démontrant le théorème suivant:
+			
+			\begin{theorem}
+				Soit une \eng{test interface} $\mathfrak{T}$, une \eng{class table} $\mathcal{A}$ et un test $(\mathcal{C},e)$ vérifiant
+				\begin{itemize}
+					\item $\mathcal{A} \triangleright \mathfrak{T}$
+					\item $\mathcal{C} \text{\textsc{ OK in }} \mathfrak{T}$
+					\item $\mathfrak{T},\mathcal{C} \Vdash e : \fj{D}$
+				\end{itemize}
+				
+				Alors il existe \fj{C} tel que $\mathcal{A} \oplus \mathcal{C} \vdash e : \fj{C}$ et $\fj{C} \subclass \fj{D}$.
+				
+				Cette dernière condition est nécessaire à cause de la tolérance de l'opérateur $\triangleright$.
+			\end{theorem}
+		
+			Ce théorème se prouve par induction sur la preuve de $\mathfrak{T},\mathcal{C} \Vdash e : \fj{D}$. La preuve est donnée en \autoref{anx:proofTyptyp}.
+			
+			On peut donc définir un préordre sur les \eng{class tables} de la manière suivante.
+			
+			\begin{definition}
+				Soit une \eng{test interface} $\mathfrak{T}$.
+				
+				Soit deux \eng{class tables} $\mathcal{A}$ et $\mathcal{B}$ qui implémentent toutes deux $\mathfrak{T}$
+				
+				\[\mathcal{A} \prec \mathcal{B} \ssi \forall (\mathcal{C},e) \left|\begin{array}{l}
+					\mathcal{C} \text{\textsc{ OK in }} \mathfrak{T}\\
+					\mathfrak{T},\mathcal{C} \Vdash e : \fj{D}\\
+					\mathcal{A}\oplus\mathcal{C} \Downarrow v
+				\end{array}\right. \implies \mathcal{B}\oplus\mathcal{C}\Downarrow v\]
+			\end{definition}
 			
 																						
 		\subsection{Renforcage de ce préordre avec les valeurs infinies}
@@ -491,5 +522,8 @@
 		On ajoute aussi la notation des nombres :
 		\[\fj{0} = \fj{new Int()}\]
 		\[n = \fj{new SInt(n-1)}\]
+		
+	\section{Preuve du théorème de cohérence du typage des \eng{test interfaces}}
+	\label{anx:proofTyptyp}
 	
 \end{document}