diff --git a/RapportStage.tex b/RapportStage.tex index 74027ce..5e280e3 100644 --- a/RapportStage.tex +++ b/RapportStage.tex @@ -11,7 +11,7 @@ \\[1ex] et Clément Aubert (Augusta University, Géorgie)} \begin{document} - + \doparttoc \maketitle \hsep @@ -34,12 +34,12 @@ 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'interessent aux equivalences de programmes et à comment les \eng{process calculis} peuvent fournir des nouvelles équivalences à d'autres langages \cite{papierContextEquiv}. + 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 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 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} @@ -67,7 +67,7 @@ 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 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. + 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). @@ -75,7 +75,7 @@ On appelle \enquote{valeur} toute expression composée uniquement de constructeurs (\autoref{rule:expr:constructor}). - 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}$. + 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}$. @@ -85,7 +85,7 @@ \begin{itemize} \item L'évaluation d'un attribut d'un objet (\textsc{R-Field}) \item L'évaluation d'une méthode (\textsc{R-Invk}) - \item L'évaluation d'un cast (\textsc{R-Cast}) + \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. @@ -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 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. + 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} @@ -142,20 +142,20 @@ \subsection{Exemples d'équivalences simples} - \paragraph{Une définition la plus simple} On peut commencer par dire qu'un contexte est simplement une expression à trou $C = h$. L'interpretation d'un programme $P = (\mathcal{A},e)$ dans un contexte $C$ est alors + \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 \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{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 qu'elles vérifient + 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'import quelle \eng{class table} contenant la classe \fj{Paire} : + 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 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. + 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. @@ -261,11 +261,11 @@ 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 \enquote{compilée} (c'est à dire être typée) avec l'interface, puis sera \enquote{executée} (c'est à dire réduite) avec des vraies \eng{class tables}. + 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é $\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. + \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 @@ -273,20 +273,20 @@ \begin{center} \refstepcounter{rule} \begin{tabular}{rll} - TR := & C : C m($\overline{\fj{C}}$) & \qquad \newtag{\textrm{\textsc{TSG-Meth}}}{rule:tsg:method} \\ - | & C \{$\overline{\fj{C}}$ $\overline{\fj{f}}$\} & \qquad \newtag{\textrm{\textsc{TSG-Attr}}}{rule:tsg:attributes} \\ - | & C ($\overline{\fj{C}}$ $\overline{\fj{?}\fj{f}}$) & \qquad \newtag{\textrm{\textsc{TSG-Cstr}}}{rule:tsg:constructor} \\ - | & C <: C & \qquad \newtag{\textrm{\textsc{TSG-Cast}}}{rule:tsg:cast} + 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}} + \caption{Grammaire des \eng{Test Interface rules}} \label{fig:tigrammaire} \end{figure} - Un exemple concret de \eng{test interface} est donnée \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}. + 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} @@ -318,15 +318,15 @@ \item Les noms de classe utilisés sont définis (sauf éventuellement \fj{Object}). \end{itemize} - La troisième règle permet d'éviter les définitions implicites, en suivant la convention du papier original \cite{fjdef}. On peut dans tous les cas rajouter pour une classe \fj{C} non définie une ligne de la forme \fj{C \{\}}. + 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é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. + 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 apparaîssent, nous n'allons pas chercher à les exprimer ici, mais vous trouverez des exemples de telles \eng{test interfaces} en \autoref{fig:tiUnsolvable} + 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} @@ -370,7 +370,7 @@ \paragraph{Opérateur d'implémentation} - Nous allons maintenant définir un opérateur \enquote{d'implémentation} noté $\triangleright$, qui décrit l'idée qu'une class table $\mathcal{A}$ implémente une \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}$). + 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] @@ -487,7 +487,7 @@ \label{fig:typops} \end{figure} - Grâce à ces méthodes, nous pouvons réutiliser les règles de typage de Featherweight Java presque à l'identique, qui sont rappelées \autoref{fig:typti}. Nous avons enlevé la règle de typage \textsc{T-SCast} qui autorisait les casts que les auteurs qualifiaient de \enquote{stupides}, entre deux types qui n'étaient pas parents l'un de l'autre. + 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 @@ -551,6 +551,9 @@ 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}$. @@ -590,7 +593,7 @@ \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éfini précédemment, nos preordres ne permettent pas de différencier ces deux expressions. En effet, puisque aucune des deux ne se réduit en une valeur, on est dans une situation 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: + 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} @@ -656,16 +659,16 @@ \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 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. + 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 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. + 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=FeatherweightJava,breaklines=true,linerange={2-26}]{FinalExample.java} + \lstinputlisting[language=Java,breaklines=true,linerange={2-26}]{FinalExample.java} \end{tcolorbox} \caption{Première \eng{class tables}} \label{fig:equivex:first} @@ -673,7 +676,7 @@ \begin{figure} \begin{tcolorbox} \small - \lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={29-62}, texcl]{FinalExample.java} + \lstinputlisting[language=Java,breaklines=true,linerange={29-62}, texcl]{FinalExample.java} \end{tcolorbox} \caption{Seconde \eng{class tables}} \label{fig:equivex:second} @@ -687,11 +690,11 @@ \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 manquerai un théorème qui permettrai 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). + 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 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. + 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. @@ -699,7 +702,7 @@ 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 aimerai 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. + 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. @@ -712,7 +715,12 @@ \endgroup \newpage + \addappheadtotoc \appendix + \addtocontents{toc}{\protect\setcounter{tocdepth}{-1}} + \appendixpage + + \section{Classes et Notations en FeatherweightJava} \label{anx:moreclass} @@ -736,7 +744,7 @@ \fjmethod{Bool}{gt}{Int other}{false} \fjmethod{Bool}{lt}{Int other}{other.isZero().ite(false,true)} }\\ - \fjclass{SInt}{\fjattr[Int]{prec}}{ + \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))} @@ -1140,7 +1148,7 @@ Nous avons donc toutes les conditions réunies pour appliquer l'hypothèse de récurrence. - \underline{La réduction s'est faîte entre un nœud de $h$ et un nœud de $\varepsilon$} + \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$. @@ -1189,6 +1197,6 @@ \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 à cause de la periode 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·e. 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. + 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} diff --git a/header.tex b/header.tex index da36389..b23397a 100644 --- a/header.tex +++ b/header.tex @@ -32,6 +32,8 @@ \usepackage{enumitem} \usepackage{amsfonts} \usepackage{mathtools} +\usepackage[page,header]{appendix} +\usepackage{minitoc} \usepackage{geometry} @@ -114,6 +116,9 @@ \newcommand{\hypitem}{\if@closemathitem$\fi\orig@item\if@mathitemize\@closemathitemtrue$\fi} \newenvironment{hyps}{\let\item\hypitem \@mathitemizetrue\hypenumerate\@closemathitemfalse}{$\endhypenumerate} \makeatother +% Remove part +\renewcommand \thepart{} +\renewcommand \partname{} %%% Subparaghaphs box @@ -157,6 +162,11 @@ {è}{{\`e}}1 {ù}{{\`u}}1 } +\lstset{literate=% + {à}{{\`a}}1 + {é}{{\'e}}1 + {è}{{\`e}}1 + {ù}{{\`u}}1} %% Commande 4 \NewDocumentEnvironment{textenv}{b}{\text{\textnormal{#1}}}{}