\documentclass[10pt,a4paper,draft]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{bbm}
\usepackage{stmaryrd}
\usepackage[french]{babel}
\usepackage{csquotes}
\usepackage{listings}
\usepackage{lstautogobble}
\usepackage{algorithm2e}
\usepackage{svg}
\usepackage{tikz}
\usepackage{multirow}
\usepackage{multicol}
\usepackage{tcolorbox}
\usepackage{mdframed}
\usepackage{proof}
\usepackage[lighttt]{lmodern}
\usetikzlibrary{shapes.geometric}

\newcommand{\pgrph}{\P}
\newcommand{\hsep}{\vspace{.2cm}\centerline{\rule{0.8\linewidth}{.05pt}}\vspace{.4cm}}
\renewcommand{\P}{\mathbb{P}}
\newcommand{\E}{\mathbb{E}}
\newcommand{\1}{\scalebox{1.2}{$\mathbbm{1}$}}
\newcommand{\floor}[1]{\left\lfloor#1\right\rfloor}
\newcommand{\littleO}{o}
\newcommand{\bigO}{\mathcal{O}}
\newcommand{\longdash}{\:\textrm{---}\:}
\newcommand{\methprec}[1]{\prec\mkern-8mu\left[\fj{#1}\right]}
\newcommand\hole{\left[\raisebox{-0.25ex}{\scalebox{1.2}{$\cdot$}}\right]}



\makeatletter
\newcommand\newtag[2]{#1\def\@currentlabel{#1}\label{#2}}
\makeatother

\DeclareMathOperator{\varnull}{varnull}
\DeclareMathOperator{\nextop}{next}
\DeclareMathOperator{\new}{\text{\textbf{new}}}
\DeclareMathOperator{\CT}{CT}
\DeclareRobustCommand{\leftsarrow}{\text{\reflectbox{$\;\rightarrow^*$}}}
\let\rbar\bar
\let\bar\overline
\newcommand\subclass{<:}

\newcommand{\ssi}{\quad\text{\underline{ssi}}\quad}

\newtheorem{theorem}{Théorème}
\newtheorem{definition}{Definition}
\newtheorem{property}{Propriété}

\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][]
{	
	%\begin{center}
	\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!96!black,#1]
		\ttfamily
}{
	 \end{tcolorbox}
	%\end{center}
}
\newcommand{\ifnullthenelse}[3]{
\ifnum\value{#1}=0
#2
\else
#3
\fi
}

\makeatletter
\newcommand*\idstyle{%
	\expandafter\id@style\the\lst@token\relax
}
\def\id@style#1#2\relax{%
	\ifcat#1\relax\else
	\ifnum`#1=\lccode`#1%
	\ttfamily\slshape
	\fi
	\fi
}
\makeatother

\lstdefinelanguage{FeatherweightJava}{
	keywords = {new, this},
	basicstyle=\ttfamily,
	identifierstyle=\idstyle,
	mathescape=true
}
\newcommand{\fj}[1]{\text{\textnormal{\lstinline[language=FeatherweightJava,mathescape=true]|#1|}}}

\newcounter{fjargcount}
\newcommand{\fjparamattributes}[2][Object]{
	\null\qquad #1 #2;\newline
}
\newcommand{\printcomma}{,}
\newcommand{\fjparamconstparameters}[2][Object]{
	\ifnullthenelse{fjargcount}{}{,} \text{#1} \;\text{#2}
	\stepcounter{fjargcount}
}
\newcommand{\fjparamconstassign}[2][Object]{
	\null\qquad\qquad \textbf{this}.#2 = #2;\newline
}
\newcommand{\method}[4]{
	\null\qquad #1 #2(#3)\{\newline
		\null\qquad\qquad \textbf{return} \lstinline[language=Java]{#4};\newline
	\null\qquad\}\newline
}

\newcommand{\fjmain}[1]{
	\noindent\fjmaincodebox{\lstinline[language=Java]{#1}}
}

% Premier argument: Nom de la classe
% Second argument: \attr{x}[Object] \attr{attr}[A]
% Troisième argument \method{C}{metname}{Object w, B par}{((D)obj).apply(par)} plusieurs fois
% Argument optionnel: la classe que l'on extend
\newcommand{\fjclass}[4][Object]{%
	\noindent \textbf{class} #2 \textbf{extends} #1 \{\newline
		% Attributs
		\let\attr\fjparamattributes
		#3
		% Constructeur
		\let\attr\fjparamconstparameters
		\setcounter{fjargcount}{0}
		\null\qquad #2(\ifx&#3&\else $#3$\fi) \{\newline
			\null\qquad\qquad \textbf{super}();\newline
			\let\attr\fjparamconstassign%
			#3
		\null\qquad\}\\
		% Méthodes
		#4
	\}\newline
}

\title{Notes de Stage}
\author{Samy Avrillon}

\begin{document}

	\maketitle
	
	\hsep
	
	\tableofcontents
	
	\newpage
	
	\section{Tentatives de définition d'un contexte sur Featherweight Java}
	
	\subsection{Définitions et notations}
	
	On se base sur les notations issues de la définition du Featherweight Java \cite{fjdef}.
	Donc $e$ est la grammaire des expressions, $L$ la grammaire des classes, $\bar{x}$ dénote une suite potentiellement vide d'élément de type $x$, \verb*|<:| désigne la relation de sous-typage, $\longrightarrow$ désigne l'opérateur de réduction.
	
	Un programme Featherweight Java est composé de deux parties: La première est une liste de définitons de classes, que le papier originel appelait \textit{collection of class definitions}, mais que nous appellerons plutôt \textit{Class Tables} \cite{yingfei_2014}. La seconde est une expression à évaluer (on peut la voir comme le body d'une fonction \fj{main} d'un programmme Java). Nous allons donc considérer qu'un programme FeatherweightJava $P$ est un couple $(\bar{L},e)$, et l'on notera $\CT(P) = \bar{L}$ et $e_P = e$ lorsque nous manipulerons plusieurs programmes.
	
	On note la gramaire à un trou $h$ :
		$$h := \fj{x} | \fj{[.]} | \fj{h.f} | \fj{h.m(}\bar{\fj{e}}\fj{)} | \fj{e.m(}\bar{\fj{e}}\fj{,h,}\bar{\fj{e}}\fj{)} | \fj{new C(}\bar{\fj{e}}\fj{,h,}\bar{\fj{e}}) | \fj{(C) h} $$
		
	On pourra souvent se ramener à la grammaire à plusieurs trous $\tilde{h}$ :
		$$\tilde{h} := x | [.] | \tilde{h}.f | \tilde{h}.m(\bar{\tilde{h}}) | \new C(\bar{\tilde{h}}) | (C) h | e $$
	
	Puis on ajoute l'opération de \textit{remplissage} $h[g]$ pour $h$ expression à trou et $g$ expression classique, définie récursivement:
	
	\begin{align*}
		x[g] &= x\\
		[.][g] &= g\\
		(h.f)[g] &= h[g].f\\
		(h.m(\bar{e}))[g] &= h[g].m(\bar{e})\\
		(e.m(\bar{e},h,\bar{e}))[g] &= e.m(\bar{e},h[g],\bar{e})\\
		(\new C(\bar{e},h,\bar{e}))[g] &= \new C(\bar{e},h[g],\bar{e})\\
		((C) h)[g] &= (C) h[g]
	\end{align*}
		
	\subsection{Première définition naïve}
		
		La première définition, à l'instar de celle donnée pour le $\pi$-calcul pourrait ressembler à ça:
		
		Un contexte est un élément de $h$.
		
		Alors l'interprétation d'un programme dans un contexte est $C[P] = (CL(P), h[e])$
		
		Le problème, c'est que cette version des contextes est peu puissante. En effet, puisque nous avons juste des expressions, nous limitons à l'utilisation de la class table du programme. Et ça nous enlève tout une batterie de tests que l'on aurait pu autrement pû utiliser.
		
		\subsubsection{Problème du trou dégénéré}
		
			\begin{theorem}
				Si la class table du programme testé permet de créer un trou dégénéré, c'est à dire un contexte à trou te que pour toute expression $e$, il existe une expression trouée $h$ telle que $\forall p \; h[p] \rightarrow^* e$.
				
				Alors $P\leqslant Q \implies \CT(P) \subseteq \CT(Q)$
			\end{theorem}
			
			Un exemple classique de contexte ayant un trou dégénéré est dans un programme dont la class table contient la classe \fj{Pair} suivante:
			\begin{fjlisting}	
				\fjclass{Pair}{
					\attr{fst}
					\attr{snd}
				}{}
			\end{fjlisting}
		
			Alors si on considère le contexte $C$ = \fj{new Pair(e,[.]).fst} pour toute expression \fj{e}. on aura $C[p]$ = \fj{new Pair(e,p).fst} $\rightarrow^*$ \fj{e}.
			
			Le théorème se prouve en construisant des expressions qui dépendent explicitement de la structure des classes: \fj{new A()} ne se résout en une valeur seulement si la class table contient une classe A sans attributs, \fj{new C(new A(), new B()).m(new A())} impose les attributs de C ainsi que l'existence d'une méthode m prenant un argument A, et cætera.
			
			\paragraph{C'est un problème} par ce que deux programmes ne peuvent pas utiliser des classes internes différentes. Par exemple, un programme de tri d'un liste qui utiliserait une classe \fj{Map} et un autre qui utiliserait \fj{Tree} ne pourraient être comparés, quand bien même leurs fonctionnement pourrait paraître similaire à nos yeux. On a le même problème sur le nom des classes «internes».
			
			\paragraph{Ce n'est pas un problème} car sans notion d'access control, un utilisateur peut utiliser toutes les classes internes. Donc la structure interne du programme a de l'importance sur ce qu'on peut modifier du programme.
			
			\paragraph{Une solution} serait de redéfinir le préordre pour ne considérer que les classes sur les parties des class tables qui sont en commun. Par contre, on ne résout pas le problème de la dépendance au nom, si deux programmes définissent une meme classe \fj{MaClasse}, doit-on imposer pour les programmes soient équivalents que les deux «implémentations» le soient ?
			
			\paragraph{Une autre solution} pourrait être de comparer uniquement avec des contextes qui «utiliseraient» (notion à définir) une partie spécifique de la Class Table qui serait alors comparée. On retrouve l'idée d'interface présente dans le Java complet (ou d'autres versions de FJ \cite{liquori_fjInterfaces}).
			
			\paragraph{Une dernière solution} serait d'ailleurs d'ajouter les access control au featherweight java, c'est à dire de pouvoir noter les classes comme  \fj{public}, \fj{private}, \fj{package-protected} ou \fj{protected}, en restreignant directement le typage des sexpressions.
		
		
	\subsection{Seconde définiton naïve}
	
		Un contexte est une class table $\bar{L}$ et un contexte à trou $h$.
		
		Alors $C[P] = (\CT(P) + \bar{L}', h[\bar{L}'/\bar{L}][e_P])$ où $\bar{L}'$ est une class table $\alpha$-convertible en $\bar{L}$ tel qu'aucun nom de classe ne coïncide avec ceux de $\CT(P)$.
		
		On définit un $\alpha$-renommage de classe dans une class table comme l'opération de changer un nom de classe en un autre nom, en changant toutes les occurences de ce nom ($\new C(\dots)$, $(C) e$, \textbf{extends}, définition d'attributs, de paramètres de méthodes et de type de retour de méthode), en s'assurant que le nom n'était pas utilisé.
		
		Deux class tables sont alors $\alpha$-convertibles si on peut passer de l'une à l'autre avec un nombre fini d'$\alpha$-renommages, à l'instar de ce qui est fait dans le $\pi$-calcul \cite{picalcul_sangiorgi}.
		
		On a alors forcément un trou dégénéré (parce que on peut ajouter la classe Paire nous-même)
		
	\subsection{Troisième définition naïve}
		Un contexte est une class table $\bar{L}$ et une expression $e_C$.
		
		Alors $C[P] = (\CT(P) + \bar{L}' + Main'', e_C[CT'/CT][Main''/Main])$ où $\bar{L}'$ est obtenu de la même manière que précédement et $Main$ est la class table suivante:
		
		\begin{fjlisting}
			\fjclass{Main}{}{
				\method{Object}{main}{Object $\bar{x}$}{e}
			}
		\end{fjlisting}
	
		où $\bar{x}$ est l'ensemble des variable libres de $e_P$.
		
		On sent que l'on veut tester l'utilisation d'une méthode plutôt que d'une expression, ce qui est en adéquation avec le paradigme orienté objet, mais ces contextes restent toujours aussi faillibles.
		
		On peut forcer un peu plus l'utilisation du main, en construisant le contexte dans sa version 3.1:
		$C$ = $\bar{L}$ et $\bar{e_C}$ interprété en 
		$$C[P] = (\CT(P) + \bar{L}' + Main'', \new Main().main(\bar{e_C[CT'/CT][Main''/Main])})$$
		
	\subsection{Quatrième définition naïve}
		La première méthode naïve est utile pour faire des équivalences entre des programmes de même class table. Mais on pourrait faire mieux.
		
		On définit déjà un préordre sur les class tables:
		
		$$ CTA \prec CTB \iff \forall e \forall v (CTA,e)\Downarrow v \implies (CTB,e)\Downarrow v$$
		
		On peut ainsi utiliser la méthode du contexte pour créer un pré-ordre sur les programmes:
		
		$$ P \prec Q \iff \CT(P) \prec \CT(Q) \text{ et } \forall h (\CT(P),h[e_P])\Downarrow v \implies (\CT(Q), h[e_Q])\Downarrow v$$
		
		On peut aussi encore augmenter le contexte en le définissant avec sa propre class table:
		
		Un contexte $C$ est alors une CT $\bar{L}$ et une expression trouée $h$.
		
		L'interpretation est alors $C[P] = (CT(C),h[e_P])$ si $\CT(P) \prec \CT(C)$. On dit alors que $C$ convient à $P$.
		
		On a alors un nouveau pré-ordre sur les programmes:
		
		$$P\prec Q \iff \forall C (C \text{ convient à } P\text{ et }C \text{ convient à } Q) \implies \left(\forall v\; C[P]\Downarrow v \implies C[Q]\Downarrow v\right)$$
		
		\paragraph{Gros problème cependant} si les deux programmes comparées n'ont aucun contexte qui leur convienne à tous les deux. On est alors bloqués dans une situation d'universalité du vide. Par exemple les deux class table suivantes, notées $CT_A$ et $CT_B$:
		
		\noindent
		\begin{minipage}{.5\textwidth}
			\begin{fjlisting}
				\fjclass{A}{}{}
				\fjclass{B}{}{}
				\fjclass{Get}{
					\attr[A]{a}
					\attr[B]{b}
				}{
					\method{Object}{get}{}{this.a}
				}
			\end{fjlisting}
		\end{minipage}
		\begin{minipage}{.5\textwidth}
			\begin{fjlisting}
				\fjclass{A}{}{}
				\fjclass{B}{}{}
				\fjclass{Get}{
					\attr[A]{a}
					\attr[B]{b}
				}{
					\method{Object}{get}{}{this.b}
				}
			\end{fjlisting}
		\end{minipage}
		\\
		Alors en notant $e_A = \fj{(A)(new Get(new A(), new B()).get())}$ et $e_B = \fj{(B)(new Get(new A(), new B()).get())}$, on a 
		
		$$(CL_A,e_A)\Downarrow \new A(); (CL_A,e_B)\not\Downarrow ; (CL_B,e_A)\not\Downarrow ; (CL_B,e_B)\Downarrow \new B()$$
		
		Donc aucun contexte ne peut satisfaire les deux class tables. Ce qui est problématique !
		
		On peut déjà chercher à simplifier le programme, afin d'enlever les opérations inutiles quand elles ne sont pas au cœur des opérations. Par exemple, dans le cas d'un programme totalement légitime, l'ajout de ces deux classes annulerai tout le travail, même si elles ne sont pas utilisées.
		
		On définit qu'un programme $P'$ est plus simple que $P$, noté $P' < P$ par trois axiomes:
		\begin{enumerate}
			\item $\CT(P') \prec \CT(P)$
			\item $e_{P'} = e_{P}$
			\item $\forall v\; P\Downarrow v \implies P'\Downarrow v$
		\end{enumerate}
	
	
	
	\section{Définir l'équivalence sur les expressions}
	
		
		Nous avions déjà défini le préordre suivant sur les Class Tables:
		$$ CTA \prec CTB \iff \forall e \forall v (CTA,e)\Downarrow v \implies (CTB,e)\Downarrow v$$
		
		Mais cette définition pose deux problèmes:
		\begin{itemize}
			\item On n'a toujours pas de préordre sur les programmes entiers, ni sur les expressions.
			\item Cette définition sémantique est difficile à vérifier, il nous faudrait une caractérisation de cette équivalence plus simple à vérifier en pratique.
		\end{itemize}
		
		\subsection{Une équivalence naïve}
		
			Si l'on souhaitait comparer deux expressions de but en blanc, dans une class table donnée.
			
			La version de l'expression trouée est superflue, en effet, on a pour toute class table $CT$ et toute paire d'expressions $e$ et $e'$ :
			
			$$ \left(\forall h \; (CT,h[e])\Downarrow v \implies (CT,h[e'])\Downarrow v\right) \ssi ((CT,e)\Downarrow v \implies (CT,e')\Downarrow v)$$
			
			Le sens direct se fait en particularisant à $h = [.]$ et le sens indirect se fait en appliquant les règles de réduction de congruence qui donnent
			$$\forall (e,e') \forall h\quad e\rightarrow e' \implies h[e] \rightarrow h[e']$$
			
			On peut alors essayer de dire que deux expressions ont le même fonctionnement sous toute class table, c'est à dire vérifier que $\forall CT ((CT,e)\Downarrow v \implies (CT,e')\Downarrow v)$.
			
			On va essayer de montrer que ce n'est pas vrai, en prouvant la chose suivante pour toute paire de formules $e$ et $e'$ qui soient cohérentes (c'est à dire $\exists CT \exists v (e,CT)\Downarrow v$, ce qui permet de s'assurer que l'on essaie pas de démentir Faux=>Faux, par exemple si $e$ vaut \fj{new A().field}):
			
			$$\exists CT\quad (e,CT)\Downarrow v \land (e',CT)\not{\Downarrow} v$$
			
			Hélas, ce résultat est faux, comme en témoignent les deux expressions suivantes: 
			$$\fj{new Pair(new A(),new B()).fst}$$ et $$\fj{new Pair(new Pair(new A(),new B()).fst,new B()).fst}$$
			
			Nous n'avons alors que trois types de classes tables: Celles qui ne compilent pas (Alors $\bot \implies \bot$), Celles où l'attribut $fst$ est donné en premier dans le constructeur de $Pair$ (Alors $e_1\Downarrow \new A()$ et $e_1\Downarrow \new A()$) et celles où l'attribut $fst$ est donné en second dans le constructeur de $Pair$ (Alors $e_1\Downarrow \new B()$ et $e_2\Downarrow \new B()$).
			
			Pire encore, on a que pour toutes formules $e$ et $e'$, $\phi(e)$ et $\phi(e')$ sont équivalents en ce sens avec $\phi$ défini comme
			
			$$\phi(e)=\fj{new Pair(new Pair(new A(),$e$).fst,new B()).fst}$$
			
			Cela est destructeur puisque l'on obtient des équivalences entre des expressions qui sont absurdes, par exemple, si $e = \fj{new T(new T())}$ qui est une valeur, mais qu'on ne peut mettre dans aucune methode, parce que la class table ne pourrait être cohérent.
			
			Nous alons donc définir la \emph{consistance} d'une liste d'expression FJ $\bar{e}$ :
			
				$$\text{$e_1,e_2,\dots,e_k$ sont consistants} \ssi \exists CT \; \forall i\in \llbracket1,k\rrbracket \; \exists T \; \emptyset\vdash_{CT}e : T$$
				
			\subsection{Preuve de l'inefficacité sur un ensemble d'expressions plus restreintes}
			
			Nous pouvons tout de même essayer de prouver le résultat pour des expressions plus restreintes. Par exemple, des expressions qui ne sont composées que de \fj{new} et d'appels à méthode (on peut imaginer remplacer les field access par des getters).
			
			Je vais maintenant expliquer comment obtenir une Class table qui prouve le théorème.
			
			Nous allons créer une class table telle que la méthode $m$ de la classe $C$ aie pour type de retour $\Phi(m,C)$ qui soit un nom de classe non utilisé. Par exemple, on choisit un mot qui n'est préfixe d'aucun nom de classe utilisé (pour l'exemple \verb*|F|), on choisit aussi un délimiteur une chaine de caractères inutilisées dans les noms de méthode (pour l'exemple \verb*|@|), et on note alors le type de retour de la méthode \fj{method} dans la classe \fj{Classe} par \fj{Fmethod@Classe}. on peut alors déterminer à partir du nom de la classe d'un objet la méthode et la classe associée.
			
			Ensuite, pour chaque occurence d'un appel à méthode \fj{e.m($\bar{x}$)} on détermine d'abord la classe de \fj{e}. C'est assez simple récursivement, puisque si \fj{e} est de la forme \fj{new C($\bar{x'}$)}, alors \fj{e} est de classe \fj{C}, et si \fj{e} est de la forme \fj{e'.m'($\bar{x}$)}, alors on détermine récursivement la classe \fj{C'} de \fj{e'}, puis on annonce que \fj{e} a le type $\phi(m',C')$, soit dans notre exemple $\verb*|F|m'\verb*|@|C'$.
			
			Une fois que l'on a déterminé la classe de $e$, on peut ajouter à $C$ une méthode $m$ définie ainsi:
			
			\begin{fjlisting}
				\method{Fm@C}{m}{Object x1,...,Object xk}{new Fm@C(this,x1,...,xk)}
			\end{fjlisting}
			
			Si la classe $C$ n'existe pas et que c'est une classe de la forme \verb*|Fm@C|, alors on peut la créer ainsi.
			
			\begin{fjlisting}
				\textbf{class} Fm@C \textbf{extends} Object \{\newline
				\null\qquad C obj;\newline
				\null\qquad Object x1;\newline
				\null\qquad \vdots\newline
				\null\qquad Object xk;\newline
				\null\qquad Fm@C(C obj, Object x1, \dots, Object xk)\{\newline
				\null\qquad\qquad \textbf{super()};\newline
				\null\qquad\qquad \textbf{this}.obj=obj;\newline
				\null\qquad\qquad \textbf{this}.x1=x1;\newline
				\null\qquad\qquad\vdots\newline
				\null\qquad\qquad \textbf{this}.xk=xk;\newline
				\null\qquad\}\newline
				\}
			\end{fjlisting}
		
		
			Appliquons maintenant à l'expression $e$ suivante :
			
			\begin{center}
				\fj{new A().quoi().qui(new B().quel(new B().quoi(new A().quoi())))}
			\end{center}
	
			Nous obtenons les structures de classes \textsc{Figure \ref{mRename:exampleClasses}} (dans l'ordre de lecture des applications de méthodes).
			
			\ttfamily
			\begin{figure}
			\begin{tabular}{cl|rcl}
				Classe & Méthode & Types paramètres & $\rightarrow$ & Type but \\
				\hline
				A & .quoi & $\emptyset$ & $\rightarrow$ & Fquoi@A \\
				Fquoi@A & .qui & \{Fquel@B\} & $\rightarrow$ & Fqui@Fquoi@A \\
				B & .quel & \{Fquoi@B\} & $\rightarrow$ & Fquel@B \\
				B & .quoi & \{Fquoi@A\} & $\rightarrow$ & Fquoi@B \\
				A & .quoi & $\emptyset$ & $\rightarrow$ & Fquoi@A \\
			\end{tabular}
			\caption{Structures de classes obtenues par l'exemple}
			\label{mRename:exampleClasses}
			\end{figure}
			\rmfamily
			
			On remarque que la première et dernière ligne sont égales. C'est normal, c'est parce que l'on appelle deux fois la même fonctions (On a une contrainte structurelle qui nous impose que ce soit la même fonction). Et puisque le programme testé est consistant, elle est appelée avec le même nombre d'arguments (possiblement des types différents, mais nous ne regardons pas le type et castons tout en \fj{Object}).
			
			On obtient alors la class table \textsc{Figure \ref{mRename:createdAB} et \ref{mRename:createdF}}
			
			\begin{figure}
			\begin{fjlisting}
				\fjclass{A}{}{
					\method{Fquoi@A}{quoi}{}{new Fquoi@A(this)}
				}
			\end{fjlisting}
			\begin{fjlisting}
				\fjclass{B}{}{
					\method{Fquel@B}{quel}{Object x}{new Fquel@B(this,x)}
					\method{Fquoi@B}{quoi}{Object x}{new Fquoi@B(this,x)}
				}
			\end{fjlisting}
			\caption{Classe A et B donnés pour l'expression exemple}
			\label{mRename:createdAB}
			\end{figure}
		
			\begin{figure}
			\begin{fjlisting}
				\fjclass{Fquoi@A}{\attr[A]{obj}}{
					\method{Fqui@Fquoi@A}{qui}{Object x}{new Fqui@Fquoi@A(this,x)}
				}
				\fjclass{Fqui@Fquoi@A}{\attr[Fquoi@A]{obj}\attr{x}}{}
				\fjclass{Fquel@B}{\attr[B]{obj}\attr{x}}{}
				\fjclass{Fquoi@B}{\attr[B]{obj}\attr{x}}{}
			
			\end{fjlisting}
			\caption{Classes artificielles pour l'expression exemple}
			\label{mRename:createdF}
			\end{figure}
			
			Alors notre exemple se résout en l'objet suivant : (les \fj{new} ont été enlevés pour plus de lisibilité)
			
			$$e \rightarrow^* \fj{Fqui@Fquoi@A(Fquoi@A(A),Fquel@B(B,Fquoi@B(B,Fquoi@A(A))))}$$
			
			On remarque que l'on peut reconstruire la formule à partir de la valeur finale. Il suffit de remplacer \fj{new Fmethod@Class(e0,e1,...ek)} par \fj{e0.method(e1,...,ek)} puis d'appliquer récursivement sur les \fj{ei}.
			
			Mais alors, étant donné deux expressions $e$ et $e'$ consistantes entre elles telles que $\forall C\; (CT,e)\Downarrow v \land (CT,e')\Downarrow v$. Alors, en particulier pour la class table que nous venons de créer, on a que les objets finaux sont égaux. Or, il est possible d'obtenir la formule qui a initié la valeur, donc les deux expressions qui n'utilisent pas les classes rajoutées, c'est à dire $e$ et $e'$ sont nécessarement égales.
			
			
			Nous pouvons aussi tester avec la restriction symétrique: Comment déterminer si deux programmes sont équivalents lorsqu'ils ne sont composés uniquement de \fj{new} et de \textit{field access} ?
			
			Dans cet autre cas simple, on n'utiliserai aucune méthode des éventuelles Class Tables, donc deux class tables se différenciant uniquement sur leurs méthodes produitront le même résultat. La même chose pour les noms de class inutilisés, ils sont .... inutilisés et donc ne changent pas le résultat si ils apparaîssent ou disparaissent.
			
			On se retrouve avec un nombre restreint de classes, il suffit de prendre la class table dans laquelle la formule est typable, de supprimer les classes inutilisées et les méthodes, puis de permuter l'ordre des attributs pour chaque classe. Il y a un nombre fini de combinaisons (encore moins si on ne considère pas les attributs non considérés), que l'on peut tester facilement (voir le contre-contre exemple du début, prouvé avec cette méthode).
			
			Mais quid des cas un peu plus intermédiaires ?
			
		\section{Des tests plus ciblés}
		
			Une première idée afin de faire des tests plus «ciblés» est de définir arbitairement un jeu de méthodes, classes, fields, sur les quelles les programmes seront comparés.
			
			\subsection{Définition des structures}
			
				Nous allons tout d'abord définir une grammaire des \textit{Test sets} ou «jeux de tests» à la \textsc{Figure \ref{ti:grammaire}}. Un exemple de tests est donné à la \textsc{Figure \ref{ti:examples}} où l'on définit des classes \fj{Int}, \fj{Frac}, \fj{Number} et \fj{RichInt} tel qu'on puisse appeler certaines méthodes sur elles. On impose aussi de pouvoir construire les object \fj{Frac} avec deux paramètres, et on impose aussi un attribut nommé \fj{value} dans la classes RichInt.
				
				\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}{rll}
								TI := & C : C m(bar{C}) & \qquad \newtag{\textrm{\textsc{TSG-Meth}}}{tsg:method} \\
								| & C \{bar{C} bar{f}\} & \qquad \newtag{\textrm{\textsc{TSG-Attr}}}{tsg:attributes} \\
								| & C (bar{C (? | f)}) & \qquad \newtag{\textrm{\textsc{TSG-Cstr}}}{tsg:constructor} \\
								| & C :> C & \qquad \newtag{\textrm{\textsc{TSG-Cast}}}{tsg:cast}
							\end{tabular}
						\end{center}
					\end{tcolorbox}
					\rmfamily
					\caption{Grammaire des test sets}
					\label{ti:grammaire}
				\end{figure}
			
				\begin{figure}
					\begin{fjlisting}
						Int \{\}
						
						Int : Int suivant(Int)
						
						Int : Int add(Int,Int)
						
						\null
						
						Frac(Int numerateur, Int denominateur)
						
						Frac : Frac inverted()
						
						Frac : Int floor()
						
						\null
						
						Number \{\}
						
						Frac <: Number
						
						Int <: Number
						
						\null
						
						RichInt \{Int value\}
						
						RichInt : Int getInt()
						
						RichInt <: Int
						
					\end{fjlisting}
					\caption{Exemple de set de tests}
					\label{ti:examples}
				\end{figure}
				
				Afin de valider un tests set, il faut simplement que :
				
				\begin{itemize}
					\item Chaque nom de classe n'est défini que une fois par une règle de type \ref{tsg:attributes} et \ref{tsg:constructor}.
					\item Chaque nom de methode n'est défini que une fois par nom de classe par une règle de type \ref{tsg:method}.
					\item Les noms de classes utilisés sont définis.
				\end{itemize}
				
				On pourrait se questionner sur la structure donnée aux règles \ref{tsg:attributes} et \ref{tsg:constructor}. La différence fondamentale entre les deux est que la première n'autorise pas à appeler \fj{new C(...)} alors que la seconde l'autorise. La première autorise seulement l'accès aux champs de la classe. On pourrait alors critiquer que cette façon de définir les règles ne permet pas d'autoriser la création d'un objet avec \fj{new} et d'autoriser certains \textit{field access} sans en imposer l'ordre. Pourtant, autoriser ces deux constructions impose que deux \textit{class tables} qui seraient équivalentes auraient le champ à la même position. Par exemple, on peut construire une expression simple \fj{new C(new P1(), new P2(), new P3(), ...).field} où \fj{P1}, \fj{P2}, \fj{P3} sont des classes créées pour l'occasion, qui ont des paramètes cohérents, etc… Alors cette expression se réduira en la même valeur dans deux \textit{class table} si et seulement si l'attribut \fj{field} est assigné au même indice dans le constructeur de \fj{C} dans les deux class tables.
				
				La troisième règle permet d'éviter des définitions «implicites» de classes, en suivant la convention suivie par la première définition du Featherweight Java \cite{fjdef}. On peut sinon ajouter la règle \fj{A\{\}} pour chaque nom de classe utilisé sans être défini.
				
				Nous allons aussi rajouter trois règles, qui ne sont pas strictement nécessaires, mais qui permettent de restreindre les tests sets aux tests sets «intéréssants», en enlevant certaines contraintes qui feraient apparaître des méthodes ou objets inutilisables.
				
				\begin{itemize}
					\item La relation obtenue par cloture réflexive et transitive des règles de type \ref{tsg:cast} est un bon ordre (en ajoutant la classe virtuelle \fj{Object})
					\item Dans les ocurrences des règles \ref{tsg:attributes} et \ref{tsg:constructor}, la relation «est le type d'un attribut» induit un bon ordre.
					\item Pour chaque règle \ref{tsg:cast} \fj{C :> B}, alors, la propriété adéquate est vérifiée, suivant les règles qui ont défini \fj{C} et \fj{B} selon le tableau suivant:
						\vspace{1ex}
						 \begin{tabular}{c|c|c|}
						 	& \fj{B\{}$\overline{\fj{G}}$ $\overline{\fj{g}}$\fj{\}} & \fj{B(}$\overline{\fj{G}}$ $\overline{\texttt{?}\fj{g}}$\fj{)}\\\hline
							 \fj{C\{}$\overline{\fj{F}}$ $\overline{\fj{f}}$\fj{\}} & \multirow{2}{*}{$\fj{f}_i = \fj{g}_j \implies \fj{F}_i = \fj{G}_j$} & $\exists \overline{\texttt{?}\fj{f'}}\;\exists \overline{\texttt{?}\fj{g'}}$\\
					 		\fj{C(}$\overline{\fj{F}}$ $\overline{\texttt{?}\fj{f}}$\fj{)} & & $\{\overline{\fj{F}} \; \overline{\left(\texttt{?}\fj{f} \oplus \texttt{?}\fj{f'}\right)}\} \subset \{\overline{\fj{G}} \; \overline{\left(\texttt{?}\fj{g} \oplus \texttt{?}\fj{g'}\right)}\}$
				 		\end{tabular}
				\end{itemize}
				
				La première règle semble cohérente, on peut imaginer simplement deux règles \fj{A <: B} et \fj{B <: A} qui n'auraient pas de sens ensemble.
				
				La troisième règle force les contraintes sur les types et noms des attributs à être cohérentes.
				
				On aimerai dire qu'il existe toujours au moins une \textit{class table} qui implémente une \textit{test interface} qui respecte toutes ces règles, mais hélas, ce n'est pas vrai, si l'on considère de manière naïve la relation «est le type d'un attribut» induit par la règle 2, voir troisième exemple de la \textsc{Figure \ref{ti:examplesfaux}}
								
				Cependant, on peut toujours (si la première et la troisième règle sont vérifiées) créer une class table bidon qui ne compile jamais. Pour cela, il suffit d'implémenter naïvement chaque class, sauf que nous remplaçons chaque occurence de \fj{extends Object} par \fj{extends SObject} (où \fj{SObject} est un nom de classe inutilisé). On crée la classe SObject avec un constructeur ne prenant pas de paramètre. Alors, on peut implémenter n'importe quelle méthode du type $\overline{\fj{M}} \rightarrow \fj{T}$ par l'expression \fj{(T) new SObject()}. L'expression est bien typable en \fj{T} puisque SObject est une superclasse de tous les types (sauf Object, auquel cas renvoyer simplement \fj{new SObject()}). Mais bien sûr, ces méthodes ne pourrons jamais renvoyer une valeur car le cast sera toujours impossible.
				
				
				
				\begin{figure}
					\begin{center}
					\begin{tabular}{ccc}
						\begin{fjlisting}[width=.2\textwidth]
							A \{\}
							
							B ()
							
							C (A)
							
							C :> B
						\end{fjlisting}
						&
						\begin{fjlisting}[width=.2\textwidth]
							A (A obj)
							
							B ()
							
							B : B m()
						\end{fjlisting}
						&
						\begin{fjlisting}[width=.2\textwidth]
							B \{obj\}
							
							C \{B obj\}
							
							C <: B
							
							C : B m()
						\end{fjlisting}
					\end{tabular}
					\end{center}
					\label{ti:examplesfaux}
					\caption{Exemples de \textit{test sets} implémentés par aucune \textit{class table} sans cast}
				\end{figure}
				
			
				Maintenant que nous avons notre grammaire, on peut définir plusieurs choses avec elles. Déjà, on va faire une relation $CT \triangleright TI$ pour dire que la class table $CT$ implémente la test interface $TI$, présentée à la \textsc{Figure \ref{ti:defImpl}}. L'implémentation est la plus tolérante possible quant au typage notamment des méthodes, car on ne veut pas comparer les \textit{class tables} sur leur typage, mais bien sur leur fonctionnement, le typage reste un garde-fou qui nous empêche de tester tout et n'importe quoi et d'obtenir une relation inexploitable. Typiquement, les deux \textit{class tables} présentées \textsc{Figure \ref{ti:exempletolerance}} implémenteront toutes deux la test interface jointe, et seront donc équivalentes.
				
				\begin{figure}
					\ttfamily
					\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
						\begin{align}
							\infer{CT \triangleright \left[\fj{C : D m($\overline{\texttt{E}}$)}\right]}{\operatorname{mtype}_{CT}(\fj{m},\fj{C}) = \fj{$\overline{\texttt{E}}$} \rightarrow \fj{D}}
						\end{align}
						\begin{align}
							\infer{CT \triangleright \left[\fj{ C \{ $\overline{\texttt{E}}\;\overline{\texttt{f}}$\}}\right]}{\bar{\fj{E}}\;\bar{\fj{f}} \subset \operatorname{fields}_{CT}(C)}
						\end{align}
						\begin{align}
							\infer{CT \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]}{\exists \bar{\fj{f'}}\; \bar{\fj{f0}} = \bar{\fj{f}}+\bar{\fj{f'}} \land \bar{\fj{E}}\;\bar{\fj{f0}} = \operatorname{fields}_{CT}(C)}
						\end{align}
						\begin{align}
							\infer{CT \triangleright \left[\fj{C} \subclass \fj{D}\right]}{\fj{C} \subclass_{CT} \fj{D}}
						\end{align}
					\end{tcolorbox}
					\rmfamily
					\caption{Grammaire des test sets}
					\label{ti:defImpl}
				\end{figure}
			
				\begin{figure}
					\begin{center}
					\begin{fjlisting}[width=.32\textwidth]
						A \{\}
						
						B \{\}
						
						Static ()
						
						Static : A get()
					\end{fjlisting}
					\begin{multicols}{2}
					\begin{fjlisting}[width=.48\textwidth]
						\fjclass{A}{}{}
						\fjclass[A]{B}{}{}
						\fjclass{Static}{}{
							\method{A}{get}{}{new B();}
						}
					\end{fjlisting}
					\columnbreak
					\begin{fjlisting}[width=.48\textwidth]
						\fjclass{A}{}{}
						\fjclass[A]{B}{}{}
						\fjclass{Static}{}{
							\method{B}{get}{}{new B();}
						}
					\end{fjlisting}
					\end{multicols}
					\end{center}
					
					\label{ti:exempletolerance}
					\caption{Exemple de classes justifiant la tolérance dans la définition de $\triangleright$}
				\end{figure}
			
				Nous allons donc maintenant essayer de typer une expression et une class table sous une test interface, dire que une expression $e$ avec sa class table associée $CT$ est «valide» dans un test interface $TI$ associé, que l'on note $TI,CT \Vdash e : T$ (pour bien différencier de la règle de typage de Featherweight Java, notée $\vdash$). 
				
				La présence d'une \textit{class table} associée à l'expression est nécessaire car il existe deux \textit{class tables} implémentant la même \textit{test interfaces} qui ne sont pas différenciables par des expressions seules, mais qui le sont lorsque l'on ajoute un class table (voir exemple \textsc{Figure \ref{ti:exempleneedct}}).
					
				\begin{figure}
					
					\begin{fjlisting}[width=.3\textwidth]
						B ()
						
						Static ()
						
						Static : B get(B)
					\end{fjlisting}
						
					\begin{fjlisting}[width=.48\textwidth]
						\fjclass{B}{}{}
						\fjclass{Static}{}{
							\method{B}{get}{B in}{in}
						}
					\end{fjlisting}
					
					\begin{fjlisting}[width=.48\textwidth]
						\fjclass{B}{}{}
						\fjclass{Static}{}{
							\method{B}{get}{B in}{new B()}
						}
					\end{fjlisting}
					
				
					\begin{fjlisting}[width=.42\textwidth]
						\fjclass[B]{A}{}{}
						\fjmain{new State().get(new A())}
					\end{fjlisting}
					
				
					\label{ti:exempleneedct}
					\caption{Exemple de class tables différentiables uniquement avec une class table}
				\end{figure}
				
				Les règles de typage sont obtenues en modifiant quelque peu les règles de typage de Featherweight java. La première étape est de définir les deux applications \textit{mtype} à partir des règles de type 1 et des déclarations de méthodes, et \textit{fields} qui s'obtient à partir des règles deux et trois et des champs présents dans la \textit{class table}. On rajoute enfin une application $\operatorname{construct(C)}$ qui est défini avec deux règles, l'une à partir de la règle trois et l'autre à partir des constructeurs réels (voir \textsc{Figure \ref{ti:defconstruct}}).
				
				\begin{figure}
					\ttfamily
					\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
						\begin{align}
							\infer{\operatorname{construct(C)} = \overline{\fj{D}}}{\fj{C(}\overline{\fj{D}}\;\overline{\fj{f}}\fj{)\{...\}}\in CT}
						\end{align}
						\begin{align}
							\infer{\operatorname{construct(C)} = \overline{\fj{D}}}{\fj{C(}\overline{\fj{D}}\;\overline{\texttt{?}\fj{f}}\fj{)} \in TI}
						\end{align}
					\end{tcolorbox}
					\rmfamily
					\caption{Application $\operatorname{construct(C)}$}
					\label{ti:defconstruct}
				\end{figure}
			
				Nous pouvons alors définir la relation de typage d'une expression sous une \textit{class table} et une \textit{test interface} avec des règles d'inférence présentées \textsc{Figure \ref{ti:deftyp}}. On ajoute aussi toutes les règles de typage d'expression présentées dans la définition du FJ Java \cite[p. 404]{fjdef}, en enlevant la règle \textsc{T-SCast} qui n'ajoute pas grand chose ...
				
				\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}{cr}
							\infer{TI,CT,\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}{\fj{x} \in \Gamma}
							& \textsc{TI-Var}
							\\[3ex]
							\infer{TI,CT,\Gamma \Vdash \fj{e.f} : \fj{E}}{TI,CT,\Gamma \Vdash e : \fj{C} \quad \fj{C} \subclass \fj{D} \quad \left[\fj{D(...,E f,...)}\right] \in TI}
							& \textsc{TI-Field}
							\\[3ex]
							\infer{TI,CT,\Gamma \Vdash \fj{e.m(}\overline{\fj{e'}}\fj{)} : \fj{R}}{\begin{array}{c}TI,CT,\Gamma \Vdash \fj{e} : \fj{C} \quad TI,CT,\Gamma \Vdash \overline{\fj{e'}} : \overline{\fj{E}} \\[-1.4ex] \fj{C} \subclass \fj{D} \quad \overline{\fj{E}} \subclass \overline{\fj{G}} \quad \left[\fj{D : R m(}\overline{\fj{G}}\fj{)}\right] \in TI\end{array}}
							&
							\textsc{TI-Invk}
							\\[3ex]
							\infer{TI,CT,\Gamma \Vdash \fj{new D(}\overline{\fj{e}}\fj{)} : \fj{D}}{TI,CT,\Gamma \Vdash \overline{\fj{e}} : \overline{\fj{E}} \quad \overline{\fj{E}} \subclass \overline{\fj{G}} \quad \left[\fj{D(}\overline{\fj{G}}\fj{)}\right] \in TI}
							&
							\textsc{TI-New}
							\\[3ex]
							\infer{TI,CT,\Gamma \Vdash \fj{(D)e} : \fj{D}}{TI,CT,\Gamma \Vdash \fj{e} : \fj{C} \quad \fj{C} \subclass_{TI} \fj{D}}
							&
							\textsc{TI-DCast}
							\\[3ex]
							\infer{TI,CT,\Gamma \Vdash \fj{(D)e} : \fj{D}}{TI,CT,\Gamma \Vdash \fj{e} : \fj{C} \quad \fj{D} \subclass_{TI} \fj{C} \quad \fj{C} \neq \fj{D}}
							&
							\textsc{TI-UCast}
						\end{tabular}
					\end{tcolorbox}
					\caption{Typage des expressions avec un test set et une class table}
					\label{ti:deftyp}
				\end{figure}
				
				
				\paragraph{Le théorème de validité du typage} que nous allons essayer de prouver s'énonce ainsi: Soit une \textit{test interface} $TI$, une \textit{class table} $CT$ et un test $(CT_t,e)$ vérifiant
				\begin{itemize}
					\item $CT \triangleright TI$
					\item $CT_t \text{\textsc{ OK in }} TI$
					\item $TS,CT_t \Vdash e : \fj{D}$
				\end{itemize}
				
				Alors il existe \fj{C} tel que $CT \oplus CT_t \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$, comme est démontré par l'exemple \textsc{Figure \ref{ti:exempletolth}}.
				
				\begin{figure}
					\begin{fjlisting}
						E \{\}
						
						D ()
						
						D : E m()
					\end{fjlisting}
				
					\begin{fjlisting}
						\fjclass{E}{}{}
						\fjclass[E]{F}{}{}
						\fjclass{F}{}{\method{F}{m}{}{new F()}}
					\end{fjlisting}
				
				$$e = \fj{new D().m()}$$
				
				$$TI \Vdash e : \fj{E} \qquad CT \vdash e:\fj{F} \qquad CT \triangleright TS$$
				
				\label{ti:exempletolth}
				\caption{Exemple de la nécessité de la seconde clause du théorème}
				\end{figure}
			
			
			\section{Équivalence de méthodes}
				
				\begin{definition}
					\slshape
					Deux méthodes de même nom \fj{Class.method} dans deux \textit{class tables} sont en préordre lorsque pour toute valeur $V$, valeurs $\overline{v}$ et valeurs $\overline{p}$ :
				
					\begin{gather*}
						(CT_1,e) \Downarrow V \implies (CT_2,e) \Downarrow V \\
						\text{avec } e=\fj{new Class($p_1$,$p_2$,...,$p_n$).method($v_1$,$v_2$,...,$v_m$)}
					\end{gather*}
				
					On note alors $CT_1 \methprec{Class.method} CT_2$
				\end{definition}
			
				Alors, nous souhaiterions prouver le théorème suivant:
				
				\begin{theorem}
					\slshape
					Soient deux \textit{class tables} $CT_1$ et $CT_2$ et une \textit{test interface} $TI$,
					
					$$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}$.
				
				Soient $CT_i$ des class tables.
				
				Soient $\overline{d}$ des expressions typables dans chaque $CT_i$ telles que pour toute sous-expression $\varepsilon$ de $d_i$, $\forall i,j \; (CT_i,\varepsilon)\Downarrow v \iff (CT_j,\varepsilon)\Downarrow v$
				
				Alors il existe une famille d'ensembles de variables $\overline{V}$ indexée par les $\overline{d}$, dont les variables sont dans $\bigwedge CT_i$ telle que
				
				$$\left[\overline{d}/\overline{x}\right]e \rightarrow^* V \iff \forall v_i \in V_i\quad \left[\overline{v}/\overline{x}\right]e \rightarrow^* V$$
				
				$\overline{V}$ dépend donc de $\bigwedge CT_i$ et de $d$.
				
				\subsubsection{Preuve de la confluence de la réduction en Featherweight Java}
					
					Nous allons dans cette section essayer de démontrer que la relation $\rightarrow$ de réduction de Featherweight Java est \textit{confluente}, c'est à dire que 
					
					$$\forall e,e_1,e_2\quad e_1 \leftsarrow e \rightarrow^* e_2 \implies (\exists e'\quad e_1 \rightarrow^* e' \leftsarrow e_2)$$
					
					La relation dénote ici la réduction sous une class table quelconque fixée.
					
					On peut se contenter de montrer la semi-confluence, c'est à dire 
					
					$$\forall e,e_1,e_2\quad e_1 \leftarrow e \rightarrow^* e_2 \implies (\exists e'\quad e_1 \rightarrow^* e' \leftsarrow e_2)$$
					
					Si $e \rightarrow e_1$, c'est qu'il y a un nœud qui s'est fait réduire de la forme \fj{e.f}, \fj{e.meth(...)} ou \fj{(C) e} où \fj{e} est de la forme \fj{new D(...)}. On va procéder à un \textit{marquage} de ce nœud afin de pouvoir l'observer dans $e_2$. Le marquage perdurera le long de la réduction $e \rightarrow^* e_2$. Notez que le marquage se démultiplie si un argument il est dans un argument d'une méthode qui se fait déplier et qu'il est utilisé plusieurs fois, et qu'il est détruit si la réduction s'effectue sur ce nœud.
					
					Ensuite, pour chaque expression du chemin $e \rightarrow^* e_2$, on remplace chaque nœud marqué par sa version réduite par application de la même règle que pour $e \rightarrow e_1$. On obtient un chemin $e_1 \rightarrow^* e'$ car une réduction ne modifie que le nœud qu'elle réduit plus éventuellement un nœud \fj{new} associé, or, une expression sous la forme \fj{new C(...)} ne pourra être réduite que en une expression de la même forme.
					
					Enfin, nous avons $e_2 \rightarrow e'$ car il suffit de réduire séquentiellement chaque nœud marqué dans $e_2$ par la même opération que pour $e \rightarrow e_1$, et nous obtenons par définition e'.
					
				\subsubsection{Obtention des ensembles de valeurs $V$}
					
					Pour créer l'ensemble de valeurs, nous allons nous restreindre à une seule \textit{class table} (la relation de réduction est donc simplement notée $\rightarrow$) et une seule expression $e \in \overline{d}$.
					
					Nous allons déjà définir une application appelée $\varnull$ qui transforme une expression en valeur en transformant les nœuds selon le tableau suivant: 
					
					\begin{tabular}{c|cl}
						Remplacer & Par & \\\hline
						\fj{e.f} & \fj{null(D)} & si $(\fj{D},\fj{f}) \in \operatorname{fields}(\fj{C})$ et $\vdash \fj{e} : \fj{C}$ \\
						\fj{e.m(...)} & \fj{null(D)} & si $\operatorname{mtype}(\fj{C},\fj{m}) = \overline{\fj{E}}\rightarrow\fj{D}$ et $\vdash \fj{e} : \fj{C}$ \\
						\fj{(D)e} & \fj{null(D)} & 
					\end{tabular}
				
					Cette transformation peut se faire dans n'importe quelle ordre, tant qu'il ne reste plus de nœuds à remplacer à la fin. Il est tout de même préférable de commencer par le nœud le plus proche de la racine afin de procéder au nombre minimal de remplacements.
					
					Nous allons distinguer trois différents cas.
					
					\paragraph{Premier cas} $e \rightarrow^* v$ et $v$ est une valeur.
					
						Alors on note simplement $V = \{v\}$ (c'était le cas le plus simple).
						
					\paragraph{Second cas} $e$ ne se réduit pas en une valeur, et toute suite de réduction partant de $e$ est finie.
					
						Alors, puisque le nombre d'expressions $e'$ telles que $e\rightarrow e'$ est fini pour tout $e$ et $e'$, on peut assurer qu'il y a un nombre fini d'expressions $e'$ telles que $e \rightarrow^* e'$. En appliquant la confluence de la réduction autant de fois qu'il y aie de $e'$ (moins $1$), on peut assurer qu'il existe une expression notée $e_v$ telle que $\forall e'\quad e \rightarrow^* e' \implies e' \rightarrow^* e_v$.
						
						On note enfin notre ensemble $V = \{\varnull(e_v)\}$.
						
					\paragraph{Troisième cas} $e$ ne se réduit pas en une valeur, et il existe au moins une suite de réductions infinie.
					
						Alors, notons $\mathcal{E}_k$ l'ensemble des expressions qui sont atteintes depuis $e$ avec $k$ réductions ou moins:
						
						$$\mathcal{E}_0 = \{e\}\qquad \mathcal{E}_{k+1}= \mathcal{E}_k \cup \rightarrow\!\!(\mathcal{E}_k)$$
				
						Par le même argument qu'au paragraphe précédent, les $\mathcal{E}_k$ sont tous finis.
						
						En appliquant $\#\mathcal{E}_k - 1$ fois la propriété de confluence, on détermine une expression $e_k$ (avec $e_0 = e$) telle que
						
						$$\forall e' \quad e' \in \mathcal{E}_k \implies e' \rightarrow^* e_k$$
					\begin{center}
					\begin{tikzpicture}
						
						\node[ellipse,draw,fill opacity=.1,minimum width=6cm,minimum height=1.4cm, fill=red] (7) at (0,0) {};
						
						
						\node (0) at (0, 2) {$e$};
						\node (1) at (-2, 0) {$e^x_1$};
						\node (2) at (-1, 0) {$e^x_2$};
						\node (3) at (1, 0) {$e^x_{n-1}$};
						\node (4) at (2, 0) {$e^x_n$};
						\node (5) at (0, -2) {$e_k$};
						\node (6) at (0,0) {$\cdots$};
						\draw [->] (0) -- (1) node[left, above,pos=1]{$*$};
						\draw [->] (0) -- (2) node[left, above,pos=1]{$*$};
						\draw [->] (0) -- (3) node[left, above,pos=1]{$*$};
						\draw [->] (0) -- (4) node[left, above,pos=1]{$*$};
						\draw [->] (1) -- (5) node[left,pos=1]{$*$};
						\draw [->] (2) -- (5) node[right, above,pos=1]{$*$};
						\draw [->] (3) -- (5) node[right, above,pos=1]{$*$};
						\draw [->] (4) -- (5) node[right,pos=1]{$*$};
						
						\node (8) at (3.2,0) {$\mathcal{E}_k$};
					\end{tikzpicture}
					\end{center}
				
				On note ensuite $\nextop(k) = \min\{i \in \mathbb{N},e_k \in \mathcal{E}_i, i > k\}$
				
				On peut enfin noter la considérer la chaine infinie (où la puissance dénote la composition).
				
				$$e_{\nextop^0(0)} \rightarrow^* e_{\nextop^1(0)} \rightarrow^* e_{\nextop^2(0)} \rightarrow^* \cdots$$
				
				
				Cette chaine a la propriété intéressante que l'on puisse y relier n'importe quelle expression $e'$ issue de $e$.
				
				$$\forall e'\quad e\rightarrow^* e' \implies (\exists i\quad e' \rightarrow^* e_{\nextop^i(0)})$$
				
				En effet, si on note $i$ le nombre d'étape de $e \rightarrow^* e'$, alors $e' \in \mathcal{E}_i$ donc $e' \in \mathcal{E}_{\nextop^i(0)}$ car $\nextop$ est strictement croissant et $\mathcal{E}$ aussi. Donc $e' \rightarrow^* e_{\nextop^i(0)}$ par définition de $e_{\nextop^i(0)}$.
				
				
				Enfin, notre ensemble de valeurs est $V = \{\varnull(e_{\nextop^i(0)})\}_{i\in\mathbb{N}}$.
				
				\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{Encore quelques critiques sur la définition de l'équivalence de classes}
					
					Je vais encore apporter une critique à la définition de l'équivalence de classes avec les Test Interfaces. Ce ne sont pas ces dernières le problème, mais plutôt la définition du préordre qui en suit. En effet, cette définition «teste» les class table sur toutes les valeurs possibles, et y impose donc des contraintes. Ainsi, deux objets au nom de classes différent seront nécessairement distincts.
					
					En effet, les deux class tables données \textsc{Figure \ref{classeq:ex}} ne sont pas équivalentes pour la \textit{test interface} donnée (l'expression \fj{new Static().true()}) premet de les distinguer, car \fj{new Bool()} est différent de \fj{new Other()}.
					
					Cependant, on pourrait souhaiter que ces classes soient équivalentes, en effet, le nom de la classe est la seule chose qui permet de les différencier car la classe \fj{Bool} de la première class table est en tout point similaire à la classe \fj{Other} de la seconde ! Un programme qui utiliserai la librairie n'aurait jamais à utiliser le nom de la classe du programme et ne saurait distinguer la valeur renvoyée par \fj{Static.true} dans la première class table et dans la seconde.
					
					\begin{figure}
						\begin{multicols}{2}
						\begin{fjlisting}
							\fjclass{Static}{}{
								\method{Bool}{true}{}{new Bool()}
								\method{Bool}{false}{}{new Other()}
							}
							\fjclass{Bool}{}{
								\method{Object}{ite}{Object t, Object f}{return t}
							}
							\fjclass[Bool]{Other}{}{
								\method{Object}{ite}{Object t, Object f}{return f}
							}
						\end{fjlisting}
						\columnbreak
						\begin{fjlisting}
							\fjclass{Static}{}{
								\method{Bool}{true}{}{new Other()}
								\method{Bool}{false}{}{new Bool()}
							}
							\fjclass{Bool}{}{
								\method{Object}{ite}{Object t, Object f}{return f}
							}
							\fjclass[Bool]{Other}{}{
								\method{Object}{ite}{Object t, Object f}{return t}
							}
						\end{fjlisting}
						\end{multicols}
						\begin{fjlisting}
							Static()
							
							Static: Bool true()
							
							Static: Bool false()
							
							Bool \{\}
							
							Bool: Object ite(Object,Object)
						\end{fjlisting}
						\label{classeq:exmpl}
						\caption{Deux classes que l'on aimerait équivalentes}
					\end{figure}
				
					Afin d'agrandir notre opérateur de préordre $\prec$, nous pouvons non plus comparer les \textit{class tables} sur toutes les valeurs, mais peut-être seulement sur celles \textbf{constructibles} dans la \textit{test interface}, plus celles \textbf{constructibles} par la class table de test.
									
				 \subsection{Renforcement du préordre sur les \textit{class tables}.}
				 
				 	On définit d'abort la grammaire des valeurs à trous. On peut la définir comme les expressions à trou, mais en enlevant toutes les règles n'étant pas \fj{new}. On les notera souvent par la lettre $\hbar$ Par exemple, \fj{new C([.],new S(new S([.],new G()),[.]))} est une valeur à trois trous. Les valeurs sont bien évidemment identifiées à des valeurs à zéro trous.
				 	
				 	On définit alors le préordre sur deux programmes $(CT_1,e_1) \prec (CT_2,e_2)$ par 
				 	
				 	$$\forall \hbar \forall \overline{e'} \quad \left(e_1 \rightarrow_{CT_1}^* \hbar\left[\overline{e'}\right] \implies \exists \overline{e''}\quad e_2 \rightarrow_{CT_2}^* \hbar \left[\overline{e''}\right]\right)$$
				 	
				 	On peut ainsi redéfinir la comparaison de deux class tables globalement ou sur une méthode:
				 	
				 	$$CT_1 \prec CT_2 \iff \forall e \quad (e,CT_1)\prec(e,CT_2)$$
				 	
				 	$$CT_1 \methprec{Class.meth} CT_2 \iff \forall \overline{p}\forall \overline{v} \quad (e,CT_1)\prec (e,CT_2) \text{ où } e=\fj{new Class(}\overline{p}\fj{).meth(}\overline{v}\fj{)}$$
				 	
				 	\begin{property}
				 		$$\forall \hbar \forall \overline{e} \quad \hbar\left[\overline{e}\right]\rightarrow e' \implies \exists \overline{e''}\quad e' = \hbar\left[\overline{e''}\right]$$
				 		
				 		On peut prouver cette propriété inductivement en montrant qu'une expression ayant un nœud \fg\fj{new}\og{} en nœud racine se réduira forcément en une expression ayant un nœud racine du même type.
				 	\end{property}
			 	
			 		\begin{property}
			 			$$CT_1\prec_{\text{new}}CT_2 \implies CT_1 \prec_{\text{old}}CT_2$$
			 			
			 			Il s'agit d'une particularisation, puisque qu'une valeur est une valeur à trou sans trou.
			 		\end{property}
		 		
		 			\begin{property}[Context Lemma]
		 				L'objectif de cette nouvelle définition était d'obtenir une sorte de \textit{context lemma}, puisque nous comparrons les expressions sur «toutes les valeurs qu'elles pourraient renvoyer».
		 				
		 				\begin{gather*}
		 				\forall CT \forall e_1,e_2\forall (h,CT_c)\\
		 				 (e_1,CT)\prec(e_2,CT) \implies (h[e_1],CT \oplus CT_c)\prec(h[e_2],CT \oplus CT_c)
		 				\end{gather*}
		 				
		 			\end{property}
	 			
	 				Nous allons le montrer en deux temps. Commençons par décomposer l'opérateur $\prec$, et à changer l'ordre des opérateurs:
	 				
	 				\begin{gather*}
	 					\forall CT\forall e_1,e_2 \forall CT_c \\
	 					\left(\forall \hbar\quad e_1 \rightarrow^* \hbar\left[\overline{e'}\right] \implies \exists \overline{e''}\quad e_2 \rightarrow^* \hbar\left[\overline{e''}\right]\right) \implies \\
	 					\left(\forall h \forall \hbar \quad h\left[e_1\right] \rightarrow^* \hbar\left[\overline{e'}\right] \implies \exists \overline{e''}\quad h\left[e_2\right] \rightarrow^* \hbar\left[\overline{e''}\right]\right)
	 				\end{gather*}
 				
 					On va déjà montrer le théorème en ajoutant comme contrainte que la réduction $h\left[e_1\right] \rightarrow^* \hbar\left[\overline{e'}\right]$ s'effectue sans application de méthode (\textsc{R-Meth}) à un appel à méthode contenu dans $h$. (C'est à dire que les appels à méthode de $h$ ne «servent à rien», ils pourraient être remplacés par \fj{null} sans modifier la réduction).
 					
 					Supposons alors $H_0:\quad \left(\forall \hbar\quad e_1 \rightarrow^* \hbar\left[\overline{e'}\right] \implies \exists \overline{e''}\quad e_2 \rightarrow^* \hbar\left[\overline{e''}\right]\right)$
 					
 					Montrons ce résultat par \textbf{induction} sur $h$.
 					
 					\paragraph{Premier cas: $\hbar = \hole$}
 						Alors on note $\overline{e''} = \left[e_2\right]$ et donc $e_2 \rightarrow^* e_2 = \hbar\left[\overline{e''}\right]$
 						
 					\paragraph{Sinon} alors on a nécessairement $\hbar = \fj{new D(}\hbar_1,\hbar_2,\dots,\hbar_k\fj{)}$. On note alors $\hbar\left[\overline{e_1'}\right] = \fj{new C(}\hbar_i\left[\overline{e}^i\right]\fj{)}$
 					
					\underline{$h = \hole$}
						On applique dirèctement $H_0$
					
					\underline{$h = \fj{new D(}e_1,\dots,e_{i-1},h',e_{i+1},\dots,e_k'\fj{)}$}
					
						Alors, \fj{D}=\fj{C} et $k'=k$ car $\fj{new D(...)} \rightarrow^* \fj{new C(...)}$
						
						Aussi, on a pour chaque $i$, $e_1^i \rightarrow^* \hbar_i\left[\overline{e'}^i\right]$
						
						Donc $h\left[e_2\right] = \fj{new C(}e_1^1,...,e_{i-1},h'\left[e_2\right],e_{i+1},...,e_1^k\fj{)}$
						
						Donc $h\left[e_2\right]\rightarrow^*\fj{new C(}\hbar_1\left[\overline{e'}^1\right],\dots,h'\left[e_2\right],\dots,\hbar_k\left[\overline{e'}^k\right]\fj{)}$
						
						Or, $h'\left[e_1\right] \rightarrow^*\hbar_i\left[\overline{e'}^i\right]$, qui n'utilise pas de réduction de méthode (car sinon, la réduction de $h\left[e_1\right]$ en utiliserai).
						
						Donc, en appliquant l'hypotèse d'induction à $h'$, on obtient que $h'\left[e_2\right] \rightarrow^*\hbar_i\left[\overline{e''}\right].$
						
						Donc $h\left[e_2\right] \rightarrow^* \fj{new C(}\hbar_1\left[\overline{e'}^1\right],\dots,\hbar_i\left[\overline{e''}\right],...,\hbar_k\left[\overline{e'}^k\right]\fj{)} = \hbar\left[\overline{e''}'\right]$
						
					\underline{$h = h'\fj{.f}$}
					
						Alors, $h'\left[e_1\right] \rightarrow^* \fj{new D(}e_1^1,\dots,e_1^{k'}\fj{)}$, et donc:
						
						$$h\left[e_1\right] \rightarrow^* \fj{new D(}e_1^1,\dots,e_1^{k'}\fj{).f} \rightarrow e_1^i \rightarrow^* \hbar\left[\overline{e'}\right]$$
						
						Donc $h'\left[e_1\right] \rightarrow^* \fj{new D(}e_1^1,\dots,e_1^{k'}\fj{)} \rightarrow^* \fj{new D(}e_1^1,\dots,\underbrace{\hbar\left[\overline{e'}\right]}_{\text{$i$ème pos}},\dots,e_1^{k'}\fj{)} = \hbar'\left[e_1^1,\dots,\overline{e'},\dots,e_1^{k'}\right]$
						
						En appliquant l'hypotèse de récurrence à $h'$ et $\hbar'$, dont la réduction ne contient toujours pas d'appel à méthode (on observe une sous-réduction), on obtient $h\left[e_2\right] = h'\left[e_2\right]\fj{.f} \rightarrow^* \hbar'\left[\overline{e''}\right]\fj{.f}$
						
						Donc $h\left[e_2\right] \rightarrow^* \hbar\left[\overline{e''}'\right]$
						
					\underline{$h = h'\fj{.meth(}\overline{e}\fj{)}$ ou $h = e\fj{.meth(}\overline{e},h',\overline{e}\fj{)}$}
						Ce cas est impossible, car alors, pour se résoudre en une expression de type \fj{new} (ici, $\hbar\left[\overline{e'}\right]$), il faudrait nécessairement un appel à méthode, ce qui n'est pas présent dans la réduction par hypothèse.
						
						
					On a donc démontré le lemme pour tous les cas, il nous manque d'inclure les appels à méthode.
					
					\paragraph{Mélange de réduction} Soient $h$ et $\hbar$ tels que $h\left[e_B\right] \rightarrow^*\hbar\left[\overline{e'}\right]$ sans autre contrainte. Alors, on peut changer l'ordre des étapes (voire en supprimer) afin d'obtenir une réduction
					
					$$h\left[e_B\right] \rightarrow^*_{\text{\textsc{R-Meth}}} h'\left[e_1\right] \underbrace{\rightarrow^*}_{\text{sans appel à méthode dans $h'$}}\hbar\left[\overline{e'}\right]$$
						 					
				\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}