Mysaa/stage-2022
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Prise en compte des Commentaires de Clément - Corps

Browse Source
This commit is contained in:
Mysaa 2022-08-18 16:09:25 +02:00
parent 95521344c6
commit 93f99896e4
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
2 changed files with 72 additions and 66 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

135
RapportStage.tex
View File

@ -27,7 +27,7 @@
\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é par les langages les plus utilisés de nos jours (Java, Python, C++, ...).
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.
@ -39,7 +39,7 @@
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 vais commencer \autoref{sec:defNots} par faire quelques rappels formels de la définition du Featherweight Java, avant de moi-même ajouter quelques nouvelles grammaires qui seront utilisées pendant le document. Je vais ensuite présenter \autoref{sec:eqsimpl} quelques unes des équivalences, les plus \enquote{évidentes}, que j'ai considéré afin d'étudier leurs propriétés et surtout d'expliciter les problèmes, propres à FJ ou non, que certaines équivalences pouvaient soulever et qu'une \enquote{bonne} définition devrait résoudre. 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 d'équivalence.
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 pendant le document. Je vais ensuite présenter \autoref{sec:eqsimpl} quelques unes des équivalences, les plus \enquote{évidentes}, que j'ai considéré afin d'étudier leurs propriétés et surtout d'expliciter les problèmes, propres à FJ ou non, que certaines équivalences pouvaient soulever et qu'une \enquote{bonne} définition devrait résoudre. 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 d'équivalence.
\section{Définitions et notations}
\label{sec:defNots}
@ -48,10 +48,10 @@
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, on aura la notation
Par exemple,
\[f(\overline{a})\quad\equiv\quad 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:
On rappelle la grammaire des expressions, notées $e$, $e_k$ ou $e'$ :
\begin{center}
\refstepcounter{rule}
@ -69,19 +69,19 @@
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 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*|CamlCase| (majuscule) et les noms de méthodes, attributs (\eng{fields}) et variables en \verb*|camelCase| (minuscule).
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)$ et est souvent noté $P$, $Q$, $R$. L'expression est en quelque sorte le \eng{main} du programme.
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. 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}$.
On note $\vdash$ la relation de typage. $\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 :
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})
@ -89,7 +89,7 @@
\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}
Enfin, nous reprenons la définition de la classe \fj{Paire} issue du papier original, reproduite \autoref{fig:pairedef}.
\begin{figure}
\begin{fjlisting}
@ -129,7 +129,7 @@
\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, ni même d'être rigoureuse, mais elle vise à donner au lecteur l'intuition sur les propriétés souhaitables pour un préordre sur les programmes FJ.
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 leur preuve complète, 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}
@ -147,13 +147,13 @@
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 \fj{class tables} qui ne peuvent être différenciées que à l'aide d'une \fj{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 field ou de méthode.
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 qu'elles vérifient
\[\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'import quelle \eng{class table} contenant la classe \fj{Paire} :
\[\fj{new Paire($\hole$,$e$).snd}\]
\[\fj{new Paire($\hole$,$e$).snd} \rightarrow e\]
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(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.
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 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 FJ, un utilisateur malveillant aurait accès à tous ces outils pour mettre en défaut le programme.
@ -177,8 +177,8 @@
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
\left|\begin{array}{l}\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{array}\right. \]
\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}$.
@ -218,7 +218,7 @@
(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 par universalité du vide.
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}
@ -251,7 +251,7 @@
\vfill\null
\end{multicols}
\end{center}
Alors, on a transformé le \emph{programme} en \emph{\eng{class table}}, et si nou 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.
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}
@ -263,7 +263,7 @@
\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é $\mathfrak{T}$, $\mathfrak{U}$, $\mathfrak{V}$. La \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. Et donc, une \eng{class table} implémente une \eng{test interface} lorsqu'elle respect chacune de ses règles.
\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é $\mathfrak{T}$, $\mathfrak{U}$, $\mathfrak{V}$. La \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. Et donc, une \eng{class table} implémente une \eng{test interface} lorsqu'elle respecte chacune de ses règles.
\begin{figure}
\ttfamily
@ -279,7 +279,7 @@
\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
$\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}
@ -320,9 +320,9 @@
Les deux règles \ref{rule:tsg:attributes} et \ref{rule:tsg:constructor} sont donc mutuellement exclusives pour un nom de classe donnée. 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.
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}\]
\[\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 apparaîssent, nous n'allons pas chercher à les exprimer ici, mais vous trouverez des exemples de telles \eng{test interfaces} en \autoref{fig:tiUnsolvable}
@ -330,6 +330,7 @@
\begin{center}
\begin{tabular}{ccc}
\begin{fjlisting}[width=.3\textwidth]
\setlength{\columnseprule}{1pt}
\begin{multicols}{2}
A \{\}\\
B \{\}\\
@ -355,11 +356,11 @@
\end{fjlisting}
\end{tabular}
\end{center}
\underline{La première} parce que la relation de sous-typage et transitive est antisymétrique
\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, \fj{C} doit avoir par héritange un attribut nommé \fj{f}
\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}
@ -416,7 +417,7 @@
$\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'implémentation des \eng{test interfaces rule}}
\caption{Définition de l'opérateur \eng{Test interface Rule Implemented} (règles \texttt{TRI})}
\label{fig:tiDefImpl}
\end{figure}
@ -445,35 +446,35 @@
\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]
& \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]
& \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]
& \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]
& \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]
& \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]
& \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]
& \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}
& \newtag{\textrm{\textsc{(LUp-Meth)}}}{rule:lup-method}
\end{tabular}
\end{center}
\end{tcolorbox}
@ -497,32 +498,32 @@
\infer
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}
{\fj{x} \in \Gamma}
& \newtag{\textrm{\textsc{TI-Var}}}{rule:ti:variable}
& \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}
& \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}
& \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}
& \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}
& \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}
& \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}}
@ -551,8 +552,9 @@
\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}$
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}\\
@ -564,7 +566,7 @@
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'abord renforcer un peu ce préordre, avant de fournir un exemple complet \autoref{sec:exPreordre}.
Nous allons d'abord renforcer ce préordre, avant de fournir un exemple complet \autoref{sec:exPreordre}.
\subsection{Renforcement de ce préordre avec les valeurs infinies}
@ -650,9 +652,9 @@
\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{class table} que je donnerai également.
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 table} auront pour objectif de définir une fonction de trie 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.
Ces \eng{class table} 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 classe table \autoref{fig:equivex:first} et la seconde classe 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.
@ -679,7 +681,7 @@
\small
\lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={65-78}]{FinalExample.java}
\end{tcolorbox}
\caption{La \eng{test interface} utilisée pour la compairaison}
\caption{La \eng{test interface} utilisée pour la comparaison}
\label{fig:equivex:ti}
\end{figure}
@ -687,7 +689,7 @@
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 out dû être utilisées afin de prévenir d'un utilisateur qui puisse intercaler 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 dans le Java officiel) est l'ajout d'un mot-clé \fj{final} sur les noms de classes des \eng{test interfaces} qui empêcherai 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.
Cet exemple nous fournit néanmoins quelques remarques supplémentaires. Nous pouvons remarquer que certaines constructions out dû être utilisées afin de s'assurer qu'un utilisateur n'aie 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 dans le Java officiel) est l'ajout d'un mot-clé \fj{final} sur les noms de classes des \eng{test interfaces} qui empêcherai 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.
@ -702,7 +704,10 @@
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
\appendix
@ -780,29 +785,27 @@
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{Exemples de \eng{class tables}}
\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}.
\subsection{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 pû 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}.
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}

3
header.tex
View File

@ -31,6 +31,7 @@
\usepackage{xpatch}
\usepackage{enumitem}
\usepackage{amsfonts}
\usepackage{mathtools}
\usepackage{geometry}
@ -68,6 +69,8 @@
\newcounter{rule}
\addto\extrasfrench{%
\renewcommand{\figureautorefname}{\textsc{Figure}}
\renewcommand{\sectionautorefname}{Section}
\renewcommand{\subsectionautorefname}{Sous-section}
\renewcommand{\appendixautorefname}{Annexe}
\renewcommand{\theoremautorefname}{Théorème}
\providecommand\propertyautorefname{Propriété}