% !TeX spellcheck = fr_FR
\documentclass[10pt,a4paper]{article}

\include{./header.tex}

\title{Vers la définition d'un préordre sur les programmes FeatherweightJava
	\\[1ex] \large Notes sur mon stage au LACL}
\hypersetup{pdftitle={Vers la définition d'un préordre sur les programmes FeatherweightJava}}
\author{Samy Avrillon, encadré par Daniele Varacca (LACL, UPEC)}

\begin{document}
	
	\maketitle
	
	\hsep
	
	\tableofcontents
	
	\newpage
	
	\section{Introduction}
		
		\subsection{Présentation du problème}
	
		\subsection{Motivations de l'étude}
		
		\subsection{Plan de ce rapport}
	
	\section{Définitions et notations}
	
		\subsection{Rappels de Featherweight Java}
			
			Dans cette section, je vais rappeler quelques notations et définitions du langage Featherweight Java, qui ont déjà été présentées dans le papier original \cite{fjdef} et que je vais continuer d'utiliser dans ce document.
			
			Je vais continuer d'utiliser la notation du sur-lignage afin d'indiquer une liste finie d'élément.
			Par exemple, on notera $f(\overline{a})$ pour indiquer un appel du type $f(a_1,a_2,\dots,a_n)$.
			
			Tout d'abord, on rappelle la grammaire des expressions, qui seront souvent notées $e$, $e_k$ ou $e'$, qui est la suivante:
			\[e = \fj{x} \spacebar \fj{new C($\overline{e}$)} \spacebar \fj{$e$.f} \spacebar \fj{$e$.m($\overline{e}$)} \spacebar \fj{(C)$e$}\]
			
			On appellera \eng{class table} tout ensemble de définitions de classes, on les notera $\mathcal{A}$, $\mathcal{B}$, $\mathcal{C}$,. Par convention, les noms de classes seront écrit en \verb*|CamlCase| (majuscule) et les noms de méthodes, attributs (\eng{fields}) et variables en \verb*|camelCase| (minuscule).
			
			Un \enquote{programme} Featherweight Java est un couple $(\mathcal{A},e)$ et est souvent noté $P$, $Q$, $R$. Cette expression est en quelque sorte le \eng{main} du programme On pourra noter $CT_P$ et $e_P$ pour accéder à la \eng{class table} et à l'expression du programme. 
			
			On appelle \enquote{valeur} toute expression composée uniquement de constructeurs.
			
			On note aussi $\vdash$ la relation de typage. On notera par exemple $\mathcal{A},\Gamma \vdash e : \fj{C}$ pour indiquer que l'expression $e$ avec l'environnement de typage $\Gamma$ (une ensemble d'entrées de type $e : \fj{C}$) est typée par la classe \fj{C} sous la \eng{class table} $\mathcal{A}$.
			
			La relation de réduction dépend de la \eng{class table} $\mathcal{A}$ utilisée. On la notera $\rightarrow_\mathcal{A}$ ou simplement $\rightarrow$ si il n'y a pas d'ambiguïté. On notera aussi $\rightarrow^*_\mathcal{A}$ ou $\rightarrow^*$ la cloture transitive et réflexive de la relation. On notera aussi $e\Downarrow v$ lorsque $e \rightarrow^* v$ et $v$ est une valeur. On pourra même écrire $e \Downarrow$ pour dire $\exists v \quad e \Downarrow v$ ($v$ est une valeur).
			
			Cette relation est définie avec deux types de règles, les règles de type \textsc{R} qui indiquent :
			\begin{itemize}
				\item L'évaluation d'un attribut d'un objet (\textsc{R-Field})
				\item L'évaluation d'une méthode (\textsc{R-Invk})
				\item L'évaluation d'un cast (\textsc{R-Cast})
			\end{itemize}
			L'autre type sont les règles de type \textsc{RC} qui sont les règles de \enquote{congruence}, permettant l'évaluation dans n'importe quelle sous-expression.
			
			Enfin, nous reprenons la définition de la classe \fj{Paire} issue du papier original, reproduite \autoref{fig:pairedef}
			
			\begin{figure}
				\begin{fjlisting}
					\fjclass{Paire}{\fjattr{fst} \fjattr{snd}}{}
				\end{fjlisting}
				\label{fig:pairedef}
				\caption{Définition de la classe Paire}
			\end{figure}
		\subsection{Définitions supplémentaires}
			
			Nous allons aussi ajouter la grammaire des expressions à trou notés $h$, $h_k$:
			\[h := \hole \spacebar \fj{$h$.f} \spacebar \fj{$h$.m($\overline{e}$)} \spacebar \fj{$e$.m($\overline{e}$,$h$,$\overline{e}$)} \spacebar \fj{new C($\overline{e}$,$h$,$\overline{e}$)} \spacebar \fj{(C) $h$}\]
			
			Puis on ajoute l'opération de \emph{remplissage} $h[e]$ pour $h$ expression à trou et $e$ expression classique, définie récursivement:
			
			\begin{align*}
				\fj{x}[e] &= \fj{x}\\
				\hole[e] &= e\\
				(\fj{$h$.f})[e] &= \fj{$h[e]$.f}\\
				(\fj{$h$.m($\overline{e}$)})[e] &= \fj{$h[e]$.m($\overline{e}$)}\\
				(\fj{$e$.m($\overline{e}$,$h$,$\overline{e}$)})[g] &= \fj{$e$.m($\overline{e}$,$h[g]$,$\overline{e}$)}\\
				(\fj{new C($\overline{e}$,$h$,$\overline{e}$)})[g] &= \fj{new C($\overline{e}$,$h[g]$,$\overline{e}$)}\\
				(\fj{(C) $h$})[e] &= \fj{(C) $h[e]$}
			\end{align*}
		
			Au niveau de la programmation en Featherweight Java, nous définissons quelques raccourcis d'écriture.
			Tout d'abord, la classe \fj{Static} que l'on suppose définie sans attributs. C'est une classe pour laquelle on suppose que les méthodes n'utilisent jamais \fj{this}. On autorise ainsi l'appel des méthodes de cette classe dirèctement. En pratique, On remplacera les appels à méthodes de type \fj{meth($\overline{e}$)} par \fj{new Static().meth($\overline{e}$)}.
			
			Enfin nous définissons plusieurs classes qui permettent de coder avec un niveau plus haut, dont les définitions complètes sont données en \autoref{anx:moreclass}.
			
			La première classe définie est la classe \fj{Bool}, liée à deux constantes \fj{true} et \fj{false}. Cette classe met à disposition une méthode \fj{ite(Object,Object)} telle que \fj{true.ite($t$,$f$)} renvoie $t$ et \fj{false.ite($t$,$f$)} renvoie $f$.
			
			La seconde classe est \fj{Int}, liée à plein de constantes \fj{0}, \fj{1}, \fj{2}, \dots. Cette classe met a disposition une méthode \fj{Bool isnull()} qui renvoie un booléen adéquat selon si l'entier testé est null ou pas. Plusieurs méthodes sont définies en sus dans la définition complète présentée en \autoref{anx:moreclass} permettant de manipuler ces objets.
			
			Aussi, nous définierons souvent les classes \fj{A}, \fj{B} et \fj{C}, qui n'ont pas d'attributs ni de méthode (ce sont des \enquote{objets simples}).
			
		\subsection{Extension du FeatherWeight Java}
		
			Afin de créer des théorèmes plus tard, nous allons parfois considérer une extension du FeatherWeight Java, qui ajoute une valeur \fj{null}. Cependant, ajouter une simple valeur qui soit typable pour tous type enlève l'unicité du typage dans une \eng{class table}, et une valeur qui ne soit typable pour aucun type enlève la préservation du type, car
			\[\underbrace{\fj{(C)null}}_{\vdash \fj{C}} \rightarrow \underbrace{\fj{null}}_{\nvdash}\]
			
			L'implémentation choisie est donc un \eng{null} toujours typé, que l'on notera \fj{null(C)}. Qui permet de préserver les deux propriétés sus-nommées.
			
			L'ajout de \fj{null(C)} ajoute une règle axiomatique de typage indiquant $\vdash \fj{null(C)}:\fj{C}$. On n'ajoute aucune règle de réduction (car on ne peut rien appliquer à \fj{null}). On ajoute aussi \fj{null(C)} dans la liste des valeurs.
			
			Une dernière remarque sur cet ajout est que l'on vient d'ajouter encore deux cas où une réduction d'une expression bien typée peut \enquote{bloquer}. Ces deux cas sont l'équivalent java des \verb*|NullPointerException| (un pour les attributs, l'autre pour les méthodes).
			
 
	\section{Étude d'équivalences simples}
		
		\subsection{Explication de l'utilité d'un contexte}
			
			Les équivalences entre les programmes sont habituellement fait en utilisant des \enquote{contextes}. Des programmes sont dits équivalents lorsqu'ils donnent les mêmes résultats sous tout contexte. Pour un contexte $C$, on va noter $C\bracket{P}$ l'interprétation d'un programme dans le contexte. Alors, le préordre sera défini comme tel:
			\[P\prec Q \ssi \forall C\quad C\bracket{P}\Downarrow v \implies C\bracket{Q}\Downarrow v\].
			On confondra souvent les termes \enquote{équivalence} et \enquote{préordre} dans la suite de ce document, car le premier est plus pratique pour visualiser l'utilité des constructions établies.
			
			Mais le plus gros problème est de déterminer ce qu'est un contexte. La tâche est d'autant plus difficile en Featherweight Java car un programme n'est pas constitué que d'une expression, comme en λ-calcul ou en π-calcul. Une expression seule n'a même aucun sens sans une \eng{class table} associée.
			
			\paragraph{Une définition la plus simple} On peut commencer par dire qu'un contexte est simplement une expression à trou $C = h$. L'interpretation d'un programme $P = (\mathcal{A},e)$ dans un contexte $C$ est alors 
			\[C\bracket{P} = (\mathcal{A},h\bracket{e})\]
			
			Le problème de cette définition est qu'elle est très peu puissante. En effet, le contexte est limité à l'utilisation de la \eng{class table} testée. Nous verrons plus tard des exemples démontrant que ce c'est une vraie limitation.
			
			Un autre problème est celui dit du trou dégénéré. En effet, beaucoup de \eng{class tables} permettent de créer un \eng{trou dégénéré}, c'est à dire que pour toute expression $e$, il existe une expression à trou $h$ telle que $\forall p h\bracket{p} \rightarrow^* e$.
			Un exemple de trou dégénéré est l'expression trouée suivante donnée pour $e$ expression, avec la classe \fj{Paire} dans la \eng{class table}
			\[\fj{new Paire($\hole$,$e$).snd}\]
			
			Ce problème du trou dégénéré permet d'évaluer n'importe quelle expression, ce qui fait que les expressions \eng{main} des programmes n'ont aucun effet sur le résultat de la comparaison. On peut donc évaluer pour chaque nom de classe $\fj{C}$ l'expression \fj{new C(null(D),...,null(E))} qui est une valeur si et seulement si la classe \fj{C} est présente dans la \eng{class table} et que ses attributs sont de types \fj{D},\fj{...},\fj{E}. De la même manière, on peut tester si une méthode existe dans une classe (à supposer qu'il existe des paramètres telle qu'elle se réduise en valeur). Donc deux programmes comparés ainsi devront avoir exactement la même structure, les mêmes noms de classe, mêmes noms d'attributs, même noms de méthode.
			
			Ainsi, on ne peut pas comparer par exemple une implémentation d'un algorithme de tri qui utiliserai une classe \fj{Tree} et une autre qui utiliserai une classe \fj{Map}. Puisqu'il n'y a pas d'\eng{access control} en Featherweigth Java, un utilisateur malveillant aurait accès à tous ces outils pour mettre en défaut le programme.
			
			La relation créée est ainsi robuste, mais inefficace.
			
			\paragraph{Une boîte à outils plus puissante}
			En essayant de résoudre le premier problème, nous aggravons le second. Afin de permettre aux contextes d'être plus complets, on est d'abord tenté d'y accoler une \eng{class table}. Ainsi, l'application du contexte $C = (\mathcal{C},h)$ au programme donne
			\[C\bracket{P} = (\mathcal{A} \oplus CT_P,h\bracket{e_P})\]
			(le $\oplus$ dénote un α-renommage évitant que les définitions s'écrasent les unes les autres)
			
			
			
		\subsection{Définitions et notations globales}
		
	\section{Des tests plus ciblés}
	
		\subsection{Définition de la structure de \eng{Test Interface}}
			
		\subsection{Définition du typage et d'un premier préordre}
																						
		\subsection{Renforcage de ce préordre avec les valeurs infinies}
		
	\section{Vers des équivalences plus pratiques}
	
		\subsection{Une équivalence entre les expressions}
		
		\subsection{Cette équivalence est trop forte}
		
		\subsection{L'équivalence méthode par méthode}
		
	\section{Conclusion}
	
		
	\newpage
	\section{Bibliographie}
	\printbibliography
	
	\newpage
	\appendix
	
	\section{Classes et Notations en FeatherweightJava}
	\label{anx:moreclass}
	\subsection{Les booléens}
		\begin{fjlisting}
			\fjclass{Bool}{}{
				\fjmethod{Object}{ite}{Object oTrue, Object oFalse}{oTrue}
			}
			\fjclass[Bool]{OBool}{}{
				\fjmethod{Object}{ite}{Object oTrue, Object oFalse}{oFalse}
			}
		\end{fjlisting}
	
		De plus, on note les constantes suivantes:
		\[\fj{true} = \fj{new Bool()}\]
		\[\fj{false} = \fj{new OBool()}\]
	\subsection{Les entiers}
		\begin{fjlisting}
			\fjclass{Int}{}{
				\fjmethod{Bool}{isNull}{}{true}
			}
			\fjclass{SInt}{\fjattr[Int]{prec}}{
				\fjmethod{Bool}{isNull}{}{false}
			}
		\end{fjlisting}
	
		On ajoute aussi la notation des nombres :
		\[\fj{0} = \fj{new Int()}\]
		\[n = \fj{new SInt(n-1)}\]
	
\end{document}
