844 lines
53 KiB
TeX
844 lines
53 KiB
TeX
% !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}
|
||
\marginpar{Voir pour enlever cette section si pas assez utilisée}
|
||
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.
|
||
|
||
\subsection{Exemples d'équivalences simples}
|
||
|
||
\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}
|
||
Afin de permettre aux contextes d'être plus complets et d'ainsi résoudre le premier problème, 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{C} \oplus CT_P,h\bracket{e_P})\]
|
||
(le $\oplus$ dénote un α-renommage évitant que les définitions s'écrasent les unes les autres)
|
||
|
||
Hélas, cela renforce le second problème, car il existe alors forcément un trou dégénéré dans une \eng{class table} $\mathcal{C} \oplus CT_P$ (on n'a qu'à rajouter une classe ressemblant à \fj{Paire}).
|
||
|
||
\paragraph{Restreindre les \eng{class tables}}
|
||
|
||
Une dernière définition simple consiste à imposer certaines contraintes sur les \eng{class tables} des programmes comparés. On va d'abord définir le préordre suivant sur les \eng{class tables} :
|
||
|
||
\[\mathcal{A} \prec \mathcal{B} \iff \forall e \forall v \quad (\mathcal{A},e)\Downarrow v \implies (\mathcal{B},e)\Downarrow v\]
|
||
|
||
Souhaitant garder les contextes les plus puissants possibles, on les définit comme des couples $(\mathcal{C},h)$ et on note alors la contextualisation d'un programme $P = (\mathcal{A},e)$
|
||
\[C\bracket{P} = (\mathcal{C}, h\bracket{e})\qquad \underline{\text{si } \mathcal{A} \prec \mathcal{C}}\]
|
||
|
||
Cette condition restreint le nombre de contextes pouvant transformer un programme, et donc transforme le préordre en
|
||
\[P \prec Q \iff \forall C\quad
|
||
\left|\begin{array}{l}CT_P \prec CT_C\\ CT_Q \prec CT_C \\
|
||
\forall v\quad C\bracket{P}\Downarrow v \implies C\bracket{Q}\Downarrow v\end{array}\right. \]
|
||
|
||
Cependant, cette définition pose un problème lorsque l'on cherche à copmarer deux \eng{class tables} qui n'ont aucune \enquote{sur-\eng{class table}} qui convienne aux deux en même temps. C'est le cas des deux classes données \autoref{fig:nosurct} notées $\mathcal{A}$ et $\mathcal{B}$.
|
||
|
||
\begin{figure}
|
||
\begin{multicols}{2}
|
||
\begin{fjlisting}
|
||
\fjclass{Get}{
|
||
\fjattr[A]{a}
|
||
\fjattr[B]{b}
|
||
}{
|
||
\fjmethod{Object}{get}{}{this.a}
|
||
}
|
||
\end{fjlisting}
|
||
\columnbreak
|
||
\begin{fjlisting}
|
||
\fjclass{Get}{
|
||
\fjattr[A]{a}
|
||
\fjattr[B]{b}
|
||
}{
|
||
\fjmethod{Object}{get}{}{this.b}
|
||
}
|
||
\end{fjlisting}
|
||
\end{multicols}
|
||
\label{fig:nosurct}
|
||
\caption{\eng{Class tables} n'ayant pas de sur-\eng{class table} commune}
|
||
\end{figure}
|
||
|
||
En effet, en notant les expressions suivantes
|
||
\[\begin{array}{c}
|
||
e_A = \fj{(A)(new Get(new A(), new B()).get())} \\
|
||
e_B = \fj{(B)(new Get(new A(), new B()).get())}
|
||
\end{array}\]
|
||
|
||
On peut observer les relations suivantes qui montrent que une \eng{class table} qui conviendrait à $\mathcal{A}$ et à $\mathcal{B}$ serait impossible, car elle pourrait et ne pourrait pas évaluer $e_A$ et $e_B$ en une valeur.
|
||
\[\begin{array}{cc}
|
||
(CL_A,e_A)\Downarrow \new A()& (CL_A,e_B)\nDownarrow \\
|
||
(CL_B,e_A)\nDownarrow & (CL_B,e_B)\Downarrow \new B()
|
||
\end{array}\]
|
||
|
||
\section{Des tests plus ciblés}
|
||
|
||
\paragraph{Abandon de l'expression \fj{main}}
|
||
|
||
Tous les tests vus dans la section précédente visaient à tester un programme entier (Une \eng{class table} et une expression). Il semble cependant étrange de procéder ainsi. En effet, nous allons souvent comparer uniquement des librairies, ce qui correspondrai à nos \eng{class tables}. On ne cherche plus à savoir si deux programmes \enquote{font la même chose}, mais plutôt est-ce que ces deux \eng{class tables} fournissent les mêmes fonctions.
|
||
|
||
En bonus, l'étude des \eng{class tables} est tout aussi complète que l'étude des programmes entiers, car nous pouvons toujours rajouter une classe \fj{Main} qui n'aie qu'une méthode \fj{Main.main} dont le corps soit l'expression de notre programme. Alors tester cette nouvelle \eng{class table} reviendra à tester le programme entier.
|
||
|
||
\paragraph{Idée d'une nouvelle structure}
|
||
|
||
Le problème de tous les contextes ci-dessus est qu'ils imposent tous une structure trop précise aux \eng{class tables} comparées. Elles doivent toutes avoir impérativement les mêmes classes, attributs et méthodes, là où on aimerai justement les comparer sur certaines classes, attributs ou méthodes.
|
||
|
||
Nous allons donc créer une structure appelée \eng{test interface} (ou interface de test) qui permet de restreindre les tests à l'utilisation de classes, attributs et méthodes spécifiques. La restriction se fera à l'aide du typage.
|
||
|
||
Le terme interface n'est pas anodin, la structure ressemble à une interface Java (ou Featherweigth Java \cite{liquori_fjInterfaces}), mais en plus rigoureuse. Une expression va \enquote{compiler} (c'est à dire être typée) contre l'interface, puis sera \enquote{executée} (c'est à dire réduite) contre des vraies \eng{class tables}.
|
||
|
||
\subsection{Définition de la structure de \eng{Test Interface}}
|
||
|
||
\paragraph{Structure} Nous définissons donc la structure des \eng{test interface rules} dans la \autoref{fig:tigrammaire}. Une teste interface est alors simplement un ensemble de \eng{test interface rules}, et sera noté $\mathfrak{T}$, $\mathfrak{U}$, $\mathfrak{V}$. La règle \autoref{rule:tsg:method} permet de déclarer une méthode dans un classe et de spécifier son type. La \autoref{rule:tsg:attributes} permet de déclarer certains attributs d'une classe, en spécifiant leur nom et leur type. La \autoref{rule:tsg:constructor} permet de déclarer le constructeur de la classe ainsi que les types des attributs, et éventuellement certains noms. Enfin, la \autoref{rule:tsg:cast} permet d'indiquer que une classe doit être un sous-type d'un autre.
|
||
|
||
Un exemple concret de \eng{test interface} est donnée \autoref{fig:tiexample}. On y définit des classes \fj{Int}, \fj{Frac}, \fj{Number} et \fj{RichInt} telles que l'on puisse appeler certaines méthodes sur elles. On impose aussi de pouvoir construire les object \fj{Frac} avec deux paramètres de type \fj{Int}, 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}
|
||
\refstepcounter{rule}
|
||
\begin{tabular}{rll}
|
||
TR := & C : C m($\overline{\fj{C}}$) & \qquad \newtag{\textrm{\textsc{TSG-Meth}}}{rule:tsg:method} \\
|
||
| & C \{$\overline{\fj{C}}$ $\overline{\fj{f}}$\} & \qquad \newtag{\textrm{\textsc{TSG-Attr}}}{rule:tsg:attributes} \\
|
||
| & C ($\overline{\fj{C}}$ $\overline{\fj{(?|f)}}$) & \qquad \newtag{\textrm{\textsc{TSG-Cstr}}}{rule:tsg:constructor} \\
|
||
| & C :> C & \qquad \newtag{\textrm{\textsc{TSG-Cast}}}{rule:tsg:cast}
|
||
\end{tabular}
|
||
\end{center}
|
||
\end{tcolorbox}
|
||
\rmfamily
|
||
\caption{Grammaire des \eng{test interface rules}}
|
||
\label{fig:tigrammaire}
|
||
\end{figure}
|
||
|
||
\begin{figure}
|
||
\begin{fjlisting}
|
||
Int \{\}\\
|
||
Int : Int suivant(Int)\\
|
||
Int : Int add(Int,Int)\medskip
|
||
|
||
Frac(Int numerateur, Int denominateur)\\
|
||
Frac : Frac inverted()\\
|
||
Frac : Int floor()\medskip
|
||
|
||
Number \{\}\\
|
||
Frac <: Number\\
|
||
Int <: Number\medskip
|
||
|
||
RichInt \{Int value\}\\
|
||
RichInt : Int getInt()\\
|
||
RichInt <: Int
|
||
\end{fjlisting}
|
||
\caption{Exemple de \eng{test interface}}
|
||
\label{fig:tiexample}
|
||
\end{figure}
|
||
|
||
À cette grammaire, nous allons ajouter quelques règles afin que la \eng{test interface} soit considérée comme valide. Dans la suite du document, on considèrera que toutes les \eng{test interfaces} utilisées sont toujours valides. Ces règles sont les suivantes:
|
||
|
||
\begin{itemize}
|
||
\item Chaque nom de classe est défini au plus une fois par une \autoref{rule:tsg:attributes} ou une \autoref{rule:tsg:constructor}.
|
||
\item Chaque nom de methode est défini au plus une fois par nom de classe par une \autoref{rule:tsg:method}.
|
||
\item Les noms de classe utilisés sont définis (sauf éventuellement Object).
|
||
\end{itemize}
|
||
|
||
Les deux règles \ref{rule:tsg:attributes} et \ref{rule:tsg:constructor} sont mutuellement exclusives pour un nom de classe donnée. La différence est que la seconde autorise l'appel au constructeur (l'expression \fj{new C(...)}) et imposant un ordre sur les paramètres là ou la seconde n'autorise pas le constructeur, et n'impose donc pas d'ordre sur les attributs.
|
||
|
||
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}\]
|
||
% TODO Ajouter une note sur l'abscence de tolérance lorsque les champs sont spécifiés.
|
||
|
||
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$, et que $\mathcal{A}$ est bien typé ($\mathcal{A}\;\textsc{OK}$).
|
||
|
||
\begin{figure}
|
||
\ttfamily
|
||
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
|
||
\refstepcounter{rule}
|
||
\begin{center}
|
||
\begin{tabular}{cr}
|
||
\infer
|
||
{\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{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]}
|
||
{\begin{array}{l}
|
||
\exists \overline{\fj{f'}}\quad \overline{\fj{f0}} = \overline{\fj{f}}+\overline{\fj{f'}} \\
|
||
\exists \overline{\fj{E'}} \quad \overline{\fj{F}} = \overline{\fj{E}} \backslash \overline{\fj{E'}} \\
|
||
\overline{\fj{E}} \subclass \overline{\fj{F}} \quad \land \quad
|
||
\overline{\fj{F}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)
|
||
\end{array}
|
||
}
|
||
&\newtag{\textrm{\textsc{(TRI-Cstr)}}}{rule:tri:constructor}\\[1em]
|
||
|
||
\infer
|
||
{\mathcal{A} \triangleright \left[\fj{C} \subclass \fj{D}\right]}
|
||
{\fj{C} \subclass_\mathcal{A} \fj{D}}
|
||
&\newtag{\textrm{\textsc{(TRI-Cast)}}}{rule:tri:cast}
|
||
\end{tabular}
|
||
\end{center}
|
||
\end{tcolorbox}
|
||
\rmfamily
|
||
\caption{Définition de l'implémentation des \eng{test interfaces rule}}
|
||
\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{B}$ 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}}}
|
||
{\left[\fj{C($\overline{\texttt{D}}\;\overline{\texttt{?f}}$)}\right] \in \mathfrak{T}}
|
||
& \newtag{\textrm{\textsc{LTi-Cstr}}}{rule:lti-construct}\\[1em]
|
||
\infer
|
||
{\operatorname{construct}(\fj{C}) = \overline{\fj{D}}}
|
||
{\fj{class C\{C($\overline{\texttt{D}}\;\overline{\texttt{f}}$)\{...\} ... \}}\in \mathcal{B}}
|
||
& \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{B}}
|
||
& \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{B}}
|
||
& \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{B}$.
|
||
|
||
\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 presque à 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{B}$, 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}. On note alors $\mathcal{B} \OKin \mathfrak{T}$. 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 mal définies.\marginpar{à prouver}
|
||
|
||
\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{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}
|
||
{\fj{x} \in \Gamma}
|
||
& \newtag{\textrm{\textsc{TI-Var}}}{rule:ti:variable}
|
||
\\[3ex]
|
||
\infer
|
||
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}}
|
||
{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{C0} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{C0})}
|
||
& \newtag{\textrm{\textsc{TI-Field}}}{rule:ti:field}
|
||
\\[3ex]
|
||
\infer
|
||
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.m($\overline{e_x}$)} : \fj{C}}
|
||
{\begin{array}{c}\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{C0} \quad \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \\[-1.4ex] \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{mtype}(\fj{m},\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}}
|
||
& \newtag{\textrm{\textsc{TI-Invk}}}{rule:ti:invoke}
|
||
\\[3ex]
|
||
\infer
|
||
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{new C(}\overline{e_x}\fj{)} : \fj{C}}
|
||
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{constructor}(\fj{C}) = \overline{\fj{D}}}
|
||
& \newtag{\textrm{\textsc{TI-New}}}{rule:ti:new}
|
||
\\[3ex]
|
||
\infer
|
||
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
|
||
{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}}
|
||
& \newtag{\textrm{\textsc{TI-DCast}}}{rule:ti:downCast}
|
||
\\[3ex]
|
||
\infer
|
||
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
|
||
{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \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}
|
||
|
||
Nous allons maintenant vérifier la définition de cette opération de typage $\Vdash$ en démontrant le théorème suivant:
|
||
|
||
\begin{theorem}
|
||
\label{thm:tiTyp}
|
||
Soit une \eng{test interface} $\mathfrak{T}$, une \eng{class table} $\mathcal{A}$ et un test $(\mathcal{B},e)$ vérifiant
|
||
\begin{itemize}
|
||
\item $\mathcal{A} \triangleright \mathfrak{T}$
|
||
\item $\mathcal{B} \OKin \mathfrak{T}$
|
||
\item $\mathfrak{T},\mathcal{B} \Vdash e : \fj{D}$
|
||
\end{itemize}
|
||
|
||
Alors il existe \fj{C} tel que $\mathcal{A} \oplus \mathcal{B} \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{B} \Vdash e : \fj{D}$. La preuve est donnée en \autoref{anx:proofTyptyp}.
|
||
|
||
On peut alors 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{A'} \ssi \forall (\mathcal{B},e) \left|\begin{array}{l}
|
||
\mathcal{B} \OKin \mathfrak{T}\\
|
||
\mathfrak{T},\mathcal{B} \Vdash e : \fj{D}\\
|
||
\mathcal{A}\oplus\mathcal{B} \Downarrow v
|
||
\end{array}\right. \implies \mathcal{A'}\oplus\mathcal{B}\Downarrow v\]
|
||
\end{definition}
|
||
|
||
|
||
\subsection{Renforcage de ce préordre avec les valeurs infinies}
|
||
|
||
Nous souhaiterions pouvoir démontrer un \eng{context lemma} sur les préordres précédents, c'est à dire un théorème qui dise que pour toute expression à trou $h$
|
||
|
||
\[(\mathcal{A},e)\prec(\mathcal{B},f) \implies (\mathcal{A},h\bracket{e})\prec(\mathcal{A},h\bracket{f})\]
|
||
|
||
Cependant, cela est généralement faux, puisque il est possible en Featherweight Java de considérer des expressions qui vont se réduire à l'infini, mais que l'on peut \enquote{utiliser} avec des appels à méthodes ou des attributs. Nous pouvons par exemples utiliser les listes infinies, définies en annexe (\autoref{anx:classes:listes}). Cette classe définie deux attributs, dont un de son propre type.
|
||
|
||
\begin{figure}
|
||
\begin{fjlisting}
|
||
\fjclass{Static}{}{
|
||
\fjmethod{IList}{intList}{Int i}{new IList(i, intList(i+1))}
|
||
\fjmethod{IList}{zeroList}{}{new IList(0, zeroList())}
|
||
}
|
||
\end{fjlisting}
|
||
\label{fig:ilistsDefs}
|
||
\caption{Définitions de listes infinies}
|
||
\end{figure}
|
||
|
||
Par exemple, avec la \eng{class table} définie \autoref{fig:ilistsDefs}, nous pouvons considérer les deux expressions $e_i = \fj{intList(0)}$ et $e_0 = \fj{zeroList()}$. Tels que nous les avons défini précédemment, nos preordres ne permettent pas de différencier ces deux expressions. En effet, puisque aucune des deux ne se réduit en une valeur, on est dans une situation de $\text{faux}\implies\text{faux}$. Cependant, certaines expressions à trou sont capables de les différencier. On peut par exemple considérer l'expression $h = \fj{$\hole$.next.obj}$, nous aurons effectivement les réductions suivantes:
|
||
|
||
\[
|
||
\begin{array}{rcl}
|
||
h\bracket{e_i} &=& \fj{intList(0).next.obj}\\
|
||
&\rightarrow& \fj{new IList(0, intList(0+1)).next.obj}\\
|
||
&\rightarrow& \fj{intList(0+1).obj}\\
|
||
&\rightarrow& \fj{new IList(0+1, intList(0+1+1)).obj}\\
|
||
&\rightarrow& \fj{0+1}\\
|
||
&\rightarrow^{\!*}& \fj{1}\\
|
||
|
||
h\bracket{e_0} &=& \fj{zeroList().next.obj}\\
|
||
&\rightarrow& \fj{new IList(0, zeroList()).next.obj}\\
|
||
&\rightarrow& \fj{zeroList().obj}\\
|
||
&\rightarrow& \fj{new IList(0, zeroList()).obj}\\
|
||
&\rightarrow& \fj{0}
|
||
\end{array}
|
||
\]
|
||
% TODO faut-il adapter l'exemple aux test interfaces au risque de trop surcharger ?
|
||
|
||
Nous avons l'impression que certaines expressions forment des sortes de \enquote{valeurs infinies}, qui peuvent quand même être utilisées dans des programmes, mais uniquement de manière finie. Nous allons donc redéfinir tous les préordres, en remplacant les propositions de la forme suivante.
|
||
\[\forall v\quad (\mathcal{A}, e) \Downarrow v \implies (\mathcal{B}, f) \Downarrow v\]
|
||
|
||
Nous allons tout d'abord définir une nouvelle grammaire, celle des \enquote{valeurs à trou}, que l'on notera souvent avec la lettre $\hbar$. Les valeurs simples sont identifiées aux valeurs à zéro trous, et par exemple, l'objet suivant est une expression à trois trous
|
||
\[\fj{new C([.],new S(new S([.],new G()),[.]))}\]
|
||
|
||
La grammaire est la suivante, on définit également l'opération de remplissage des trous, comme fait pour la définition des expressions à trou.
|
||
\[\hbar := \hole \spacebar \fj{new C($\overline{\hbar}$)}\]
|
||
\marginpar{y a t'il besoin de redéfinir le remplissage des trous ?}
|
||
|
||
Nous alons alors pouvoir redéfinir le préordre sur deux programmes :
|
||
\[(\mathcal{A},e)\pprec(\mathcal{B},f) \ssi \forall \hbar \forall \overline{e'} \quad \left(e \rightarrow_\mathcal{A}^* \hbar\left[\overline{e'}\right] \implies \exists \overline{e''}\quad f \rightarrow_\mathcal{B}^* \hbar \left[\overline{e''}\right]\right)\]
|
||
|
||
Intuitivement, on vérifie que si d'un coté du préordre, l'expression peut s'évaluer en \fj{new C(...)}, alors l'autre coté s'évalue en un objet de la même classe, et ce récursivement.
|
||
\marginpar{Cette expression me semble peu claire.}
|
||
|
||
On redéfit ainsi tous les autres préordres, notamment celui sur les \eng{class tables}:
|
||
\[\mathcal{A}\pprec\mathcal{B} \ssi \forall e \quad (\mathcal{A},e) \pprec (\mathcal{B},e)\]
|
||
|
||
Nous allons maintenant étudier les propriétés de ce préordre.
|
||
|
||
\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 \enquote{\fj{new}} en nœud racine se réduira forcément en une expression ayant un nœud racine du même type, en inversant la relation de réduction.
|
||
\marginpar{y a t'il besoin d'une preuve plus complète ?}
|
||
\end{property}
|
||
|
||
\begin{property}
|
||
$$\mathcal{A} \pprec \mathcal{B} \implies \mathcal{A} \prec \mathcal{B}$$
|
||
|
||
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 comparons dorénavant les expressions sur \enquote{toutes les valeurs qu'elles pourraient renvoyer}.
|
||
|
||
\begin{gather*}
|
||
\forall \mathcal{A} \quad\forall e,f \quad\forall (h,\mathcal{B})\\
|
||
(e,\mathcal{A})\pprec(f,\mathcal{B}) \implies (h[e],\mathcal{A} \oplus \mathcal{B})\pprec(h[f],\mathcal{A}\oplus\mathcal{B})
|
||
\end{gather*}
|
||
|
||
La démonstration est présentée en annexe (\autoref{anx:proofHValCL})
|
||
\marginpar{Besoin de présenter rapidement la preuve}
|
||
\end{property}
|
||
|
||
|
||
|
||
|
||
\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}
|
||
|
||
|
||
\clearpage
|
||
\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)}\]
|
||
|
||
\subsection{Les listes}
|
||
\label{anx:classes:listes}
|
||
\begin{fjlisting}
|
||
// Listes Infinies\\
|
||
\fjclass{IList}{\fjattr[IList]{next}\fjattr{obj}}{}\\
|
||
// Listes Finies\\
|
||
\fjclass{List}{}{
|
||
\fjmethod{Bool}{isEmpty}{}{true}
|
||
}\\
|
||
\fjclass[List]{Cons}{\fjattr[List]{queue}\fjattr{head}}{
|
||
\fjmethod{Bool}{isEmpty}{}{false}
|
||
}
|
||
\end{fjlisting}
|
||
|
||
On ajoute aussi les notations des listes :
|
||
\[\fj{[]} = \fj{new List()}\]
|
||
\[\fj{$o$::$e$} = \fj{new Cons($e$,$o$)}\]
|
||
|
||
\section{Preuve du théorème de cohérence du typage des \eng{test interfaces}}
|
||
\label{anx:proofTyptyp}
|
||
|
||
Cette section a pour but de présenter la preuve complète du \autoref{thm:tiTyp}, sur la cohérence du typage des \eng{test interfaces}.
|
||
|
||
Nous avons $\mathfrak{T}$ une \eng{test interface}, $\mathcal{C}$ une \eng{class table} telle que $\mathcal{A} \triangleright \mathfrak{T}$ et $(\mathcal{B}, e)$ un programme test, tel que $\mathcal{B}\OKin\mathfrak{T}$.
|
||
|
||
Nous allons donc essayer de montrer, par induction sur la preuve de la prémisse, la propriété suivante
|
||
|
||
\[\mathfrak{T},\mathcal{B}, \Gamma \Vdash e : \fj{C} \implies \exists \fj{C'}\quad \mathcal{A}\oplus\mathcal{B},\Gamma \vdash e : \fj{C'} \quad\text{et}\quad \fj{C'} \subclass \fj{C}\]
|
||
|
||
\subsection{Propriétés sur les fonctions utilitaires}
|
||
|
||
La définition de $\vdash$ dans Featherweight Java de base utilise les fonctions utilitaires non surchargées. Afin de bien les différencier, nous allons noter avec un prime les versions surchargées définies \autoref{fig:typops}.
|
||
|
||
Par exemple, $(\operatorname{fields'})$ correspond à la définition surchargée dans la \eng{test interface} $\mathfrak{T}$ et la \eng{class table} de tests $\mathcal{B}$, et $(\operatorname{fields})$ correspond à la définition originale dans la \eng{class table} $\mathcal{A} \oplus \mathcal{B}$. Il en va de même pour l' opérateur $(\subclass')$, qui dénotera la cloture transitive et réflexive de l'union des relations \fj{<:} sur $\mathfrak{T}$ et \fj{extends} dans $\mathcal{B}$ et l'opérateur $(\subclass)$ qui dénotera la relation de sous-typage sur la \eng{class table} $\mathcal{A} \oplus \mathcal{B}$.
|
||
|
||
Nous allons déjà montrer les trois propriétés suivantes sur ces fonctions utilitaires:
|
||
|
||
\[
|
||
\begin{array}{rcl}
|
||
\fj{C}\;\fj{f} \in \operatorname{fields'}(\fj{C0}) &\implies& \exists \fj{C'}\subclass\fj{C}\quad\fj{C'}\;\fj{f} \in \operatorname{fields}(\fj{C0}) \\
|
||
\operatorname{mtype'}(\fj{m},\fj{C0}) = \overline{\fj{D}}\rightarrow\fj{C} & \implies& \exists \fj{C'}\subclass \fj{C}\ \exists \overline{\fj{D'}} \superclass \overline{\fj{D}}\quad \operatorname{mtype}(\fj{m},\fj{C0}) = \overline{\fj{D'}}\rightarrow\fj{C'}\\
|
||
\operatorname{construct'}(\fj{C0}) = \overline{\fj{D}} & \implies & \exists \overline{\fj{D'}} \superclass \overline{\fj{D}}\quad\exists \overline{\fj{f}} \quad \operatorname{fields}(\fj{C0}) = \overline{\fj{D'}}\;\overline{\fj{f}}
|
||
\end{array}
|
||
\]
|
||
|
||
\paragraph{Première propriété}
|
||
Montrons cette propriété par induction sur la relation $\subclass'$.
|
||
|
||
En inversant la règle qui a permis de prouver $\fj{C}\;\fj{f} \in \operatorname{fields'}(\fj{C0})$, il y a quatre possibilités.
|
||
|
||
\subparagraph{Cas $\fj{C}\;\fj{f} \in \bigcup_{\fj{C}\subclass'\fj{E}}\operatorname{fields'}(\fj{E})$}
|
||
On applique alors directement l’hypothèse d'induction.
|
||
|
||
\subparagraph{Cas $\fj{class C0 \{C f;...\}} \in \mathcal{B}$ (\textnormal{\ref{rule:lct-fields})}}
|
||
Alors, par construction de $\operatorname{fields}$, on a $\fj{C}\;\fj{f} \in \operatorname{fields}(C0)$
|
||
|
||
\subparagraph{Cas $\left[\fj{C0 \{C f, ...\}}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-fields})}}
|
||
Alors, puisque $\mathcal{A} \triangleright \mathfrak{T}$, c'est nécessairement par la règle \ref{rule:tri:attributes}, et on a donc
|
||
\[\fj{C'} \fj{f} \in \operatorname{fields}_\mathcal{A}(\fj{C0})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\]
|
||
|
||
\subparagraph{Cas $\left[\fj{C0 (..., C f, ...)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-fields2})}}
|
||
Alors, puisque $\mathcal{A} \triangleright \mathfrak{T}$, c'est nécessairement par la règle \ref{rule:tri:constructor}, et on a donc, puisque le field \fj{f} est défini,
|
||
\[\fj{C'} \fj{f} \in \operatorname{fields}_\mathcal{A}(\fj{C0})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\]
|
||
|
||
\paragraph{Seconde propriété}
|
||
Procédons un peu de la même manière, par induction sur la définition de $\operatorname{mtype'}$.
|
||
|
||
Nous avons comme hypotèse $\operatorname{mtype'}(\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{C}$.
|
||
|
||
\subparagraph{Cas $\left[\fj{C0 : C m($\overline{\texttt{D}}$)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-method})}}
|
||
Alors, puisque $\mathcal{A} \triangleright \mathfrak{T}$, c'est nécessairement par la règle \ref{rule:tri:method}, et on a donc.
|
||
\[\operatorname{mtype}_\mathcal{A}(\fj{m},\fj{C}) = \overline{\fj{D'}} \rightarrow \fj{C'}\quad;\quad\overline{\fj{D}} \subclass \overline{\fj{D'}}\quad;\quad \fj{C'}\subclass\fj{C}\]
|
||
CQFD.
|
||
|
||
\subparagraph{Cas $\fj{class C0 \{...,C m($\overline{\texttt{D}}\;\overline{\texttt{x}}$)\}}\in \mathcal{B}$ (\textnormal{\ref{rule:lct-method}})}
|
||
Alors, par définition de $\operatorname{mtype}$, on a que
|
||
\[\operatorname{mtype}_\mathcal{B}(\fj{m},\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{E}\quad\text{et}\quad\fj{C0}\subclass\fj{C0}\]
|
||
CQFD.
|
||
\subparagraph{Cas $\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}} \rightarrow \fj{E}$ et $\fj{C}\subclass'\fj{C0}$ (\textnormal{\ref{rule:lup-method}})}
|
||
|
||
\label{proof:mtype:cchain}
|
||
Puisque $\fj{C}\subclass'\fj{C0}$, alors, il existe une chaine de classes
|
||
\[\fj{C} = \fj{C}_0 , \fj{C}_1 , \dots , \fj{C}_n = \fj{C0}\]
|
||
|
||
telles que $\fj{C}_k\;\fj{extends}\;\fj{C}_{k+1}$ dans $\mathcal{A}$ ou $\mathcal{B}$.
|
||
|
||
Or, on sait que les défintions de $\mathcal{A}$ et $\mathcal{B}$ sont $\textsc{OK}$ (c'est imposé par la définition de $\mathcal{A}\triangleright\mathfrak{T})$.
|
||
On a donc que pour chacune de ces classes:
|
||
|
||
\[\operatorname{mtype}(\fj{m},\fj{C}_n) = \operatorname{mtype}(\fj{m},\fj{C}_{n-1}) = \cdots = \operatorname{mtype}(\fj{m},\fj{C}_0)\]
|
||
|
||
Donc $\operatorname{mtype}(\fj{m},\fj{C0}_n) = \overline{\fj{D}}\rightarrow \fj{E}$. CQFD
|
||
|
||
\paragraph{Troisième propritété}
|
||
|
||
Une dernière fois, inversons la règle qui a permis de prouver $\operatorname{construct'}(\fj{C0}) = \overline{\fj{D}}$.
|
||
|
||
\subparagraph{Cas $\left[\fj{C0 ($\overline{\texttt{D}}\;\overline{\texttt{f}}$)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-construct})}}
|
||
|
||
Alors, puisque $\mathcal{A} \triangleright \mathfrak{T}$, c'est nécessairement par la règle (\ref{rule:tri:constructor}), et on a donc
|
||
\[\exists \overline{\fj{D'}}\quad\overline{\fj{D'}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)\]
|
||
CQFD
|
||
|
||
\subparagraph{Cas $\fj{class C0\{C0($\overline{\texttt{D}}\;\overline{\texttt{f}}$)\{...\} ... \}}\in \mathcal{B}$ (\textnormal{\ref{rule:lct-construct}})}
|
||
|
||
Alors, puisqu'en Featherweight Java, les objets sont immuables et les constructeurs définissent tous les fields, on sait que les paramètres du constructeurs sont \emph{exactement} les champs de la classe. Et donc
|
||
|
||
\[\operatorname{fields}(\fj{C0}) = \overline{\fj{D}} \quad\text{et}\quad \overline{\fj{D}} \subclass \overline{\fj{D}}\]
|
||
|
||
\subsection{Corps de la preuve}
|
||
|
||
Démarrons l'induction sur la preuve de la propriété présentée au début de la section.
|
||
|
||
\subparagraph{\textnormal{\textsc{\ref{rule:ti:variable}}}}
|
||
|
||
\begin{hyps}
|
||
\item e = \fj{x}
|
||
\item \fj{C} = \Gamma(\fj{x})
|
||
\item \fj{x} \in \operatorname{dom}(\Gamma)
|
||
\end{hyps}
|
||
|
||
Alors, d'après la règle FJ \textsc{T-Var}
|
||
\[\mathcal{A}\oplus\mathcal{B},\Gamma \vdash \fj{x} : \Gamma(\fj{x})\]
|
||
|
||
\subparagraph{\textnormal{\textsc{\ref{rule:ti:field}}}}
|
||
\begin{hyps}
|
||
\item e = \fj{$e_0$.f}
|
||
\item \fj{C} = \fj{C}
|
||
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash e_0 : \fj{C0} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash e_0 : \fj{C0'}\quad\text{et}\quad \fj{C0'}\subclass\fj{C0}
|
||
\item \fj{C}\;\fj{f} \in \operatorname{fields'}(\fj{C0})
|
||
\end{hyps}
|
||
|
||
On peut alors appliquer la première propriété sur la quatrième hypotèse qui nous donne
|
||
\[\exists\fj{C'}\subclass \fj{C} \quad \fj{C'}\;\fj{f} \in \operatorname{fields}(\fj{C0})\]
|
||
|
||
Alors, on peut directement appliquer la règle FJ \textsc{T-Field}
|
||
|
||
\subparagraph{\textnormal{\textsc{\ref{rule:ti:invoke}}}}
|
||
\begin{hyps}
|
||
\item e = \fj{$e_0$.m($\overline{e_x}$)}
|
||
\item \fj{C} = \fj{C}
|
||
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash e_0 : \fj{C0} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash e_0 : \fj{C0'}\quad\text{et}\quad \fj{C0'}\subclass\fj{C0}
|
||
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash \overline{e_x} : \overline{\fj{CX'}}\quad\text{et}\quad \overline{\fj{CX'}}\subclass\overline{\fj{CX}}
|
||
\item \operatorname{mtype'}(\fj{m},\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{C}
|
||
\item \overline{\fj{CX}} \subclass \overline{\fj{C}}
|
||
\end{hyps}
|
||
|
||
On peut alors appliquer la seconde propriété sur la cinquième hypothèse, on obtient que
|
||
\[\operatorname{mtype}(\fj{m}, \fj{C0}) = \overline{\fj{D'}} \rightarrow \fj{C'} \quad\text{et}\quad \overline{\fj{D}}\subclass\overline{\fj{D'}}\quad\text{et}\quad\fj{C'}\subclass\fj{C}\]
|
||
|
||
Alors, en utilisant la même preuve que pendant la preuve de la sous propriété (\autoref{proof:mtype:cchain})
|
||
|
||
\[\operatorname{mtype}(\fj{m},\fj{C0'}) = \overline{\fj{D'}}\rightarrow\fj{C'} \quad\text{et}\quad \overline{\fj{CX'}} \subclass \overline{\fj{CX}} \subclass \overline{\fj{D}} \subclass \overline{\fj{D'}}\]
|
||
|
||
On peut maintenant appliquer la règle FJ \textsc{T-Invk} et obtenir le résultat.
|
||
|
||
\subparagraph{\textnormal{\textsc{\ref{rule:ti:new}}}}
|
||
\begin{hyps}
|
||
\item e = \fj{new C($\overline{e_x}$)}
|
||
\item \fj{C} = \fj{C}
|
||
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash \overline{e_x} : \overline{\fj{CX'}}\quad\text{et}\quad \overline{\fj{CX'}}\subclass\overline{\fj{CX}}
|
||
\item \operatorname{construct'}(\fj{C}) = \overline{\fj{D}}
|
||
\item \overline{\fj{CX}} \subclass \overline{\fj{D}}
|
||
\end{hyps}
|
||
|
||
On peut appliquer la troisième propriété sur la quatrième hypothèse. On obtient alors que :
|
||
\[\operatorname{fields}(\fj{C}) = \overline{\fj{D'}}\;\overline{\fj{f}} \quad\text{et}\quad \overline{\fj{CX'}} \subclass \overline{\fj{CX}} \subclass \overline{\fj{D}} \subclass \overline{\fj{D'}}\]
|
||
|
||
On peut maintenant appliquer la règle FJ \textsc{T-New} et obtenir le résultat.
|
||
|
||
\subparagraph{\textnormal{\textsc{\ref{rule:ti:upCast}}}}
|
||
\begin{hyps}
|
||
\item e = \fj{(C)$e_0$}
|
||
\item \fj{C} = \fj{C}
|
||
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash e_0 : \fj{C} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash e_0 : \fj{D}\quad\text{et}\quad \fj{D}\subclass\fj{C}
|
||
\item \fj{D} \subclass \fj{C}
|
||
\end{hyps}
|
||
|
||
On a alors l'inégalité suivante :
|
||
\[\fj{D'} \subclass \fj{D} \subclass \fj{C}\]
|
||
|
||
On peut donc appliquer directement la règle \textsc{T-UCast}
|
||
|
||
\subparagraph{\textnormal{\textsc{\ref{rule:ti:downCast}}}}
|
||
Exactement la même preuve que le point précédent en appliquant la règle \textsc{T-UCast}
|
||
|
||
\section{Preuve du \eng{context lemma} avec les valeurs infinies}
|
||
\label{anx:proofHValCL}
|
||
|
||
Nous allons démontrer une version un peu plus puissante de ce théorème, ce qui simplifiera l'induction que nous ferrons.
|
||
|
||
Tout d'abord, nous allons définir quelques notations locales à cette preuve.
|
||
|
||
Déjà, nous ne spécifierons pas la \eng{class table}, puisque nous supposerons que nous travaillerons dans la \eng{class table} $\mathcal{A} \oplus \mathcal{B}$, car puisque le $\oplus$ impose que les noms de classe n'entrent pas en collision, si un expression s’exécutant dans $\mathcal{A}$ ou $\mathcal{B}$ s'executera de la même façon dans $\mathcal{A}\oplus\mathcal{B}$.
|
||
|
||
$h$ définira une expression FJ possédant des variables libres (càd, des nœuds de la forme \fj{x}). Bien que ce soient techniquement des expressions FJ, nous les dénoterons ainsi afin de ne pas les confondre avec les expressions \enquote{fermées}, dénotées elles $e$,$f$.
|
||
|
||
Nous allons ausssi noter $\varepsilon$, $\gamma$ les \eng{mappings} d'un ensemble de noms de variables vers un ensemble d'expressions fermées. On va ainsi définir la complétion d'une expression ayant des variables libres par un de ces \eng{mappings}, ce qui sera noté $h\bracket{\varepsilon}$ où l'on remplace chaque occurrence d'une variable par l'image par $\varepsilon$ de ce nom de variable.
|
||
|
||
On note toujours le préordre entre deux expressions fermées de la même façon:
|
||
\[e \prec f \ssi \forall\hbar \quad (\exists \overline{e'}\quad e \rightarrow \hbar\bracket{\overline{e'}}) \implies (\exists \overline{f'}\quad f \rightarrow \hbar\bracket{\overline{f'}})\]
|
||
|
||
Nous allons aussi étendre cette définition à deux \eng{mappings} ayant le même domaine:
|
||
\[\varepsilon \prec \gamma \ssi \forall \fj{x}\in\operatorname{Dom}(\varepsilon)=\operatorname{Dom}(\gamma)\quad \varepsilon(\fj{x}) \prec \gamma(\fj{x})\]
|
||
\marginpar{Un exemple d'utilisation de ces notations est-il nécessaire ?}
|
||
|
||
Le théorème, plus général que nous allons montrer est le suivant:
|
||
|
||
\begin{theorem}
|
||
Pour $\varepsilon$, $\gamma$ des \eng{mappings} de même domaine\\
|
||
Pour $h$ expression avec des variables libres tel que $\operatorname{Var}(h) \subset \operatorname{Dom}(\varepsilon)$\\
|
||
Si $\varepsilon \prec \gamma$\\
|
||
Alors $h\bracket{\varepsilon} \prec h\bracket{\gamma}$\\
|
||
C'est à dire \[\forall \hbar \left(\exists e'\quad h\bracket{\varepsilon}\rightarrow^* h\bracket{e'}\right)\implies\left(\exists f'\quad h\bracket{\gamma}\rightarrow^* h\bracket{f'}\right)\]
|
||
\end{theorem}
|
||
|
||
|
||
|
||
|
||
\end{document}
|