diff --git a/FinalExample.java b/FinalExample.java index 648304f..0576cb6 100644 --- a/FinalExample.java +++ b/FinalExample.java @@ -1,28 +1,3 @@ -///////////////// COMMON TO BOTH CLASS TABLES ///////////////// -class Optional extends Object {} -class Some extends Optional { - Object value; - Object orElse(Object e){ - return this.value; - } -} -class None extends Optional { - Object orElse(Object e){ - return e; - } -} - -class Static extends Object { - /* - Makes sure that the input list is a "real" one, - that is, one created with [] and :: (List and Cons). - Cannot reduce to any value if not. - */ - List ensure(List in) { - return in.isEmpty().ite((List)in,(Cons)in); - } -} - //////////////// FIRST CLASS TABLE ///////////////// class MinGetter extends Object { /* diff --git a/NeedTestCT.java b/NeedTestCT.java new file mode 100644 index 0000000..9fff36e --- /dev/null +++ b/NeedTestCT.java @@ -0,0 +1,13 @@ +class IListProblem extends Object { + IList getList() { + return new IList(new IList(getList(), 1), 0); + } + // Premiere class table + Bool contains(IList arg) { + return ((Int)arg.head).eq(0).ite(true, this.contains(arg.tail)); + } + // Seconde class table + Bool contains(IList arg) { + return ((Int)arg.head).eq(1).ite(true, this.contains(arg.tail)); + } +} diff --git a/RapportStage.tex b/RapportStage.tex index c2a4a95..af83a84 100644 --- a/RapportStage.tex +++ b/RapportStage.tex @@ -37,7 +37,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 + 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. \section{Définitions et notations} \label{sec:defNots} @@ -65,8 +65,6 @@ 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$. - 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. - 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). @@ -100,7 +98,7 @@ \end{figure} \subsection{Définitions et raccourcis de programmation} - Nous allons définir en sus la grammaire des expressions à trou notés $h$, $h'$: + 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: @@ -114,6 +112,8 @@ (\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}$)}. @@ -121,21 +121,9 @@ 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.%TODO Vérifier qu'elles le soient + 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}). - - \subsection{Extension de Featherweight Java} - \marginpar{Voir pour enlever cette section si pas assez utilisée} - Afin de créer des théorèmes plus tard, nous allons parfois considérer une extension du Featherweight Java, qui ajoute une valeur \fj{null}. Cependant, ajouter une simple valeur qui soit typable pour tous type enlève l'unicité du typage dans une \eng{class table}, et une valeur qui ne soit typable pour aucun type enlève la préservation du type, car - \[\underbrace{\fj{(C)null}}_{\vdash \fj{C}} \rightarrow \underbrace{\fj{null}}_{\nvdash}\] - - L'implémentation choisie est donc un \eng{null} toujours typé, que l'on notera \fj{null(C)}. Qui permet de préserver les deux propriétés sus-nommées. - - L'ajout de \fj{null(C)} ajoute une règle axiomatique de typage indiquant $\vdash \fj{null(C)}:\fj{C}$. On n'ajoute aucune règle de réduction (car on ne peut rien appliquer à \fj{null}). On ajoute aussi \fj{null(C)} dans la liste des valeurs. - - Une dernière remarque sur cet ajout est que l'on vient d'ajouter encore deux cas où une réduction d'une expression bien typée peut \enquote{bloquer}. Ces deux cas sont l'équivalent java des \verb*|NullPointerException| (un pour les attributs, l'autre pour les méthodes). - \section{Étude d'équivalences simples} \label{sec:eqsimpl} @@ -154,7 +142,7 @@ \paragraph{Une définition la plus simple} On peut commencer par dire qu'un contexte est simplement une expression à trou $C = h$. L'interpretation d'un programme $P = (\mathcal{A},e)$ dans un contexte $C$ est alors \[C\bracket{P} = (\mathcal{A},h\bracket{e})\] - Le \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. Nous verrons plus tard des exemples démontrant que c'est une vraie limitation.%TODO Ajouter les exemples avec des références précises pour cette phrase, ou la supprimer + 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. 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 @@ -162,7 +150,7 @@ 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}\] - Ce problème du trou dégénéré permet d'évaluer n'importe quelle expression, ce qui fait que les expressions \eng{main} des programmes n'ont aucun effet sur le résultat de la comparaison. On peut donc évaluer pour chaque nom de classe $\fj{C}$ l'expression \fj{new C(null(D),...,null(E))} qui est une valeur si et seulement si la classe \fj{C} est présente dans la \eng{class table} et que ses attributs sont de types \fj{D},\fj{...},\fj{E}. De la même manière, on peut tester si une méthode existe dans une classe (à supposer qu'il existe des paramètres telle qu'elle se réduise en valeur). Donc deux programmes comparés ainsi devront avoir exactement la même structure, les mêmes noms de classe, mêmes noms d'attributs, même noms de méthode. + 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. 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. @@ -471,7 +459,8 @@ Grâce à ces méthodes, nous pouvons réutiliser les règles de typage de Featherweight Java presque à l'identique, qui sont rappelées \autoref{fig:typti}. Nous avons enlevé la règle de typage \textsc{T-SCast} qui autorisait les casts que les auteurs qualifiaient de \enquote{stupides}, entre deux types qui n'étaient pas parents l'un de l'autre. - Nous vérifions aussi évidement la \eng{class table} $\mathcal{B}$, en vérifiant que le corps de chaque méthode est bien typé par le type attendu dans la méthode, que les champs de la \eng{class table} ne contredisent pas la \eng{test interface}. On note alors $\mathcal{B} \OKin \mathfrak{T}$. Les seules contradictions sont grammaticales si l'on a déjà vérifié que les applications $\operatorname{fields}$, $\operatorname{construct}$ et $\operatorname{mtype}$ n'étaient pas redéfinies ou mal définies.\marginpar{à prouver} + Nous vérifions aussi évidement la \eng{class table} $\mathcal{B}$, en vérifiant que le corps de chaque méthode est bien typé par le type attendu dans la méthode, que les champs de la \eng{class table} ne contredisent pas la \eng{test interface}. On note alors $\mathcal{B} \OKin \mathfrak{T}$. Les seules contradictions sont grammaticales si l'on a déjà vérifié que les applications $\operatorname{fields}$, $\operatorname{construct}$ et $\operatorname{mtype}$ n'étaient pas redéfinies ou mal définies. + %TODO prouver l'affirmation \begin{figure} \begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue] @@ -542,7 +531,8 @@ \mathcal{A}\oplus\mathcal{B} \Downarrow v \end{array}\right. \implies \mathcal{A'}\oplus\mathcal{B}\Downarrow v\] \end{definition} - %TODO Ajouter un exemple + + Nous allons d'abord renforcer un peu ce préordre, avant de fournir un exemple complet \autoref{sec:exPreordre}. \subsection{Renforcement de ce préordre avec les valeurs infinies} @@ -595,7 +585,7 @@ 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 \j{C}, alors l'autre coté s'évaluera lui aussi en un objet de type \fj{C}, et ce récursivement. + 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 la définition de tous les autres préordres, notamment celui sur les \eng{class tables}: \[\mathcal{A}\pprec\mathcal{B} \ssi \forall e \quad (\mathcal{A},e) \pprec (\mathcal{B},e)\] @@ -625,28 +615,19 @@ 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{class table} 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. - Nous utiliserons quatre classes communes aux deux class tables présentées \autoref{fig:equivex:common} Les trois premières définirons la classe \fj{Optional} qui fonctionne comme \lstinline[language=Caml]|a' option| en OCaml, et qui peut contenir une valeur ou non. Nous définirons aussi une méthode \fj{ensure(List in)} qui nous permet de nous assurer que nous n'avons pas créé de nouvelles classes se substituant aux constructeurs privilégiés des listes (\fj{[]} et \fj{::}). - - 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 seconde classes sont celles qui font le processus de tri à proprement parler. + 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. 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=FeatherweightJava,breaklines=true,linerange={2-24}]{FinalExample.java} - \end{tcolorbox} - \caption{Classes communes aux deux \eng{class tables}} - \label{fig:equivex:common} - \end{figure} - \begin{figure} - \begin{tcolorbox} - \small - \lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={27-51}]{FinalExample.java} + \lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={2-26}]{FinalExample.java} \end{tcolorbox} \caption{Première \eng{class tables}} \label{fig:equivex:first} @@ -654,7 +635,7 @@ \begin{figure} \begin{tcolorbox} \small - \lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={54-87}]{FinalExample.java} + \lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={29-62}]{FinalExample.java} \end{tcolorbox} \caption{Seconde \eng{class tables}} \label{fig:equivex:second} @@ -662,7 +643,7 @@ \begin{figure} \begin{tcolorbox} \small - \lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={90-103}]{FinalExample.java} + \lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={65-78}]{FinalExample.java} \end{tcolorbox} \caption{La \eng{test interface} utilisée pour la compairaison} \label{fig:equivex:ti} @@ -739,13 +720,57 @@ \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{Exemples de \eng{class tables}} + + \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 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} @@ -930,7 +955,6 @@ Nous allons aussi étendre cette définition à deux \eng{mappings} ayant le même domaine: \[\varepsilon \prec \gamma \ssi \forall \fj{x}\in\operatorname{Dom}(\varepsilon)=\operatorname{Dom}(\gamma)\quad \varepsilon(\fj{x}) \prec \gamma(\fj{x})\] - \marginpar{Un exemple d'utilisation de ces notations est-il nécessaire ?} Le théorème, plus général que nous allons montrer est le suivant: