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

Prise en compte des remarques de Daniele, esquisse d'intro et de conclusion.

Browse Source
This commit is contained in:
Mysaa 2022-08-08 23:42:32 +02:00
parent e4178b644b
commit e31a43228a
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
1 changed files with 34 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

49
RapportStage.tex
View File

@ -20,14 +20,23 @@
\section{Introduction}
\subsection{Présentation du problème}
\subsection{Motivations de l'étude}
Ce document a été réalisé dans le cadre de mon stage réalisé au LACL à Créteil, plus de détails sont donnés en \autoref{anx:stage}.
\subsection{Présentation du problème}
Featherweight Java (abrégé en FJ) \cite{fjdef} est une formalisation, à l'instar du $\lambda$-calcul ou du $\pi$-calcul de la programmation en orienté objet (POO). Les programmes FJ ont leur syntaxe calquée depuis le language Java, et sont compilables avec un compilateur. On peut y définir classes, attributs et méthodes, mais pas d'assignation, les objets considérés étant tous immuables.
L'objectif du stage est de définir une équivalence (ou plutôt un préordre) entre les programmes FJ, comme l'on pourrait faire en $\pi$-calcul, 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, ont ensemble écrit un papier qui critiquait la manière peu rigoureuse mais surtout peu réaliste avec laquelle les équivalences entre programmes étaient habituellement définies dans la littérature, et proposent une nouvelle manière qui leur semble \enquote{meilleure} sous plusieurs aspects \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 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
\section{Définitions et notations}
\label{sec:defNots}
\subsection{Rappel sur la définition de Featherweight Java}
Dans cette section, je vais rappeler quelques notations et définitions du langage Featherweight Java \cite{fjdef}. Le lecteur souhaitant toutes les définitions complètes devra lire \cite[Section 1]{fjdef}.
@ -85,7 +94,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'$, $h_k$:
Nous allons définir en sus la grammaire des expressions à 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:
@ -123,10 +132,10 @@
\section{Étude d'équivalences simples}
\label{sec:eqsimpl}
\subsection{Explication de l'utilité d'un contexte}
Les équivalences entre les programmes sont habituellement définies en utilisant des \enquote{contextes}. Des programmes sont dits équivalents lorsqu'ils donnent les mêmes résultats sous tout contexte. Pour un contexte $C$, on va noter $C\bracket{P}$ l'interprétation d'un programme $P$ dans le contexte. Alors, le préordre sera défini comme tel:
Les équivalences entre les programmes sont habituellement définies en utilisant des \enquote{contextes}. Deux programmes sont dits équivalents lorsqu'ils donnent les mêmes résultats sous tout contexte. Pour un contexte $C$, on va noter $C\bracket{P}$ l'interprétation d'un programme $P$ dans le contexte. Alors, le préordre sera défini comme tel:
\[P\prec Q \ssi \forall C\quad C\bracket{P}\Downarrow v \implies C\bracket{Q}\Downarrow v\]
On confondra souvent les termes \enquote{équivalence} et \enquote{préordre} dans la suite de ce document, car le premier est plus pratique pour visualiser l'utilité des constructions établies.
@ -149,7 +158,7 @@
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.
La relation créée en utilisant de simples expressions à trou comme contextes est ainsi robuste, mais inefficace.
La relation créée en utilisant de simples expressions à trou comme contextes est ainsi robuste, mais trop restrictive pour être utile.
\paragraph{Une boîte à outils plus puissante}
Afin de permettre aux contextes d'être plus complets et d'ainsi résoudre le premier problème, on est d'abord tenté d'y accoler une \eng{class table} supplémentaire dite «de tests». Ainsi, l'application du contexte $C = (\mathcal{C},h)$ au programme $P = (\mathcal{A}, e_P)$ donne
@ -213,7 +222,7 @@
Alors, puisque aucun de nos \emph{contextes} ne satisfait les hypothèses, les deux programmes sont équivalents par universalité du vide.
\section{Des tests plus ciblés}
\label{sec:titech}
\paragraph{Abandon de l'expression \fj{main}}
Tous les tests présentés dans la section précédente visaient à tester un programme entier (une \eng{class table} et une expression). Il semble cependant étrange de procéder ainsi. En effet, un développeur souhaitera principalement comparer entre elles des librairies, ce qui correspondrait à nos \eng{class tables}. On ne cherche plus à savoir si deux programmes \enquote{font la même chose}, mais plutôt est-ce que ces deux \eng{class tables} fournissent les mêmes fonctions.
@ -292,7 +301,7 @@
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 interface} pour lesquelles il existe au moins une \eng{class table} les implémentant. Cela impose certaines règles, notamment que l'opération $\subclass$ induite puisse créer un bon ordre, mais d'autres contraintes plus 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 apparaîssent, nous n'allons pas chercher à les exprimer ici, mais vous trouverez des exemples de telles \eng{test interfaces} en \autoref{fig:tiUnsolvable}
\begin{figure}
\begin{center}
@ -573,8 +582,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 \fj{new C(...)}, alors l'autre coté s'évalue en un objet de la même classe, et ce récursivement.
\marginpar{Cette expression me semble peu claire.}
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.
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)\]
@ -601,11 +609,16 @@
\end{property}
Ce théorème était en quelque sorte l'objectif de cette redéfinition, puisque nous comparons dorénavant les expressions sur \enquote{toutes les valeurs qu'elles pourraient renvoyer}.
La demonstration 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}.
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}.
\section{Conclusion}
Nous avons donc créé un préordre en définissant une nouvelle structure de \eng{test interface}. Cette structure est à la fois assez puissante pour que l'on puisse tester profondément les programmes, mais aussi assez tolérante pour que l'équivalence ne s'arrête pas sur la moindre différence de grammaire. Nous avons aussi obtenu un \eng{context lemma} pour notre préordre, ce qui nous conforte dans son bon fondement.
La preuve complète des théorèmes a pris plus de temps que prévu, notamment à cause de la structure moins intuitive de la seconde, et elles mériteraient d'être formalisées dans un assistant de preuve comme Coq.
La structure de \eng{test interface} peut aussi être utilisée à d'autre fins, par exemple à la définition de librairies, ou de \enquote{modules} dans la terminologie de Java 9+.
\clearpage
\section{Bibliographie}
@ -982,5 +995,11 @@
On peut enfin appliquer l'hypothèse de récurrence de la même manière.
Enfin, dans le dernier cas $\fj{(D)x}$, puisque la réduction s'est bien effectuée, c'est que $\fj{C} \subclass \fj{D}$. On peut donc simplement remplacer dans $h$ le cast par la variable $\fj{x}$ seule.
\section{Le stage au LACL}
\label{anx:stage}
Je vais présenter ici le laboratoire dans lequel j'ai fait ce stage. Le Laboratoire d'Algorithmique, Complexité et Logique est un petit laboratoire inclus dans l'Université Paris-Est Créteil. Le laboratoire est donc dans un campus universitaire, et contient aussi quelques thésard·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.
\end{document}