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

Prise en compte des commentaires de Clément, partie 1

Browse Source
This commit is contained in:
Mysaa 2022-08-04 18:38:54 +02:00
parent 5c830b50d7
commit b139cc06dd
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
2 changed files with 43 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
NotesSurCommentairesClement.md Normal file
View File

@ -0,0 +1,7 @@
# Notes sur les commentaires de Clément
### 1 - Recherche du titre
J'ai appris qu'il fallait notifier le responsable des stages si le titre du Rapport devait être différent de celui du Stage. Cela me semble adéquat, le titre original étant « Revisiting Contextual Equivalences for Process Algebras ». Je n'ai étudié que partie du sujet, le Featherweight Java.
- Comparaison sémantique de programmes Featherweight Java (je ne suis pas sûr d'avoir encore complètement compris le sens du mot « sémantique »).
- Définition d'un préordre sur les programmes Featherweight Java
- Équivalences entre programmes orientés objets

67
RapportStage.tex
View File

@ -28,27 +28,43 @@
\section{Définitions et notations}
\subsection{Rappels de Featherweight Java}
\subsection{Rappel sur la définition de Featherweight Java}
Dans cette section, je vais rappeler quelques notations et définitions du langage Featherweight Java, qui ont déjà été présentées dans le papier original \cite{fjdef} et que je vais continuer d'utiliser dans ce document.
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}.
Je vais continuer d'utiliser la notation du sur-lignage afin d'indiquer une liste finie d'élément.
Par exemple, on notera $f(\overline{a})$ pour indiquer un appel du type $f(a_1,a_2,\dots,a_n)$.
On utilisera la notation du sur-lignage afin d'indiquer une liste finie d'élément.
Par exemple, on notera $f(\overline{a})$ pour indiquer un appel de la forme $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:
\[e = \fj{x} \spacebar \fj{new C($\overline{e}$)} \spacebar \fj{$e$.f} \spacebar \fj{$e$.m($\overline{e}$)} \spacebar \fj{(C)$e$}\]
On appellera \eng{class table} tout ensemble de définitions de classes, 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).
\begin{center}
\refstepcounter{rule}
\begin{tabular}{rll}
$e$ $:=$ & \fj{x} & \qquad \newtag{\textrm{\textsc{E-Var}}}{rule:expr:variable} \\
| & \fj{new C($\overline{e}$)} & \qquad \newtag{\textrm{\textsc{E-Cstr}}}{rule:expr:constructor} \\
| & \fj{$e$.f} & \qquad \newtag{\textrm{\textsc{E-Field}}}{rule:expr:field} \\
| & \fj{$e$.m($\overline{e}$)} & \qquad \newtag{\textrm{\textsc{E-Meth}}}{rule:expr:method} \\
| & \fj{(C)$e$} & \qquad \newtag{\textrm{\textsc{E-Cast}}}{rule:expr:cast}
\end{tabular}
\end{center}
où \fj{x} est un nom de variable, \fj{C} un nom de classe, \fj{f} un nom d'attribut de classe et \fj{m} un nom de méthode de classe.
Un \enquote{programme} Featherweight Java est un couple $(\mathcal{A},e)$ et est souvent noté $P$, $Q$, $R$. Cette expression est en quelque sorte le \eng{main} du programme On pourra noter $CT_P$ et $e_P$ pour accéder à la \eng{class table} et à l'expression du programme.
On dit d'une expression qui ne contient pas de noms de variable (\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}.
On appelle \enquote{valeur} toute expression composée uniquement de constructeurs.
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 note aussi $\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 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).
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'ambiguïté. On notera aussi $\rightarrow^*_\mathcal{A}$ ou $\rightarrow^*$ la cloture transitive et réflexive de la relation. On notera aussi $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$ ($v$ est une valeur).
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.
Cette relation est définie avec deux types de règles, les règles de type \textsc{R} qui indiquent :
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}$.
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 cloture transitive et réflexive de la relation. On notera enfin $e\Downarrow v$ lorsque $e \rightarrow^* v$ et $v$ est une valeur. On pourra même écrire $e \Downarrow$ pour dire $\exists v \quad e \Downarrow v$.
Cette relation est définie avec deux types de règles (
\cite[Fig.3]{fjdef}, les règles de type \textsc{R} qui indiquent :
\begin{itemize}
\item L'évaluation d'un attribut d'un objet (\textsc{R-Field})
\item L'évaluation d'une méthode (\textsc{R-Invk})
@ -62,8 +78,8 @@
\begin{fjlisting}
\fjclass{Paire}{\fjattr{fst} \fjattr{snd}}{}
\end{fjlisting}
\label{fig:pairedef}
\caption{Définition de la classe Paire}
\label{fig:pairedef}
\end{figure}
\subsection{Définitions supplémentaires}
@ -93,7 +109,7 @@
Aussi, nous définierons souvent les classes \fj{A}, \fj{B} et \fj{C}, qui n'ont pas d'attributs ni de méthode (ce sont des \enquote{objets simples}).
\subsection{Extension du FeatherWeight Java}
\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}\]
@ -175,8 +191,8 @@
}
\end{fjlisting}
\end{multicols}
\label{fig:nosurct}
\caption{\eng{Class tables} n'ayant pas de sur-\eng{class table} commune}
\label{fig:nosurct}
\end{figure}
En effet, en notant les expressions suivantes
@ -207,7 +223,7 @@
Le terme interface n'est pas anodin, la structure ressemble à une interface Java (ou Featherweigth Java \cite{liquori_fjInterfaces}), mais en plus rigoureuse. Une expression va \enquote{compiler} (c'est à dire être typée) contre l'interface, puis sera \enquote{executée} (c'est à dire réduite) contre des vraies \eng{class tables}.
\subsection{Définition de la structure de \eng{Test Interface}}
\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 teste interface est alors simplement un ensemble de \eng{test interface rules}, et sera noté $\mathfrak{T}$, $\mathfrak{U}$, $\mathfrak{V}$. La règle \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.
@ -300,8 +316,8 @@
\end{fjlisting}
\end{tabular}
\end{center}
\label{fig:tiUnsolvable}
\caption{Exemples de \textit{test interfaces} implémentés par aucune \textit{class table}}
\label{fig:tiUnsolvable}
\end{figure}
\paragraph{Opérateur d'implémentation}
@ -486,7 +502,7 @@
\end{definition}
\subsection{Renforcage de ce préordre avec les valeurs infinies}
\subsection{Renforcement de ce préordre avec les valeurs infinies}
Nous souhaiterions pouvoir démontrer un \eng{context lemma} sur les préordres précédents, c'est à dire un théorème qui dise que pour toute expression à trou $h$
@ -501,8 +517,8 @@
\fjmethod{IList}{zeroList}{}{new IList(0, zeroList())}
}
\end{fjlisting}
\label{fig:ilistsDefs}
\caption{Définitions de listes infinies}
\label{fig:ilistsDefs}
\end{figure}
Par exemple, avec la \eng{class table} définie \autoref{fig:ilistsDefs}, nous pouvons considérer les deux expressions $e_i = \fj{intList(0)}$ et $e_0 = \fj{zeroList()}$. Tels que nous les avons dé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 de $\text{faux}\implies\text{faux}$. 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:
@ -570,17 +586,6 @@
La démonstration est présentée en annexe (\autoref{anx:proofHValCL})
\marginpar{Besoin de présenter rapidement la preuve}
\end{property}
\section{Vers des équivalences plus pratiques}
\subsection{Une équivalence entre les expressions}
\subsection{Cette équivalence est trop forte}
\subsection{L'équivalence méthode par méthode}
\section{Conclusion}
@ -807,7 +812,7 @@
\subparagraph{\textnormal{\textsc{\ref{rule:ti:downCast}}}}
Exactement la même preuve que le point précédent en appliquant la règle \textsc{T-UCast}
\section{Preuve du \eng{context lemma} avec les valeurs infinies}
\section{Preuve du \eng{context lemma} avec valeurs infinies}
\label{anx:proofHValCL}
Nous allons démontrer une version un peu plus puissante de ce théorème, ce qui simplifiera l'induction que nous ferrons.
@ -847,7 +852,7 @@
On suppose que $h\bracket{\varepsilon} = \hbar\bracket{\overline{e'}}$.
\subparagraph{Cas $\hbar = \hole$}
\subparagraph{Cas $\hbar = \hole$}¨
Alors
\[h\bracket{\gamma} = \hbar\bracket{\overline{f'}}\quad\text{avec}\quad \overline{f'} = \left(h\bracket{\gamma}\right)\]