1203 lines
83 KiB
TeX
1203 lines
83 KiB
TeX
% !TeX spellcheck = fr_FR
|
||
\documentclass[10pt,a4paper]{article}
|
||
|
||
\include{./header.tex}
|
||
|
||
\title{Définition d'un préordre sur les programmes Featherweight Java
|
||
\\[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
|
||
\\[1ex] Daniele Varacca (LACL, UPEC)
|
||
\\[1ex] et Clément Aubert (Augusta University, Géorgie)}
|
||
|
||
\begin{document}
|
||
\doparttoc
|
||
\maketitle
|
||
|
||
\hsep
|
||
|
||
\tableofcontents
|
||
|
||
\newpage
|
||
|
||
\section{Introduction}
|
||
|
||
Ce document a été réalisé dans le cadre de mon stage réalisé au LACL à Créteil, plus de détails sont donnés en \autoref{anx:stage}.
|
||
|
||
\subsection{Présentation du problème}
|
||
Featherweight Java (abrégé en FJ) \cite{fjdef} est une formalisation de la programmation en orienté objet (POO). Les programmes FJ ont leur syntaxe calquée sur celle du langage Java, et sont compilables avec un compilateur classique. On peut y définir classes, attributs et méthodes, mais pas d'assignation, les objets considérés étant tous immuables.
|
||
|
||
Le FJ est un bon cas d'étude, si l'on veut étudier formellement un phénomène d'informatique théorique, comme la compilation, le typage incrémental \cite{kuci_et_al:cocoTypecheck}, la généricité/polymorphisme ou la possession d'objets, et ce dans un langage orienté objet, paradigme utilisé dans la plupart des langages actuels (Java, Python, C++, ...).
|
||
|
||
Nous allons utiliser ce langage pour étudier les équivalences entre des programmes, qui n'ont, à notre connaissance, jamais été étudiées en FJ. Trouver une équivalence, cela signifie essayer de dire formellement que deux programmes \enquote{font la même chose}. Cela peut être utile afin de vérifier si une optimisation temporelle, mémorielle ou sécuritaire d'un programme ne change pas son fonctionnement.
|
||
|
||
L'objectif du stage est donc de définir une équivalence (ou plutôt un préordre) entre les programmes FJ et d'essayer d'obtenir des théorèmes utiles sur la nouvelle relation \cite{picalcul_sangiorgi}.
|
||
|
||
\subsection{Motivations de l'étude}
|
||
Mes tuteurs de stage, Daniele Varacca et Clément Aubert, s’intéressent aux équivalences de programmes et à comment les \eng{process calculis} peuvent fournir des nouvelles équivalences à d'autres langages \cite{papierContextEquiv}.
|
||
|
||
Mon objectif était alors de fournir une réflexion sur une étude de cas (le Featherweight Java), afin d'ensuite pouvoir étudier la manière dont mon exploration \enquote{naïve} mais néanmoins approfondie peut-être rapprochée de leur méthode, pouvant ainsi la valider, ou au contraire fournir d'autres éléments afin de la consolider.
|
||
|
||
\subsection{Plan de ce rapport}
|
||
Je fais \autoref{sec:defNots} quelques rappels formels de la définition du Featherweight Java, accompagnés de quelques nouvelles grammaires qui seront utilisées dans ce document. Je vais ensuite présenter \autoref{sec:eqsimpl} quelques unes des équivalences, les plus \enquote{évidentes}, que j'ai considérées afin d'étudier leurs propriétés et d'expliciter leurs problèmes. Ces problèmes, qu'ils soient propres à FJ ou non, devraient être résolus par une \enquote{bonne} définition d'équivalence. Enfin, la \autoref{sec:titech} décrira techniquement la relation d'équivalence à laquelle je suis arrivé après toutes ces considérations, et finira par un exemple pratique.
|
||
|
||
\section{Définitions et notations}
|
||
\label{sec:defNots}
|
||
\subsection{Rappel sur la définition de Featherweight Java}
|
||
|
||
Dans cette section, je vais rappeler quelques notations et définitions du langage Featherweight Java \cite{fjdef}. Le lecteur souhaitant toutes les définitions complètes devra lire \cite[Section 1]{fjdef}.
|
||
|
||
On utilisera la notation du sur-lignage afin d'indiquer une liste finie d'éléments.
|
||
Par exemple,
|
||
\[f(\overline{a})\quad\equiv\quad f(a_1,a_2,\dots,a_n)\]
|
||
|
||
On rappelle la grammaire des expressions, notées $e$, $e_k$ ou $e'$ :
|
||
|
||
\begin{center}
|
||
\refstepcounter{rule}
|
||
\begin{tabular}{rll}
|
||
$e$ $:=$ & \fj{x} & \qquad \newtag{\textrm{\textsc{E-Var}}}{rule:expr:variable} \\
|
||
| & \fj{new C($\overline{e}$)} & \qquad \newtag{\textrm{\textsc{E-Cstr}}}{rule:expr:constructor} \\
|
||
| & \fj{$e$.f} & \qquad \newtag{\textrm{\textsc{E-Field}}}{rule:expr:field} \\
|
||
| & \fj{$e$.m($\overline{e}$)} & \qquad \newtag{\textrm{\textsc{E-Meth}}}{rule:expr:method} \\
|
||
| & \fj{(C)$e$} & \qquad \newtag{\textrm{\textsc{E-Cast}}}{rule:expr:cast}
|
||
\end{tabular}
|
||
\end{center}
|
||
où \fj{x} est un nom de variable, \fj{C} un nom de classe, \fj{f} un nom d'attribut de classe et \fj{m} un nom de méthode de classe.
|
||
|
||
On dit d'une expression qui ne contient pas de référence à des variables (\autoref{rule:expr:variable}) qu'elle est \emph{fermée}. Dans la suite du document, nous allons utiliser le terme \enquote{expression} pour désigner les expressions fermées. Les expressions quelconques seront désignées par \emph{expressions ouvertes} ou \emph{expressions à variables}, parfois notées $h$.
|
||
|
||
Le langage définit aussi des classes, qui sont composées d'un nombre quelconque d'attributs nommés dont le type est spécifié, d'un unique constructeur qui prend autant de paramètres que la classe a d'attributs et qui définit tous ces derniers, et d'un nombre quelconque de méthodes ayant un nom, un type de retour, des paramètres ayant chacun un nom et un type et surtout un corps, qui est une expression ouverte utilisant les noms de variable décrits dans les paramètres plus éventuellement le nom de variable spécial \fj{this} désignant l'objet duquel la méthode est appelée. Les classes ont aussi une classe mère, par défaut la classe \fj{Object} de laquelle elles héritent les attributs et les méthodes, qu'elles peuvent surcharger sans changer leur type.
|
||
|
||
On appellera \eng{class table} tout ensemble de définitions de classes, et on les notera $\mathcal{A}$, $\mathcal{B}$, $\mathcal{C}$. Par convention, les noms de classes seront écrit en \verb*|CamelCase| (majuscule) et les noms de méthodes, attributs (\eng{fields}) et variables en \verb*|camelCase| (minuscule).
|
||
|
||
Un \emph{programme} Featherweight Java est un couple $(\mathcal{A},e)$, noté $P$, $Q$, $R$. L'expression est en quelque sorte le \eng{main} du programme.
|
||
|
||
On appelle \enquote{valeur} toute expression composée uniquement de constructeurs (\autoref{rule:expr:constructor}).
|
||
|
||
On note $\vdash$ la relation de typage. \enquote{$\mathcal{A},\Gamma \vdash e : \fj{C}$} indiquera que l'expression $e$ avec l'environnement de typage $\Gamma$ (un ensemble d'entrées de type $e : \fj{C}$) est typée par la classe \fj{C} sous la \eng{class table} $\mathcal{A}$.
|
||
|
||
Notez qu'une \eng{class table} n'est pas nécessairement typée. En effet, toutes les classes sont définies individuellement, et c'est le typage de la \eng{class table} complète qui les lie et qui leur donne leur cohérence. Cette propriété nous permet de considérer des \eng{class tables} partielles, qui seront ensuite accolées à d'autres pour être bien typées. FJ définit la notation $\mathcal{A}\;\texttt{OK}$ pour indiquer que la \eng{class table} $\mathcal{A}$ est bien typée. On notera aussi souvent la concaténation de deux \eng{class tables} qui définissent des noms de classe \emph{distincts} $\mathcal{A} \oplus \mathcal{B}$.
|
||
|
||
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’ambigüité. On notera aussi $\rightarrow^*_\mathcal{A}$ ou $\rightarrow^*$ la clôture transitive et réflexive de la relation. On notera enfin $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$.
|
||
|
||
Cette relation est définie avec deux types de règles \cite[Fig. 3]{fjdef}, 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 \eng{cast} (\textsc{R-Cast})
|
||
\end{itemize}
|
||
Et 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}
|
||
\caption{Définition de la classe Paire}
|
||
\label{fig:pairedef}
|
||
\end{figure}
|
||
\subsection{Définitions et raccourcis de programmation}
|
||
|
||
Nous allons définir en sus la grammaire des expressions à (un seul) trou notés $h$, $h'$:
|
||
\[h := \hole \spacebar \fj{new C($\overline{e}$,$h$,$\overline{e}$)} \spacebar \fj{$h$.f} \spacebar \fj{$h$.m($\overline{e}$)} \spacebar \fj{$e$.m($\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 quelconque, définie récursivement:
|
||
|
||
\begin{align*}
|
||
\hole[e] &= e\\
|
||
(\fj{new C($\overline{e_1}$,$h$,$\overline{e_2}$)})[e] &= \fj{new C($\overline{e_1}$,$h[e]$,$\overline{e_2}$)}\\
|
||
(\fj{$h$.f})[e] &= \fj{$h[e]$.f}\\
|
||
(\fj{$h$.m($\overline{e_1}$)})[e] &= \fj{$h[e]$.m($\overline{e_1}$)}\\
|
||
(\fj{$e_1$.m($\overline{e_2}$,$h$,$\overline{e_3}$)})[e] &= \fj{$e_1$.m($\overline{e_2}$,$h[e]$,$\overline{e_3}$)}\\
|
||
(\fj{(C) $h$})[e] &= \fj{(C) $h[e]$}
|
||
\end{align*}
|
||
|
||
Nous allons ausssi noter $\alpha$,$\beta$,$\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 à variables par un de ces \eng{mappings}, ce qui sera noté $h\bracket{\alpha}$ où l'on remplace chaque occurrence d'une variable par l'image par $\alpha$ de ce nom de variable.
|
||
|
||
Au niveau de la programmation FJ, 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 directement, ce qui correspond en pratique à autoriser des expressions de la forme \fj{meth($\overline{e}$)}, et de les remplacer par \fj{new Static().meth($\overline{e}$)}.
|
||
|
||
Enfin nous définissons plusieurs classes qui permettent de coder de façon plus abstraite, 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 objets notés \fj{true} et \fj{false}. Cette classe met à disposition une méthode \enquote{if then else} \fj{ite(Object,Object)} construite telle que \fj{true.ite($e_t$,$e_f$)} renvoie $e_t$ et \fj{false.ite($e_t$,$e_f$)} renvoie $e_f$.
|
||
|
||
La seconde classe est \fj{Int}, liée à des objets notés \fj{0}, \fj{1}, \fj{2}, \dots. Cette classe met a disposition une méthode \fj{Bool isZero()} qui renvoie \fj{true} si l'objet appelant est zéro, et renvoie \fj{false} sinon. 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éfinirons souvent implicitement les classes \fj{A}, \fj{B} et \fj{C}, qui n'ont pas d'attribut et pas de méthode (ce sont des \enquote{objets simples}).
|
||
|
||
\section{Étude d'équivalences simples}
|
||
\label{sec:eqsimpl}
|
||
Dans cette section, je vais présenter les équivalences les plus simples et présenter les problèmes que je leur ai trouvé. Cette section n'a pas pour objectif de construire des théorèmes accompagnés de leurs preuves complètes, mais elle vise à donner au lecteur l'intuition sur les propriétés souhaitables pour un préordre sur les programmes FJ.
|
||
|
||
\subsection{Explication de l'utilité d'un contexte}
|
||
|
||
Les équivalences entre les programmes sont habituellement définies en utilisant des structures appelées \enquote{contextes}. Deux 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 $P$ 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.
|
||
|
||
Dans des langages formels basés sur une simple expression, comme le λ-calcul ou le π-calcul, cette notion de contexte fonctionne bien. Il suffit de bien la formaliser puis d'étudier ses propriétés \cite{picalcul_sangiorgi}. Cependant, en FJ, un programme n'est pas constitué que d'une expression. Une expression seule n'a d'ailleurs aucun sens si elle n'est pas associée à une \eng{class table}. Il faut donc construire un contexte qui tienne compte de l'ensemble du programme.
|
||
|
||
\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'interprétation d'un programme $P = (\mathcal{A},e)$ dans un contexte $C$ est alors
|
||
\[C\bracket{P} = (\mathcal{A},h\bracket{e})\]
|
||
|
||
Le \emph{premier} 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. Un exemple de deux \eng{class tables} qui ne peuvent être différenciées que à l'aide d'une \eng{class table} supplémentaire \enquote{de tests} est donnée \autoref{anx:exmpl:cttest}.
|
||
|
||
Le \emph{second} problème est que les expressions peuvent observer de manière trop précise et profonde la \eng{class table} est ainsi les distinguer au moindre changement de nom de classe, de nom d'attribut ou de nom de méthode.
|
||
On peut s'en convaincre en considérant les \eng{class tables} qui contiennent des trous dégénérés, c'est à dire celles vérifiant
|
||
\[\forall e \exists h \forall p \quad h\bracket{p} \rightarrow^*e\]
|
||
Un exemple de trou dégénéré est l'expression trouée suivante donnée pour $e$ expression, dans n'importe quelle \eng{class table} contenant la classe \fj{Paire} :
|
||
\[\fj{new Paire($\hole$,$e$).snd} \rightarrow e\]
|
||
|
||
Avec un trou dégénéré, on peut alors \enquote{jeter} le \eng{main} du programme, et comparer les deux \eng{class tables} sur n'importe quelle expression. Le \eng{main} du programme n'a plus d'effet. On peut donc évaluer pour chaque nom de classe $\fj{C}$ l'expression \fj{new C(new D(...), ..., new 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} (et que ces types sont instanciables, c'est à dire qu'il existe une valeur de ce type). 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 utiliserait une classe \fj{Tree} et une autre qui utiliserait une classe \fj{Map}. Puisqu'il n'y a pas d'\eng{access control} en FJ, un utilisateur malveillant aurait accès à tous ces outils pour mettre en défaut le programme.
|
||
|
||
La relation créée en utilisant de simples expressions à trou comme contextes est ainsi robuste, mais trop restrictive pour être utile.
|
||
|
||
\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} supplémentaire dite «de tests». Ainsi, l'application du contexte $C = (\mathcal{C},h)$ au programme $P = (\mathcal{A}, e_P)$ donne
|
||
\[C\bracket{P} = (\mathcal{C} \oplus \mathcal{A},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 = (\mathcal{A}, e_P) \prec Q = (\mathcal{B}, e_Q) \iff \forall C=(\mathcal{C}, e_C)\quad
|
||
\begin{dcases}\mathcal{A} \prec \mathcal{C}\\ \mathcal{B} \prec \mathcal{C} \\
|
||
\forall v\quad C\bracket{P}\Downarrow v \implies C\bracket{Q}\Downarrow v\end{dcases} \]
|
||
|
||
Cependant, cette définition pose un problème lorsque l'on cherche à comparer 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}
|
||
\caption{\eng{Class tables} n'ayant pas de sur-\eng{class table} commune}
|
||
\label{fig:nosurct}
|
||
\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}\]
|
||
|
||
Alors, puisque aucun de nos \emph{contextes} ne satisfait les hypothèses, les deux programmes sont équivalents trivialement.
|
||
|
||
\section{Des tests plus ciblés}
|
||
\label{sec:titech}
|
||
\paragraph{Abandon de l'expression \fj{main}}
|
||
|
||
Tous les tests présentés 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, un développeur souhaitera principalement comparer entre elles des librairies, ce qui correspondrait à 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. La transformation est présentée \autoref{fig:prgToCT}.
|
||
|
||
\begin{figure}
|
||
\begin{center}
|
||
\begin{multicols}{2}
|
||
\null\vfill
|
||
\begin{fjlisting}[width=.4\textwidth]
|
||
class XXX extends XXX \{\\
|
||
\}\\
|
||
\vdots\\
|
||
\fjmain{expression}
|
||
\end{fjlisting}
|
||
\vfill\null
|
||
\columnbreak
|
||
\begin{fjlisting}[width=.4\textwidth]
|
||
class XXX extends XXX \{\\
|
||
\}\\
|
||
\vdots\\
|
||
\fjclass{Main}{}{
|
||
\fjmethod{Object}{main}{}{expression}
|
||
}
|
||
\end{fjlisting}
|
||
\end{multicols}
|
||
\end{center}
|
||
\caption{Transformation d'un programme en \eng{class table}}
|
||
\label{fig:prgToCT}
|
||
\end{figure}
|
||
Alors, on a transformé le \emph{programme} en \emph{\eng{class table}}, et si nous voulons tester le main du programme, il suffit de tester ce que renvoie l'expression \fj{new Main().main()}, qui se réduit en une étape en le main du programme.
|
||
|
||
\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 aimerait 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 (que certaines extensions du FJ considèrent \cite{liquori_fjInterfaces}), sauf que les \eng{test interface} ne serviront que lors de la compilation. Une expression va être \enquote{compilée} (c'est à dire être typée) avec l'interface, puis sera \enquote{exécutée} (c'est à dire réduite) avec 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 \eng{test interface} est alors simplement un ensemble de \eng{test interface rules}, et sera notée $\mathfrak{T}$, $\mathfrak{U}$, $\mathfrak{V}$. La \autoref{rule:tsg:method} permet de déclarer une méthode dans une 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 qu'une classe doit être un sous-type d'une autre. Et donc, une \eng{class table} implémente une \eng{test interface} lorsqu'elle respecte chacune de ses règles.
|
||
|
||
\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{TIG-Meth}}}{rule:tsg:method} \\
|
||
| & C \{$\overline{\fj{C}}$ $\overline{\fj{f}}$\} & \qquad \newtag{\textrm{\textsc{TIG-Attr}}}{rule:tsg:attributes} \\
|
||
| & C ($\overline{\fj{C}}$ $\overline{\fj{?}\fj{f}}$) & \qquad \newtag{\textrm{\textsc{TIG-Cstr}}}{rule:tsg:constructor} \\
|
||
| & C <: C & \qquad \newtag{\textrm{\textsc{TIG-Cast}}}{rule:tsg:cast}
|
||
\end{tabular}
|
||
\end{center}
|
||
\end{tcolorbox}
|
||
\rmfamily
|
||
$\overline{\fj{?}\fj{f}}$ désigne une liste d'éléments qui sont ou bien vides, ou bien un nom d'attribut, par exemple $\fj{f1}, vide, vide, \fj{f2}$
|
||
\caption{Grammaire des \eng{Test Interface rules}}
|
||
\label{fig:tigrammaire}
|
||
\end{figure}
|
||
|
||
Un exemple concret de \eng{test interface} est donné \autoref{fig:tiexample}. Elle impose la déclaration des classes \fj{Int}, \fj{Frac}, \fj{Number} et \fj{RichInt} telles que l'on puisse appeler certaines méthodes sur elles. Elle impose aussi de pouvoir construire les object \fj{Frac} avec deux paramètres de type \fj{Int}, et elle impose aussi un attribut nommé \fj{value} dans la classe \fj{RichInt}.
|
||
|
||
\begin{figure}
|
||
\begin{fjlisting}
|
||
Number \{\}\\\null
|
||
|
||
Int \{\}\\
|
||
Int : Int suivant(Int)\\
|
||
Int : Int add(Int,Int)\\
|
||
Int <: Number\\\null
|
||
|
||
Frac(Int numerateur, Int denominateur)\\
|
||
Frac : Frac inverted()\\
|
||
Frac : Int floor()\\
|
||
Frac <: Number\\\null
|
||
|
||
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 ou bien une \autoref{rule:tsg:attributes} ou bien 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 \fj{Object}).
|
||
\end{itemize}
|
||
|
||
Cette 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 \{\}}.
|
||
|
||
Les deux règles \ref{rule:tsg:attributes} et \ref{rule:tsg:constructor} sont donc mutuellement exclusives pour un nom de classe donné. Leur différence est que la seconde autorise le développeur à appeler le constructeur \fj{new C(...)} et impose la position de chaque attribut déclaré dans les paramètres du constructeur. Il impose aussi le nombre d'attributs de la classe (en prenant en compte l'hérédité). La première n'autorise pas l'utilisation du constructeur, et n'impose donc pas d'ordre sur ses paramètres.
|
||
|
||
Il peut sembler au premier abord qu'il manque à cette définition des \eng{test interfaces} une façon d'autoriser le programmeur à utiliser un constructeur, sans en imposer l'ordre des paramètres, mais en autorisant l'accès à certains attributs. Pourtant, si l'on peut construire et accéder à un certain attribut \fj{field} sur un type \fj{C}, et que 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 une expression qui nous indique la position dans le constructeur de l'attribut.
|
||
Pour ce faire, il faut, pour chaque nom de classe \fj{Pk} des paramètres, créer 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{Pj\_k}, et on aura ainsi accès à la position dans le 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}\]
|
||
|
||
Nous allons aussi considérer uniquement les \eng{test interfaces} 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 complexes à exprimer apparaissent, nous n'allons pas chercher à les exprimer ici, mais vous trouverez des contre-exemples de \eng{test interfaces} en \autoref{fig:tiUnsolvable}
|
||
|
||
\begin{figure}
|
||
\begin{center}
|
||
\begin{tabular}{ccc}
|
||
\begin{fjlisting}[width=.3\textwidth]
|
||
\setlength{\columnseprule}{1pt}
|
||
\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}
|
||
\underline{La première} parce que la relation de sous-typage et transitive est antisymétrique.
|
||
|
||
\underline{La seconde} parce que si \fj{B} a un attribut de type \fj{A}, alors \fj{C} en hérite, et ne peut pas être construit sans attributs.
|
||
|
||
\underline{La troisième} comme la précédente, parce que \fj{C} devrait avoir par héritage un attribut nommé \fj{f}.
|
||
|
||
\caption{Exemples de \textit{test interfaces} implémentés par aucune \textit{class table}}
|
||
\label{fig:tiUnsolvable}
|
||
\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 \eng{class table} $\mathcal{A}$ implémente une \eng{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}
|
||
\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}}\boxplus\overline{\fj{f'}} \\
|
||
\overline{\fj{F}} = \overline{\fj{E}} \quad\text{où \fj{f} est défini} \\
|
||
\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}
|
||
|
||
$\operatorname{mtype}_\mathcal{A}$ est une application qui renvoie le type de la méthode spécifiée de la classe spécifiée \cite[Fig.1]{fjdef}, dans la \eng{class table} $\mathcal{A}$.
|
||
|
||
$\operatorname{fields}_\mathcal{A}$ est une application qui renvoie la liste complète des attributs de la classe spécifiée \cite[Fig.1]{fjdef}, dans la \eng{class table} $\mathcal{A}$.
|
||
|
||
$\overline{\fj{f}}\boxplus\overline{\fj{f'}}$ désigne la liste $\overline{\fj{f}}$ dont \emph{tous} les attributs manquants ont été complétés par les éléments de la liste $\overline{\fj{f'}}$.
|
||
|
||
\caption{Définition de l'opérateur \eng{Test interface Rule Implemented} (règles \texttt{TRI})}
|
||
\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 le différencier de celui défini dans FJ \cite[Fig.2]{fjdef}, notée $\vdash$. Une expression sera typée sous une \eng{test interface} $\mathfrak{T}$, une \eng{class table} $\mathcal{B}$ et un environnement de typage $\Gamma$.
|
||
|
||
Pour simplifier la définition du typage, nous allons (re)définir les applications suivantes :
|
||
\begin{description}
|
||
\item[\underline{$\operatorname{fields}$}] renvoie l'ensemble des attributs de la classe spécifiée.
|
||
\item[\underline{$\operatorname{mtype}$}] renvoie le type de la méthode spécifiée dans la classe spécifiée.
|
||
\item[\underline{$\operatorname{mbody}$}] renvoie le corps de la méthode spécifiée dans la classe spécifiée (donc une expression avec variables).
|
||
\item[\underline{$\operatorname{construct}$}] renvoie le type du constructeur de la classe spécifiée, c'est à dire la liste finie des types des paramètres.
|
||
|
||
\end{description}
|
||
Ces applications étaient déjà définies dans le papier original \cite[Fig.1]{fjdef} et \enquote{recherchaient} dans une simple \eng{class table}, notre redéfinition les définit recherchant dans une \eng{class table} mais aussi dans une \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{pour \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{C'}) = \overline{\fj{D}}\rightarrow\fj{E}\quad \fj{C} \subclass \fj{C'}}
|
||
& \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. Nous les donnons \autoref{fig:typti}. Nous avons enlevé la règle de typage \textsc{T-SCast} qui autorisait les casts que les auteurs qualifiaient de \enquote{stupides}, entre deux types qui ne sont 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}$.
|
||
%XXX Si le temps, rajouter cette ligne et la prouver
|
||
%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.
|
||
|
||
\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{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})}
|
||
& \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{Cc} \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{Cc}) = \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{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}}
|
||
& \newtag{\textrm{\textsc{(TI-UCast)}}}{rule:ti:upCast}
|
||
\\[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}
|
||
\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}$, un couple $(\mathcal{B},e)$ \eng{class table} $\times$ expression fermée appelée \enquote{test}, et un environnement de typage $\Gamma$ vérifiant
|
||
\begin{itemize}
|
||
\item $\mathcal{A} \triangleright \mathfrak{T}$
|
||
\item $\mathcal{B} \OKin \mathfrak{T}$
|
||
\item $\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D}$
|
||
\end{itemize}
|
||
|
||
Alors il existe \fj{C} tel que $\mathcal{A} \oplus \mathcal{B},\Gamma \vdash e : \fj{C}$ et $\fj{C} \subclass \fj{D}$.
|
||
\end{theorem}
|
||
Cette dernière condition est nécessaire à cause de la tolérance de l'opérateur $\triangleright$.
|
||
|
||
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 pour chaque \eng{test interface} un préordre sur les \eng{class tables} qui l'implémentent de la manière suivante.
|
||
|
||
%XXX Remove if unnecessary
|
||
\vspace{3ex}
|
||
|
||
\begin{definition}
|
||
Soit une \eng{test interface} $\mathfrak{T}$.
|
||
|
||
Soient deux \eng{class tables} $\mathcal{A}$ et $\mathcal{B}$ qui implémentent toutes deux $\mathfrak{T}$
|
||
|
||
Alors
|
||
\[\mathcal{A} \prec_\mathfrak{T} \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\]
|
||
|
||
où $\mathcal{A} \oplus \mathcal{B}$ dénote l'ensemble des classes de $\mathcal{A}$ auquel on a ajouté les classes de $\mathcal{B}$ dont les noms n'étaient pas déjà dans $\mathcal{A}$.
|
||
\end{definition}
|
||
|
||
Nous noterons la plupart du temps simplement $\prec$ pour désigner $\prec_\mathfrak{T}$ si la \eng{test interface} considérée est sans ambiguïté.
|
||
|
||
Nous allons déjà renforcer ce préordre, avant de fournir un exemple complet \autoref{sec:exPreordre}.
|
||
|
||
\subsection{Renforcement 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 acceptent une suite infinie de réductions, 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 \fj{IList} définit deux attributs, dont un de son propre type.
|
||
|
||
\begin{figure}
|
||
\small
|
||
\begin{fjlisting}
|
||
\fjclass{Static}{}{
|
||
\fjmethod{IList}{intList}{Int i}{new IList(i, intList(i+1))}
|
||
\fjmethod{IList}{zeroList}{}{new IList(0, zeroList())}
|
||
}
|
||
\end{fjlisting}
|
||
\caption{Définitions de listes infinies}
|
||
\label{fig:ilistsDefs}
|
||
\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éfinis précédemment, nos préordres 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 où les prémisses ne sont jamais vérifiées, et donc, l'universalité du vide s'applique. 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}
|
||
\]
|
||
|
||
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 changer la définition de tous nos préordres, en remplaçant 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 ouvertes} ou \enquote{valeurs avec variables}, que l'on notera avec la lettre $\hbar$. Il s'agit simplement d'expressions ouvertes qui ne contiennent que des nœuds de type \ref{rule:expr:variable} et \ref{rule:expr:constructor} et telles que un nom de variable n'est utilisé au plus qu'\emph{une seule fois}.
|
||
|
||
Par exemple, l'objet suivant est une valeur à trois variables
|
||
\[\fj{new C(x,new S(new S(y,new G()),z))}\]
|
||
|
||
On a donc aussi une opération de remplissage, comme pour les expressions à variables, que l'on note de la même manière. On supposera que si l'on marque $\hbar\bracket{\alpha}$, c'est que l'ensemble des variables libres de $\hbar$ est inclus dans l'ensemble de définition de $\alpha$.
|
||
|
||
Nous alons alors pouvoir redéfinir le préordre sur deux programmes :
|
||
\[(\mathcal{A},e)\pprec(\mathcal{B},f) \ssi \forall \hbar \forall \alpha \quad \left(e \rightarrow_\mathcal{A}^* \hbar\bracket{\alpha} \implies \exists \beta\quad f \rightarrow_\mathcal{B}^* \hbar\bracket{\beta}\right)\]
|
||
|
||
Intuitivement, on vérifie que si d'un coté du préordre, l'expression peut s'évaluer en un objet de type \fj{C}, alors l'autre coté s'évaluera lui aussi en un objet de type \fj{C}, et ce récursivement.
|
||
|
||
On change ainsi dans la définition précédente du préordre sur les \eng{class tables}, mais aussi dans tout autre préordre \enquote{simple} que l'on aurait pu définir:
|
||
\[\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 cette nouvelle définition du préordre.
|
||
|
||
\begin{property}
|
||
\label{thm:hnewnew}
|
||
\[\forall \hbar \forall \alpha \quad \hbar\bracket{\alpha}\rightarrow^* e' \implies \exists \beta\quad e' = \hbar\bracket{\beta}\]
|
||
\end{property}
|
||
|
||
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.
|
||
La preuve complète est présentée \autoref{anx:proofPt1Val}.
|
||
|
||
\begin{property}
|
||
\[\mathcal{A} \pprec \mathcal{B} \implies \mathcal{A} \prec \mathcal{B}\]
|
||
\end{property}
|
||
Il s'agit d'une particularisation, puisque qu'une valeur est une valeur à trou sans trou.
|
||
|
||
\begin{property}[Context Lemma]
|
||
\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*}
|
||
\end{property}
|
||
Ce théorème était en quelque sorte l'objectif de cette redéfinition, puisque nous comparons dorénavant les expressions sur \enquote{toutes les valeurs qu'elles pourraient renvoyer}.
|
||
|
||
La démonstration se fera sur une version plus puissante du théorème où $h$ peut prendre plusieurs trous. La preuve se fait ensuite par récurrence sur la longueur de la chaine de réduction, en discriminant selon l'emplacement de la réduction (dans $h$, dans $e$ ou entre les deux), et en changeant les noms de variables afin de pouvoir boucler la récurrence. La démonstration complète est présentée en \autoref{anx:proofHValCL}.
|
||
|
||
\subsection{Un exemple concret}
|
||
\label{sec:exPreordre}
|
||
Je vais enfin présenter un exemple de \eng{class tables} qui sont différentes et qui seront équivalentes sous une certaine \eng{test interface} que je donnerai également.
|
||
|
||
Ces \eng{class tables} auront pour objectif de définir une fonction de tri de listes (\fj{Sort.sort}), en utilisant deux algorithmes récursif différents. Le premier qui trouve le minimum de la liste, le place au début de cette dernière puis trie le reste. Le second trouve le maximum de la liste, le place à la fin (à l'aide d'un accumulateur), puis trie le reste.
|
||
|
||
La première \eng{class table} \autoref{fig:equivex:first} et la seconde \eng{class table} \autoref{fig:equivex:second} définissent toutes deux une première classe d'utilité afin de calculer des minimums/maximums. Les secondes classes sont celles qui font le processus de tri à proprement parler.
|
||
|
||
Enfin, la \eng{test interface} présentée \autoref{fig:equivex:ti} est assez restreinte afin d'éviter de trop discriminer nos deux classes.
|
||
|
||
\begin{figure}
|
||
\begin{tcolorbox}
|
||
\small
|
||
\lstinputlisting[language=Java,breaklines=true,linerange={2-26}]{FinalExample.java}
|
||
\end{tcolorbox}
|
||
\caption{Première \eng{class tables}}
|
||
\label{fig:equivex:first}
|
||
\end{figure}
|
||
\begin{figure}
|
||
\begin{tcolorbox}
|
||
\small
|
||
\lstinputlisting[language=Java,breaklines=true,linerange={29-62}, texcl]{FinalExample.java}
|
||
\end{tcolorbox}
|
||
\caption{Seconde \eng{class tables}}
|
||
\label{fig:equivex:second}
|
||
\end{figure}
|
||
\begin{figure}
|
||
\begin{tcolorbox}
|
||
\small
|
||
\lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={65-78}]{FinalExample.java}
|
||
\end{tcolorbox}
|
||
\caption{La \eng{test interface} utilisée pour la comparaison}
|
||
\label{fig:equivex:ti}
|
||
\end{figure}
|
||
|
||
Je ne vais pas présenter ici une preuve formelle de l'équivalence de ces deux classes, notamment parce que c'est assez compliqué sans d'autres théorèmes, la définition étant sémantique, il nous manquerait un théorème qui permettrait de se ramener, par exemple, à l'évaluation de chaque méthode. J'ai quelque peu essayé de construire certains de ces théorèmes, mais je n'ai pas eu le temps d'en obtenir un utile avant la fin de mon stage (même si le \eng{context lemma} fournit un très bon moyen de prouver de tels théorèmes).
|
||
|
||
Algorithmiquement, nous pouvons nous convaincre que les méthodes font ce qui leur est demandé, et l'équivalence algorithmique des deux façons de faire est assez simple.
|
||
|
||
Cet exemple nous fournit néanmoins quelques remarques supplémentaires. Nous pouvons remarquer que certaines constructions ont dû être utilisées afin de s'assurer qu'un·e utilisateur·ice n'ait pas intercalé des classes différentes altérant le fonctionnement de notre programme, notamment pour la classe \fj{List} qui est utilisable par le programme de test. Une solution qui pourrait être envisagée (et d'ailleurs celle retenue en Java classique) est l'ajout d'un mot-clé \fj{final} sur les noms de classes des \eng{test interfaces} qui empêcherait aux classes d'une \eng{class table} l'implémentant d'étendre d'une classe marquée \eng{final}, au delà des extensions indiquées.
|
||
|
||
|
||
|
||
\section{Conclusion}
|
||
|
||
Nous avons donc créé un préordre en définissant une nouvelle structure de \eng{test interface}. Cette structure est à la fois assez puissante pour que l'on puisse tester profondément les programmes, mais aussi assez tolérante pour que l'équivalence ne s'arrête pas sur la moindre différence de grammaire. Nous avons aussi obtenu un \eng{context lemma} pour notre préordre, ce qui nous conforte dans son bon fondement.
|
||
|
||
Nous pourrions complexifier la structure en observant d'autres problèmes, par exemple, la comparaison des valeurs de retour (finies ou infinies) n'a pas de limitation sur les types des objets. Nous pourrions imaginer une libraire dont on aimerait qu'elle renvoie un objet \fj{State} décrivant son état, que la \eng{test interface} n'autorise pas à utiliser, si ce n'est comme argument d'une méthode. Alors, la comparaison telle qu'elle est faite va vérifier les variables \enquote{internes} de \fj{State} alors que nous aimerions laisser l'implémentation libre.
|
||
|
||
La preuve complète des théorèmes a pris plus de temps que prévu, notamment à cause de la structure moins intuitive de la seconde, et elles mériteraient d'être formalisées dans un assistant de preuve comme Coq.
|
||
|
||
La structure de \eng{test interface} peut aussi être utilisée à d'autre fins, par exemple à la définition de librairies, ou de \enquote{modules} dans la terminologie de Java 9+.
|
||
|
||
\section{Bibliographie}
|
||
\begingroup
|
||
\renewcommand{\section}[2]{}%
|
||
\printbibliography
|
||
\endgroup
|
||
|
||
\newpage
|
||
\addappheadtotoc
|
||
\appendix
|
||
\addtocontents{toc}{\protect\setcounter{tocdepth}{-1}}
|
||
\appendixpage
|
||
|
||
|
||
|
||
\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}{isZero}{}{true}
|
||
\fjmethod{Bool}{gt}{Int other}{false}
|
||
\fjmethod{Bool}{lt}{Int other}{other.isZero().ite(false,true)}
|
||
}\\
|
||
\fjclass[Int]{SInt}{\fjattr[Int]{prec}}{
|
||
\fjmethod{Bool}{isZero}{}{false}
|
||
\fjmethod{Bool}{gt}{Int other}{other.isZero().ite(true,this.prec.gt(((SInt)other).prec))}
|
||
\fjmethod{Bool}{lt}{Int other}{other.isZero().ite(false,this.prec.lt(((SInt)other).prec))}
|
||
}
|
||
\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}
|
||
\fjmethod{Object}{ensureFinite}{Object obj}{obj}
|
||
}\\
|
||
\fjclass[List]{Cons}{\fjattr[List]{queue}\fjattr{head}}{
|
||
\fjmethod{Bool}{isEmpty}{}{false}
|
||
\fjmethod{Object}{ensureFinite}{Object obj}{this.queue.ensureFinite(obj)}
|
||
}\\
|
||
// Plus une méthode ajoutée dans la classe Static\\
|
||
List ensure(List in) \{\\
|
||
\null\qquad return in.isEmpty().ite((List)in,(Cons)in);\\
|
||
\}
|
||
\end{fjlisting}
|
||
|
||
On ajoute aussi les notations des listes :
|
||
\[\fj{[]} = \fj{new List()}\]
|
||
\[\fj{$o$::$e$} = \fj{new Cons($e$,$o$)}\]
|
||
|
||
Cette dernière méthode \fj{ensure} s'assure que la liste donnée en paramètre est une \enquote{vrai} liste, c'est à dire, une liste créée avec \fj{[]} et \fj{::}. La fonction ne se réduit pas en une valeur le cas contraire.
|
||
|
||
\subsection{Les Optional}
|
||
\label{anx:classes:optional}
|
||
\begin{fjlisting}
|
||
\fjclass{Optional}{}{
|
||
\fjmethod{Object}{orElse}{Object e}{e}
|
||
}\\
|
||
\fjclass[Optional]{Some}{\fjattr{value}}{
|
||
\fjmethod{Object}{orElse}{Object e}{this.value}
|
||
}\\
|
||
\fjclass[Optional]{None}{}{}
|
||
\end{fjlisting}
|
||
|
||
Ces trois classes définissent la notion d'\fj{Optional} qui fonctionne comme \lstinline[language=Caml]|a' option| en OCaml, et qui peut contenir une valeur ou non. La méthode \fj{orElse} permet de récupérer la valeur contenue si elle est présente, ou de renvoyer le paramètre dans le cas contraire.
|
||
|
||
\section{Exemple sur la nécessité d'utiliser une \eng{class table} de test}
|
||
\label{anx:exmpl:cttest}
|
||
Nous présentons l'exemple suivant:
|
||
\begin{tcolorbox}
|
||
\small
|
||
\lstinputlisting[language=FeatherweightJava,breaklines=true]{NeedTestCT.java}
|
||
\end{tcolorbox}
|
||
Nous y ajoutons bien sûr la définition de \fj{IList}, de \fj{Int} et de \fj{Bool} présentées \autoref{anx:moreclass}.
|
||
|
||
Dans cet exemple, nous avons deux \eng{class table} qui définissent toutes deux une méthode \fj{getList} qui renvoie intuitivement une liste infinie alternant \fj{0} et \fj{1}.
|
||
|
||
La différence entre ces deux classes réside dans la méthode \fj{IListProblem.contains} qui dans une \eng{class table} vérifie si la liste infinie contient un \fj{0}, et dans l'autre vérifie si la liste infinie contient un \fj{1}.
|
||
|
||
Sans ajouter de classes de \enquote{test}, il n'est pas possible de différencier ces deux class tables. En effet, le seul moyen de les différencier serait d'obtenir un résultat différent par la fonction \fj{IListProblem.contains} en fournissant le même paramètre de type \fj{IList}.
|
||
Cependant, la classe \fj{IList} ayant un paramètre de son propre type, il n'est possible de créer une expression typée par \fj{IList} que en utilisant un appel à méthode récursif.
|
||
Or, le seul appel qu'il est possible de faire dans ces deux \eng{class tables} est sur \fj{IListProblem.getList}. Et donc, toute liste infinie que l'on pourra créer dans ces deux \eng{class tables} sera nécessairement terminée par la liste infinie de \fj{0} et de \fj{1}.
|
||
Donc les méthodes \fj{contains} renverrons toujours \fj{true}.
|
||
|
||
Notez que le problème est le même sans la présence de la méthode \fj{getList}, on n'aurait alors pas pu discriminer les deux méthodes \fj{contains} pour un même argument, puisqu'il n'aurait alors pas été possible d'instancier un argument.
|
||
|
||
Bien sûr, avec une \eng{class table} de tests, il est possible de créer des objets \fj{IList} de la forme que l'on souhaite, et donc de discriminer ces deux méthodes, par exemple avec une liste infinie de \fj{0}.
|
||
|
||
\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
|
||
|
||
\begin{equation}
|
||
\label{eqn:ptePartielle}
|
||
\mathfrak{T},\mathcal{B}, \Gamma \Vdash e : \fj{D} \implies \exists \fj{C}\quad \mathcal{A}\oplus\mathcal{B},\Gamma \vdash e : \fj{C} \quad\text{et}\quad \fj{C} \subclass \fj{D}
|
||
\end{equation}
|
||
\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{align}
|
||
\fj{C}\;\fj{f} \in \operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc}) &\implies \exists \fj{C'}\subclass\fj{C}\quad\fj{C'}\;\fj{f} \in \operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(\fj{Cc}) \label{eqn:utl:fields}\\
|
||
\operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}(\fj{m},\fj{Cc}) = \overline{\fj{D}}\rightarrow\fj{C} & \implies \exists \fj{C'}\subclass \fj{C}\ \exists \overline{\fj{D'}} \superclass \overline{\fj{D}}\quad \operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m},\fj{Cc}) = \overline{\fj{D'}}\rightarrow\fj{C'} \label{eqn:utl:mtype}\\
|
||
\operatorname{construct'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc}) = \overline{\fj{D}} & \implies \exists \overline{\fj{D'}} \superclass \overline{\fj{D}}\quad\exists \overline{\fj{f}} \quad \operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(\fj{Cc}) = \overline{\fj{D'}}\;\overline{\fj{f}} \label{eqn:utl:construct}
|
||
\end{align}
|
||
|
||
\renewcommand\equationautorefname{Propriété}
|
||
\paragraph{\autoref{eqn:utl:fields}}
|
||
Montrons cette propriété par induction sur la relation $\subclass'$.
|
||
|
||
Nous pouvons déjà discriminer sur le cas suivant:
|
||
|
||
\underline{Cas $\fj{C}\;\fj{f} \in \bigcup_{\fj{C}\subclass'\fj{E}}\operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{E})$}
|
||
On applique alors directement l’hypothèse d'induction.
|
||
|
||
\underline{Sinon}
|
||
En inversant la règle qui permet de prouver $\fj{C}\;\fj{f} \in \operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc})$, il y reste trois possibilités, correspondant aux trois règles de construction de $\operatorname{fields}$. La première discrimination permet d'éliminer les second cas où l'attribut aurait été défini pour une classe mère.
|
||
|
||
\subparagraph{Cas $\left[\fj{Cc \{C f, ...\}}\right] \in \mathfrak{T}$ \textnormal{\ref{rule:lti-fields}}}
|
||
Alors, en inversant la preuve de $\mathcal{A} \triangleright \mathfrak{T}$, on obtient une seule règle possible: la règle \ref{rule:tri:attributes}, et on a donc
|
||
\[\fj{C'} \fj{f} \in \operatorname{fields}_\mathcal{A}(\fj{Cc})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\]
|
||
|
||
\subparagraph{Cas $\left[\fj{Cc (..., C f, ...)}\right] \in \mathfrak{T}$ \textnormal{\ref{rule:lti-fields2}}}
|
||
Alors, en inversant la preuve de $\mathcal{A} \triangleright \mathfrak{T}$, on obtient une seule règle possible: 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{Cc})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\]
|
||
|
||
\subparagraph{Cas $\fj{class Cc \{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}_{\mathcal{A}\oplus\mathcal{B}}(\fj{Cc})$ (On prend $\fj{C'} = \fj{C}$)
|
||
|
||
\paragraph{\autoref{eqn:utl:mtype}}
|
||
Procédons par induction sur la définition de $\operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}$.
|
||
|
||
Nous avons comme hypothèse $\operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C}$.
|
||
|
||
\subparagraph{Cas $\left[\fj{Cc : 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}\]
|
||
|
||
\subparagraph{Cas $\fj{class Cc \{... 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{Cc}) = \overline{\fj{D}} \rightarrow \fj{E}\quad\text{et}\quad\fj{Cc}\subclass\fj{Cc}\]
|
||
|
||
\subparagraph{Cas $\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}} \rightarrow \fj{E}$ et $\fj{C}\subclass'\fj{Cc}$ \textnormal{\ref{rule:lup-method}}}
|
||
|
||
\label{proof:mtype:cchain}
|
||
Puisque $\fj{C}\subclass'\fj{Cc}$, alors, il existe une chaine de classes
|
||
\[\fj{C} = \fj{C}_0 , \fj{C}_1 , \dots , \fj{C}_n = \fj{Cc}\]
|
||
|
||
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})$.
|
||
Être $\textsc{OK}$ implique notamment que l'on ne change pas le type d'une méthode que l'on aurait éventuellement surchargée.
|
||
On a donc que pour chacune de ces classes:
|
||
|
||
\[\operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m},\fj{C}_n) = \operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m},\fj{C}_{n-1}) = \cdots = \operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m},\fj{C}_0)\]
|
||
|
||
Donc $\operatorname{mtype}(\fj{m},\fj{Cc}) = \overline{\fj{D}}\rightarrow \fj{E}$.
|
||
|
||
\paragraph{\autoref{eqn:utl:construct}}
|
||
|
||
Inversons la règle qui a permis de prouver : \[\operatorname{construct'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc}) = \overline{\fj{D}}\]
|
||
|
||
\subparagraph{Cas $\left[\fj{Cc ($\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 \autoref{rule:tri:constructor}, et on a donc
|
||
\[\exists \overline{\fj{D'}}\quad\overline{\fj{D'}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)\]
|
||
|
||
\subparagraph{Cas $\fj{class Cc\{Cc($\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}_{\mathcal{A}\oplus\mathcal{B}}(\fj{Cc}) = \overline{\fj{D}}\;\overline{\fj{f}} \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 prémisse de la \autoref{eqn:ptePartielle}, présentée au début de la section.
|
||
Cette prémisse est la suivante:
|
||
\[\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D}\]
|
||
|
||
Je vais, pour chaque règle, lister directement en dessous la liste des hypothèses qu'elle induit.
|
||
\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{Cc} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash e_0 : \fj{Cc'}\quad\text{et}\quad \fj{Cc'}\subclass\fj{Cc}
|
||
\item \fj{C}\;\fj{f} \in \operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc})
|
||
\end{hyps}
|
||
|
||
On peut alors appliquer la \autoref{eqn:utl:fields} sur la quatrième hypotèse qui nous donne
|
||
\[\exists\fj{C'}\subclass \fj{C} \quad \fj{C'}\;\fj{f} \in \operatorname{fields}(\fj{Cc})\]
|
||
|
||
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{Cc} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash e_0 : \fj{Cc'}\quad\text{et}\quad \fj{Cc'}\subclass\fj{Cc}
|
||
\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'}_{\mathfrak{T},\mathcal{B}}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C}
|
||
\item \overline{\fj{CX}} \subclass \overline{\fj{C}}
|
||
\end{hyps}
|
||
|
||
On peut alors appliquer la \autoref{eqn:utl:mtype} sur la cinquième hypothèse, on obtient que
|
||
\[\operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m}, \fj{Cc}) = \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 \autoref{eqn:utl:mtype} (après inversion de la règle \ref{rule:lup-method})
|
||
|
||
\[\operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m},\fj{Cc'}) = \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'}_{\mathfrak{T},\mathcal{B}}(\fj{C}) = \overline{\fj{D}}
|
||
\item \overline{\fj{CX}} \subclass \overline{\fj{D}}
|
||
\end{hyps}
|
||
|
||
On peut appliquer la \autoref{eqn:utl:construct} sur la quatrième hypothèse. On obtient alors que :
|
||
\[\operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(\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 les relations de sous-typage 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-DCast}
|
||
|
||
\section{Preuve de la \autoref{thm:hnewnew} sur les valeurs infinies}
|
||
\label{anx:proofPt1Val}
|
||
On rappelle tout d'abord la propriété:
|
||
\[\forall \hbar \forall \alpha \quad \hbar\bracket{\alpha}\rightarrow^* e' \implies \exists \beta\quad e' = \hbar\bracket{\beta}\]
|
||
|
||
Nous allons d'abord montrer la propriété sur les expressions suivante:
|
||
\begin{property}
|
||
\label{thm:enewnew}
|
||
Soit $e$ et $f$ des expressions fermées, telles que $e \rightarrow^* f$,
|
||
|
||
Si $e = \fj{new C($\overline{e'}$)}$
|
||
|
||
Alors $f = \fj{new C($\overline{f'}$)}$ et $\overline{e'} \rightarrow^* \overline{f'}$.
|
||
\end{property}
|
||
|
||
Montrons cette propriété par récurrence sur la longueur de la réduction $e \rightarrow^* f$.
|
||
\subparagraph{Initialisation}
|
||
Dans le cas $e = f$, on a simplement $f = \fj{new C($\overline{e'}$)}$ et $\overline{e'} \rightarrow^0 \overline{e'}$.
|
||
\subparagraph{Hérédité}
|
||
Nous sommes dans l'hypothèse où $e \rightarrow^n f$.
|
||
Observons la première relation. Elle se fait nécessairement sur un nœud de type \ref{rule:expr:method}, \ref{rule:expr:field} ou \ref{rule:expr:cast}, qui est donc contenu dans l'un des $\overline{e'}$. Donc, on a $e'_i \rightarrow e''_i$. On note $e''_k = e'_k$ pour $k$ différent de $i$, et on obtient que
|
||
\[e = \fj{new C($\overline{e'}$)} \rightarrow \fj{new C($\overline{e''}$)} \rightarrow^{n-1} f\]
|
||
On peut donc appliquer l'hypothèse de récurrence à la dernière relation $\rightarrow^{n-1}$, et nous obtenons bien que
|
||
\[f = \fj{new C($\overline{f'}$)} \quad\text{et}\quad \overline{e'} \rightarrow^* \overline{e''} \rightarrow^* \overline{f'}\]
|
||
|
||
La récurrence est terminée.
|
||
|
||
Nous allons donc pouvoir facilement montrer la \autoref{thm:hnewnew} par induction sur le paramètre $\hbar$.
|
||
|
||
\subparagraph{$\hbar = \fj{x}$}
|
||
|
||
En notant $\beta$ tel que $\beta(\fj{x}) = e'$, on obtient que
|
||
|
||
\[\hbar\bracket{\alpha} = \alpha(\fj{x}) \rightarrow e' = \hbar\bracket{\beta}\]
|
||
|
||
\subparagraph{$\hbar = \fj{new C($\overline{\hbar'}$)}$}
|
||
|
||
Alors, par application de la \autoref{thm:enewnew}, on obtient que
|
||
\[e' = \fj{new C($\overline{e}$)} \quad\text{et}\quad \overline{\hbar\bracket{\alpha}} \rightarrow^* \overline{e}\]
|
||
|
||
On peut alors appliquer l'hypothèse d'induction, et obtenir que
|
||
\[\overline{e} = \overline{\hbar\bracket{\beta_x}}\]
|
||
|
||
Donc, en notant $\beta$ la concaténation des $\beta_x$, qui est possible puisque les noms de variables utilisés dans $\hbar$ sont tous distincts, on obtient le résultat
|
||
\[e' = \hbar\bracket{\beta}\]
|
||
|
||
|
||
\section{Preuve du \eng{context lemma} avec 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}$.
|
||
|
||
La lettre $h$ dénotera une expression FJ quelconque (ouverte ou fermée). Nous les dénoterons ainsi afin de ne pas les confondre avec les expressions \enquote{fermées}, dénotées elles $e$,$f$.
|
||
|
||
Nous noterons aussi $\varepsilon$ et $\gamma$ les \eng{mappings} servant à \enquote{remplir} les expression ouvertes, afin de ne pas les confondre avec $\alpha$ et $\beta$, qui servent à remplir les valeurs avec variables.
|
||
|
||
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 \alpha\quad e \rightarrow \hbar\bracket{\alpha}) \implies (\exists \beta\quad f \rightarrow \hbar\bracket{\beta})\]
|
||
|
||
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})\]
|
||
|
||
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 \alpha\quad h\bracket{\varepsilon}\rightarrow^* \hbar\bracket{\alpha}\right)\implies\left(\exists \beta\quad h\bracket{\gamma}\rightarrow^* \hbar\bracket{\beta}\right)\]
|
||
\end{theorem}
|
||
|
||
C'est sous cette seconde forme que nous allons prouver le théorème (elle est plus \enquote{bas niveau}).
|
||
|
||
Nous allons tout d'abord faire une récurrence sur la longueur de la réduction $h\bracket{\varepsilon}\rightarrow^* \hbar\bracket{\beta}$, notée $n$.
|
||
|
||
|
||
\paragraph{Initialisation}
|
||
On démontre alors le résultat par induction sur $\hbar$.
|
||
|
||
On suppose que $h\bracket{\varepsilon} = \hbar\bracket{\alpha}$.
|
||
|
||
\subparagraph{Cas $\hbar = \hole$}
|
||
Alors
|
||
\[h\bracket{\gamma} = \hbar\bracket{\beta}\quad\text{avec}\quad \beta = \left(h\bracket{\gamma}\right)\]
|
||
|
||
\subparagraph{Cas $\hbar = \fj{new C($\overline{\hbar'}$)}$}
|
||
Alors, il y a deux possibilités.
|
||
|
||
Ou bien, on a $h = \fj{x}$, et alors puisque $\varepsilon \prec \gamma$ et que $\varepsilon(\fj{x}) = \hbar\bracket{\alpha}$, alors, on a que $\gamma(\fj{x})\rightarrow^*\hbar\bracket{\beta}$
|
||
|
||
Ou bien, on a $h = \fj{new C($\overline{h'}$)}$, et donc par induction
|
||
\[\overline{h'}\bracket{\gamma} \rightarrow^* \overline{\hbar'\bracket{\beta'}}\]
|
||
|
||
Et donc, en notant $\beta$ la concaténation des $\overline{\beta'}$ (puisque les noms de variables sont utilisés de manière unique, les domaines de définition sont donc disjoints), on obtient que
|
||
\[h\bracket{\gamma} \rightarrow^* \hbar\bracket{\beta}\]
|
||
|
||
\paragraph{Hérédité}
|
||
|
||
Notre hypothèse de récurrence \textsc{(HR)} est la suivante:
|
||
\[\forall h \quad \varepsilon \prec \gamma \implies h\bracket{\varepsilon} \prec^{<n} h\bracket{\gamma}\]
|
||
|
||
Nous aurons ensuite trois cas, suivant l'endroit où s'effectue la première étape de la réduction.
|
||
|
||
\underline{La réduction se fait uniquement avec des nœuds de $h$}
|
||
Alors, on a $h \rightarrow h'$ indépendamment du \eng{mapping} considéré, et on peut appliquer \textsc{(HR)} qui nous donne que, puisque $h'\bracket{\varepsilon} \rightarrow^{n-1} \hbar\bracket{\alpha}$
|
||
\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma} \rightarrow^* \hbar\bracket{\beta}\]
|
||
|
||
\underline{La réduction se fait sur un nœud à l’intérieur d'une variable $\fj{x}$ de $h$}
|
||
Alors, dans cette occurrence de la variable $\fj{x}$ dans $h$, nous avons une réduction de la forme suivante.
|
||
\[\varepsilon(\fj{x}) \rightarrow e^{\fj{x}}\]
|
||
Choisissons alors un nom de variable non utilisé dans $\epsilon$ et $\gamma$ : $\fj{y}$, et créons $\varepsilon'$ ainsi:
|
||
|
||
\[\varepsilon' = \left[ \begin{array}{ccc}
|
||
\fj{x} &\mapsto& \varepsilon(\fj{x})\\
|
||
\fj{y} &\mapsto& e^{\fj{x}}\\
|
||
v &\mapsto& \varepsilon(v)
|
||
\end{array} \right]
|
||
\quad
|
||
\gamma' = \left[ \begin{array}{ccc}
|
||
\fj{x} &\mapsto& \gamma(\fj{x})\\
|
||
\fj{y} &\mapsto& \gamma(\fj{x})\\
|
||
v &\mapsto& \gamma(v)
|
||
\end{array} \right]\]
|
||
|
||
Ainsi, la réduction considérée s'exprime comme
|
||
\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\alpha}\]
|
||
|
||
Or, nous avons aussi que $\varepsilon' \prec \gamma'$. Nous n'avons en effet que $\varepsilon(\fj{y})\prec\gamma(\fj{y})$ à vérifier, c'est à dire que $\varepsilon(\fj{x})\rightarrow e^{\fj{x}} \prec \gamma(\fj{x})$
|
||
|
||
Cela est vrai par propriété de confluence sur l'opération de réduction. Intuitivement, un nœud d'une expression FJ ne peut se réduire que d'une seule façon (l'une des trois règles de réduction), et cette réduction se fait sans perte d'information (dans le sens où on aurait pas pu en extraire plus sans modifier le nœud en question). Il suffit donc de réduire les même nœuds des deux cotés afin d'obtenir une même expression.
|
||
\begin{center}
|
||
\begin{tikzpicture}
|
||
\node (e1) at (1,1) {$\varepsilon(\fj{x})$};
|
||
|
||
\node (e2) at (0,0) {$e^{\fj{x}}$};
|
||
|
||
\node (e3) at (0,-1) {$\hbar\bracket{\alpha}$};
|
||
|
||
\node (e4) at (1,-2) {$\hbar\bracket{\alpha'}$};
|
||
|
||
\draw[->] (e1) -- (e2);
|
||
\draw[->] (e2) to node[very near end, above right] {$*$} (e3);
|
||
|
||
\draw[->,dashed] (e1) to node[very near end, above right] {$*$} (e4);
|
||
\draw[->,dashed] (e3) to node[very near end, above right] {$*$} (e4);
|
||
\end{tikzpicture}
|
||
\end{center}
|
||
|
||
On peut alors appliquer l'hypothèse $\varepsilon \prec \gamma$.
|
||
|
||
Nous avons donc toutes les conditions réunies pour appliquer l'hypothèse de récurrence.
|
||
|
||
\underline{La réduction s'est faite entre un nœud de $h$ et un nœud de $\varepsilon$}
|
||
Il y a trois cas de figure pour lesquels les deux cas précédents ne sont pas adéquats. Le premier est un appel à \eng{field} de la forme $\fj{x.field}$, le second est un appel à méthode de la forme $\fj{x.meth($\overline{h'}$)}$ et le troisième cas est le \eng{cast} de la forme $\fj{(D)x}$.
|
||
|
||
Dans ces trois cas, nous avons nécessairement $\varepsilon(\fj{x}) = \fj{new C($\overline{e^\varepsilon}$)}$, et donc aussi $\gamma(\fj{x}) = \fj{new C($\overline{e^\gamma}$)}$ avec $\overline{e^\varepsilon} \prec \overline{e^\gamma}$, puisque $\varepsilon \prec \gamma$.
|
||
|
||
Dans le cas de $\fj{x.field}$, on choisit un nouveau nom de variable inutilisé $\fj{y}$, et nous créons une nouvelle fois $\varepsilon'$ et $\gamma'$ ainsi.
|
||
|
||
\[\varepsilon' = \left[ \begin{array}{ccc}
|
||
\fj{x} &\mapsto& \varepsilon(\fj{x})\\
|
||
\fj{y} &\mapsto& e^\varepsilon_k\\
|
||
v &\mapsto& \varepsilon(v)
|
||
\end{array} \right]
|
||
\quad
|
||
\gamma' = \left[ \begin{array}{ccc}
|
||
\fj{x} &\mapsto& \gamma(\fj{x})\\
|
||
\fj{y} &\mapsto& e^\gamma_k\\
|
||
v &\mapsto& \gamma(v)
|
||
\end{array} \right]\]
|
||
|
||
Nous avons alors toujours $\varepsilon' \prec \gamma'$, mais aussi que la première réduction s'écrit
|
||
\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\alpha}\]
|
||
où $h'$ est obtenu en remplaçant l'occurrence de $\fj{x.field}$ susnommée par $\fj{y}$.
|
||
|
||
|
||
On peut donc appliquer l'hypothèse de récurrence pour obtenir, puisque les \eng{class table} considérées sont les mêmes
|
||
\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma'} \rightarrow^* \hbar\bracket{\beta}\]
|
||
|
||
Dans le cas de $\fj{x.meth($\overline{h'}$)}$, la procédure est presque la même.
|
||
|
||
Nous allons noter $\overline{v}$ les noms des paramètres de $\fj{C.meth}$. Nous noterons aussi $h_m$ le corps de cette méthode.
|
||
|
||
Nous allons enfin obtenir $h_m'$ en remplacant dans $h_m$ la variable $\fj{this}$ par la variable $\fj{x}$ et les appels à chaque variable $v_k$ par l'expression à variables $h'_k$.
|
||
|
||
Nous pouvons garder $\varepsilon$ et $\gamma$ tels qu'ils sont.
|
||
|
||
Alors, en remplacant l'appel $\fj{x.meth($\overline{h'}$)}$ susnommé par $h_m'$ dans $h$, on obtient une nouvelle expression $h'$ telle que la réduction soit
|
||
\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon} \rightarrow^{n-1} \hbar\bracket{\alpha}\]
|
||
|
||
Mais en ayant aussi que
|
||
\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma}\]
|
||
|
||
On peut enfin appliquer l'hypothèse de récurrence de la même manière.
|
||
|
||
Enfin, dans le dernier cas $\fj{(D)x}$, puisque la réduction s'est bien effectuée, c'est que $\fj{C} \subclass \fj{D}$. On peut donc simplement remplacer dans $h$ le cast par la variable $\fj{x}$ seule.
|
||
|
||
|
||
|
||
\section{Le stage au LACL}
|
||
\label{anx:stage}
|
||
Je vais présenter ici le laboratoire dans lequel j'ai fait ce stage. Le Laboratoire d'Algorithmique, Complexité et Logique est un laboratoire inclus dans l'Université Paris-Est Créteil. Le laboratoire est donc dans un campus universitaire, et accueille aussi quelques doctorant·es, que je n'ai que peu vu·es à cause de la période tardive du stage. Ce stage m'a en partie confirmé que je voulais m'orienter vers de la recherche, le travail bien que modeste que j'ai effectué correspondait à l'image que je me faisait de l'\enquote{exercice} de la recherche, ce que je n'avais jamais expérimenté avant. Je reste conscient que je n'ai vu qu'une très petite partie du quotidien d'un·e chercheur·euse. J'ai aussi été sous la tutelle de Clément Aubert, Maître de conférence à l'université d'Augusta, Géorgie. Je n'ai pas beaucoup croisé les membres des autres équipes du laboratoire, ne serait-ce que pendant quelques discussions lors des pauses repas.
|
||
|
||
\end{document}
|