Ajout des notes du Mardi.

NotesStage.tex

@@ -54,6 +54,7 @@
 \tcbuselibrary{fitting}
 
 \newtcbox{\fjmaincodebox}{nobeforeafter,tcbox raise base, arc=0pt, outer arc=0pt, boxsep=0pt,left=2pt,right=2pt,top=2pt,bottom=2pt,boxrule=0pt,colback=white!85!black}
+\newtcbox{\fjind}{nobeforeafter,tcbox raise base, rounded corners=all, boxsep=0pt,left=1pt,right=1pt,top=1pt,bottom=1pt,boxrule=0pt,colback=white!52!orange}
 
 \newenvironment{fjlisting}[1][]
 {	
@@ -809,6 +810,10 @@
 					$$CT_1 \prec_{TS} CT_2 \iff \forall \left[\fj{Class : D meth(}\overline{\fj{E}}\fj{)}\right] \in TI \quad CT_1 \methprec{Class.meth} CT_2$$
 				\end{theorem}
 			
+				\subsubsection{Ajout de \fj{null} à Featherweight Java}
+				
+				%TODO décrire le choix de l'implémentation de null typé
+			
 				\subsection{Lemme des arguments finis}
 				
 				Pour un ensemble $\overline{CT}$, on note $\bigwedge \overline{CT}$ l'ensemble des valeurs qui sont valides dans chaque \textit{class table} de $\overline{CT}$.
@@ -923,8 +928,72 @@
 				
 				\subsubsection{Preuve du lemme}
 				
+				\subsection{Exemples montrant l'inutilité de l'équivalence sur les méthodes}
+					\begin{fjlisting}
+						\fjclass{IList}{\attr[IList]{next} \attr[Object]{obj}}{}
+						\fjclass{Static}{}{
+							\null\qquad IList gen()\{\newline
+							\fjind{$CT_1 - CT_1'$}\null\qquad \textbf{return} \lstinline[language=Java]{new IList(0,new IList(1,gen()))};\newline
+							\fjind{$CT_2 - CT_2'$}\null\qquad \textbf{return} \lstinline[language=Java]{new IList(0,gen())};\newline
+							\null\qquad\}\newline
+							
+							\method{Object}{evilNext}{Object x}{x.next}
+						}
+					\end{fjlisting}
+				
+					\begin{fjlisting}
+						\fjind{$TI_1 - TI_1'$}IList\{\}
+						
+						\fjind{$TI_2 - TI_2'$}IList\{Object obj\}
+						
+						\fjind{$TI_3 - TI_3'$}IList\{IList next, Object obj\}
+						
+						Static ()
+						
+						Static: IList gen()
+						
+						\fjind{$TI_1' - TI_2' - TI_3'$}Static: Object evilNext(Object)
+					\end{fjlisting}
+				
+					On a ici créé comme exemple quatre class tables ($CT_1,CT_1',CT_2,CT_2'$) et six test interfaces ($TI_1,TI_1',TI_2,TI_2',TI_3,TI_3'$) qui vérifient les équivalences suivantes:
+					
+					\begin{center}
+					\begin{tabular}{c|ccc}
+						& $TI_1$ & $TI_2$ & $TI_3$\\\hline
+						$CT_1/CT_2$&Oui&Non&Non\\
+						$CT_1'/CT_2'$&Oui&Oui&Non
+					\end{tabular}
+					\end{center}
+			
+					On peut montrer les «non» en utilisant les expressions $e=\fj{new Static().gen().next.obj}$ et $e'=\fj{new Static().evilNext(new Static().get()).obj}$.
+					
+					Aussi, dans ces exemples, les \textit{class tables} $CT_1/CT_2$ et $CT_1'/CT_2'$ sont équivalents sous l'angle de toutes les méthodes des \textit{test interfaces}. Et pourtant ne sont pas équivalentes sous certaines.
+					
+					On pourrait vouloir palier ce problème en comparant les méthodes sur les valeurs «infinies» qu'elles produisent, mais de la même façon, les \textit{class tables} ne sont alors jamais équivalentes sous l'angle de \fj{Static.get}, mais elles sont parfois équivalentes (comme sous $TI_1$).
+					
+					L'exemple $TI_2$ et $TI_2'$ nous indique qu'on ne peut pas se contenter de comparer les valeurs de sortie sur les fields laissés apparents par la test interface.
+					
+				\subsection{Tentative de limitation des class tables}
+					Nous allons dans cette section essayer de prouver le théorème avec plusieurs class tables en les empêchant d'utiliser des fields non présents dans la test interface.
+					%TODO here
+				\subsection{Petites variations dans la class table}
+					Nous allons dans cette section essayer d'utiliser le lemme des arguments finis dans une seule class table pour essayer de la «modifier» en une class table équivalente en modifiant uniquement le corps d'une seule méthode (ou d'un groupe mutuellement récursif).
+					%TODO here
+					
 	\newpage
 	\bibliography{NotesStage}
 	\bibliographystyle{ieeetr}
 	
+	\newpage
+	
+	\appendix
+	
+	\section{Classes et Notations en FeatherweightJava}
+		\subsection{La classe Static}
+			%TODO here
+		\subsection{Les booléens}
+			%TODO here
+		\subsection{Les entiers}
+			%TODO here
+	
 \end{document}