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

Prise en compte des commentaire de Clément, Partie 2

Browse Source
This commit is contained in:
Mysaa 2022-08-06 20:59:22 +02:00
parent b139cc06dd
commit 4848e9d71a
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
3 changed files with 124 additions and 69 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
NotesSurCommentairesClement.md
View File

@ -5,3 +5,39 @@ J'ai appris qu'il fallait notifier le responsable des stages si le titre du Rapp
- 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
### 4 - Pourquoi le paramètre k
Je voulais juste indiquer que les expressions à trous n'étaient pas toutes marquées $h$, mais en incluant toutes les déclinaisons.
### 4 - Le titre de 2.2
Est-ce que le nouveau titre fonctionne ?
### 4 - Définition appel static
Est-ce plus clair maintenant ?
### 5 - Incompréhension sur null
Je n'ai pas vraiment compris l'incompréhension, je traiterai cette partie plus tard, en voyant si elle me sert ou pas.
### 6 - Sur la définition des trous dégénérés
Le contenu de cette section n'est pas très rigoureux. C'est une sorte de présentation des différentes choses que j'ai éssayé avant d'en arriver à la définition des *test interfaces*. Elle a plutôt pour but d'indiquer à læ lecteur·ice pourquoi j'ai été ammené à considérer uniquement les *class tables*, et que j'ai ajouté des restriction sur les champs/méthodes accessibles. De plus, ais-je vraiment le temps de faire un théorème. Il y a d'autres cas différents en plus, parce qu des objets infinis ne pouvant pas être instanciés complètement, ils ne peuvent pas discriminer deux *class tables*.
### 7 - Problème des class tables qui ne pourraient pas être comparées.
Je l'ai mal formulé dans le document, mais le problème est justement que ces classes seraient vues équivalentes, sans jamais être en pratique vraiment comparées (universalité du vide).
### 8 - Sauf éventuellement Object
Le éventuellement réferrait à l'utilisation qui est éventuelle. Si la classe Object n'est pas utilisée, la règle n'impose rien.
### 8 - Ordre des définitions
Les différentes règles supplémentaires font à mon avis partie de la définition de la grammaire des *test interface*, c'est pour cela que ne voulais pas intercaler la définition de l'opérateur d'implémentation. L'explication informelle du sens des règles explique déjà leur sens vis-à-vis des *class tables*. J'ai rajouté une phrase, à voir si vous pensez si ça suffit.
### 10 - On suppose toujours que A est bien typé
Et bien, certaines des *class tables* que l'on manipule ne sont pas typées par elles-même, c'est le cas des *class tables* supplémentaires que l'on utilise pour les tests, que l'on concatène ensuite avec la *class table* testée pour obtenir notre environnement d'execution. Le «A OK» fait référence au typage des *class* défini dans le papier original.
Du point de vue formel, une class table est un ensemble de classes, et une classe est rarement typée par elle-même.
J'ai ajouté cette phrase, parce que pendant la preuve, j'ai eu besoin d'utiliser cet argument.
### 11 - Pourquoi A
Dans tous le document, à partir de la définition des *test interfaces*, j'ai utilisé comme convention que **A** représentait la class table *testée*, c'est à dire celle qui prenait la place de l'interface (d'où son utilisation dans la définition de l'opérateur d'implémentation), et que **B** représentait la class table de tests, qu'on ajoute afin d'avoir une batterie de tests plus puissante (d'où son utilisation dans la définition des opérateurs).
Cela facilite surtout la lecture de la preuve 1, parce que alors les définitions collent aux définitions en place, il n'y a pas de renommage peu lisible à faire.
### 11 - Sur la notation C'
La notation C' est effectivement plus claire que C0, mais mon problème est que ce n'est pas un nom de classe FJ valide. Est-ce que c'est vraiment génant ?

156
RapportStage.tex
View File

@ -81,37 +81,36 @@
\caption{Définition de la classe Paire}
\label{fig:pairedef}
\end{figure}
\subsection{Définitions supplémentaires}
\subsection{Définitions et raccourcis de programmation}
Nous allons aussi ajouter la grammaire des expressions à trou notés $h$, $h_k$:
\[h := \hole \spacebar \fj{$h$.f} \spacebar \fj{$h$.m($\overline{e}$)} \spacebar \fj{$e$.m($\overline{e}$,$h$,$\overline{e}$)} \spacebar \fj{new C($\overline{e}$,$h$,$\overline{e}$)} \spacebar \fj{(C) $h$}\]
Nous allons définir en sus la grammaire des expressions à trou notés $h$, $h'$, $h_k$:
\[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 classique, définie récursivement:
Puis on ajoute l'opération de \emph{remplissage} $h[e]$ pour $h$ expression à trou et $e$ expression quelconque, définie récursivement:
\begin{align*}
\fj{x}[e] &= \fj{x}\\
\hole[e] &= e\\
(\fj{new C($\overline{e_1}$,$h$,$\overline{e_2}$)})[e] &= \fj{new C($\overline{e_1}$,$h[e]$,$\overline{e_2}$)}\\
(\fj{$h$.f})[e] &= \fj{$h[e]$.f}\\
(\fj{$h$.m($\overline{e}$)})[e] &= \fj{$h[e]$.m($\overline{e}$)}\\
(\fj{$e$.m($\overline{e}$,$h$,$\overline{e}$)})[g] &= \fj{$e$.m($\overline{e}$,$h[g]$,$\overline{e}$)}\\
(\fj{new C($\overline{e}$,$h$,$\overline{e}$)})[g] &= \fj{new C($\overline{e}$,$h[g]$,$\overline{e}$)}\\
(\fj{$h$.m($\overline{e_1}$)})[e] &= \fj{$h[e]$.m($\overline{e_1}$)}\\
(\fj{$e_1$.m($\overline{e_2}$,$h$,$\overline{e_3}$)})[e] &= \fj{$e_1$.m($\overline{e_2}$,$h[e]$,$\overline{e_3}$)}\\
(\fj{(C) $h$})[e] &= \fj{(C) $h[e]$}
\end{align*}
Au niveau de la programmation en Featherweight Java, 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 dirèctement. En pratique, On remplacera les appels à méthodes de type \fj{meth($\overline{e}$)} par \fj{new Static().meth($\overline{e}$)}.
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}$)}.
Enfin nous définissons plusieurs classes qui permettent de coder avec un niveau plus haut, dont les définitions complètes sont données en \autoref{anx:moreclass}.
Enfin nous définissons plusieurs classes qui permettent de coder de façon plus abstraite, dont les définitions complètes sont données en \autoref{anx:moreclass}.
La première classe définie est la classe \fj{Bool}, liée à deux constantes \fj{true} et \fj{false}. Cette classe met à disposition une méthode \fj{ite(Object,Object)} telle que \fj{true.ite($t$,$f$)} renvoie $t$ et \fj{false.ite($t$,$f$)} renvoie $f$.
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)} 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 à plein de constantes \fj{0}, \fj{1}, \fj{2}, \dots. Cette classe met a disposition une méthode \fj{Bool isnull()} qui renvoie un booléen adéquat selon si l'entier testé est null ou pas. 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.
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
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}).
Aussi, nous définirons souvent implicitement 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 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
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.
@ -125,8 +124,8 @@
\subsection{Explication de l'utilité d'un contexte}
Les équivalences entre les programmes sont habituellement fait 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 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\].
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:
\[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.
Mais le plus gros problème est de déterminer ce qu'est un contexte. La tâche est d'autant plus difficile en Featherweight Java car un programme n'est pas constitué que d'une expression, comme en λ-calcul ou en π-calcul. Une expression seule n'a même aucun sens sans une \eng{class table} associée.
@ -136,22 +135,24 @@
\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 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 ce c'est une vraie limitation.
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
Un autre problème est celui dit du trou dégénéré. En effet, beaucoup de \eng{class tables} permettent de créer un \eng{trou dégénéré}, c'est à dire que pour toute expression $e$, il existe une expression à trou $h$ telle que $\forall p h\bracket{p} \rightarrow^* e$.
Un exemple de trou dégénéré est l'expression trouée suivante donnée pour $e$ expression, avec la classe \fj{Paire} dans la \eng{class table}
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
\[\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}\]
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.
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 Featherweigth Java, 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 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 est ainsi robuste, mais inefficace.
La relation créée en utilisant de simples expressions à trou comme contextes est ainsi robuste, mais inefficace.
\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}. Ainsi, l'application du contexte $C = (\mathcal{C},h)$ au programme donne
\[C\bracket{P} = (\mathcal{C} \oplus CT_P,h\bracket{e_P})\]
(le $\oplus$ dénote un α-renommage évitant que les définitions s'écrasent les unes les autres)
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
\[C\bracket{P} = (\mathcal{C} \oplus \mathcal{A},h\bracket{e_P})\]
(le $\oplus$ dénote un α-renommage évitant que les définitions s'écrasent les unes les autres).
Hélas, cela renforce le second problème, car il existe alors forcément un trou dégénéré dans une \eng{class table} $\mathcal{C} \oplus CT_P$ (on n'a qu'à rajouter une classe ressemblant à \fj{Paire}).
@ -165,11 +166,11 @@
\[C\bracket{P} = (\mathcal{C}, h\bracket{e})\qquad \underline{\text{si } \mathcal{A} \prec \mathcal{C}}\]
Cette condition restreint le nombre de contextes pouvant transformer un programme, et donc transforme le préordre en
\[P \prec Q \iff \forall C\quad
\left|\begin{array}{l}CT_P \prec CT_C\\ CT_Q \prec CT_C \\
\[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. \]
Cependant, cette définition pose un problème lorsque l'on cherche à copmarer 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}$.
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}$.
\begin{figure}
\begin{multicols}{2}
@ -207,27 +208,28 @@
(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.
\section{Des tests plus ciblés}
\paragraph{Abandon de l'expression \fj{main}}
Tous les tests vus 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, nous allons souvent comparer uniquement des librairies, ce qui correspondrai à 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.
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.
En bonus, l'étude des \eng{class tables} est tout aussi complète que l'étude des programmes entiers, car nous pouvons toujours rajouter une classe \fj{Main} qui n'aie qu'une méthode \fj{Main.main} dont le corps soit l'expression de notre programme. Alors tester cette nouvelle \eng{class table} reviendra à tester le programme entier.
%TODO Ajouter un exemple, ou faire un théorème
\paragraph{Idée d'une nouvelle structure}
Le problème de tous les contextes ci-dessus est qu'ils imposent tous une structure trop précise aux \eng{class tables} comparées. Elles doivent toutes avoir impérativement les mêmes classes, attributs et méthodes, là où on aimerai justement les comparer sur certaines classes, attributs ou méthodes.
Le problème de tous les contextes ci-dessus est qu'ils imposent tous une structure trop précise aux \eng{class tables} comparées. Elles doivent toutes avoir impérativement les mêmes classes, attributs et méthodes, là où on aimerait justement les comparer sur certaines classes, attributs ou méthodes.
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 (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}.
Le terme interface n'est pas anodin, la structure ressemble à une interface Java (ou Featherweigth Java \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}.
\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.
Un exemple concret de \eng{test interface} est donnée \autoref{fig:tiexample}. On y définit des classes \fj{Int}, \fj{Frac}, \fj{Number} et \fj{RichInt} telles que l'on puisse appeler certaines méthodes sur elles. On impose aussi de pouvoir construire les object \fj{Frac} avec deux paramètres de type \fj{Int}, et on impose aussi un attribut nommé \fj{value} dans la classes RichInt.
\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.
\begin{figure}
\ttfamily
@ -237,29 +239,32 @@
\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{(?|f)}}$) & \qquad \newtag{\textrm{\textsc{TSG-Cstr}}}{rule:tsg:constructor} \\
| & C :> C & \qquad \newtag{\textrm{\textsc{TSG-Cast}}}{rule:tsg:cast}
| & 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}
\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
\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}.
\begin{figure}
\begin{fjlisting}
Number \{\}\\
Int \{\}\\
Int : Int suivant(Int)\\
Int : Int add(Int,Int)\medskip
Int : Int add(Int,Int)\\
Int <: Number\\++
Frac(Int numerateur, Int denominateur)\\
Frac : Frac inverted()\\
Frac : Int floor()\medskip
Number \{\}\\
Frac : Int floor()\\
Frac <: Number\\
Int <: Number\medskip
RichInt \{Int value\}\\
RichInt : Int getInt()\\
@ -274,18 +279,19 @@
\begin{itemize}
\item Chaque nom de classe est défini au plus une fois par une \autoref{rule:tsg:attributes} ou une \autoref{rule:tsg:constructor}.
\item Chaque nom de methode est défini au plus une fois par nom de classe par une \autoref{rule:tsg:method}.
\item Les noms de classe utilisés sont définis (sauf éventuellement Object).
\item Les noms de classe utilisés sont définis (sauf éventuellement \fj{Object}).
\end{itemize}
Les deux règles \ref{rule:tsg:attributes} et \ref{rule:tsg:constructor} sont mutuellement exclusives pour un nom de classe donnée. La différence est que la seconde autorise l'appel au constructeur (l'expression \fj{new C(...)}) et imposant un ordre sur les paramètres là ou la seconde n'autorise pas le constructeur, et n'impose donc pas d'ordre sur les attributs.
Il peut sembler au premier abord qu'il manque à cette définition des \eng{test sets} une façon de définir la constructabilité d'un objet et certains nom d'attributs sans en préciser l'ordre. Cependant, avec un test simple, si l'on peut construire et accéder à un certain attribut \fj{field} sur un type \fj{C}, Si 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 pour chaque nom de classe \fj{Pk} des paramètres 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{PP\_k}, et on aura ainsi accès à l'indice du paramètre 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}\]
% TODO Ajouter une note sur l'abscence de tolérance lorsque les champs sont spécifiés.
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 \{\}}.
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 complèxes à exprimer apparaîssent, nous n'allons pas chercher à les exprimer ici, mais vous trouverez des exemples de telles class tables en \autoref{fig:tiUnsolvable}
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.
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}\]
% TODO Ajouter une note sur l'abscence de tolérance lorsque les champs sont spécifiés.
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}
\begin{figure}
\begin{center}
@ -322,10 +328,9 @@
\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 \enquote{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 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}
\ttfamily
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
\refstepcounter{rule}
\begin{center}
@ -350,8 +355,8 @@
\infer
{\mathcal{A} \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]}
{\begin{array}{l}
\exists \overline{\fj{f'}}\quad \overline{\fj{f0}} = \overline{\fj{f}}+\overline{\fj{f'}} \\
\exists \overline{\fj{E'}} \quad \overline{\fj{F}} = \overline{\fj{E}} \backslash \overline{\fj{E'}} \\
\exists \overline{\fj{f'}}\quad \overline{\fj{f0}} = \overline{\fj{f}}\boxplus\overline{\fj{f'}} \\
\overline{\fj{F}} = \overline{\fj{E}} \quad\text{où \fj{f} est défini} \\
\overline{\fj{E}} \subclass \overline{\fj{F}} \quad \land \quad
\overline{\fj{F}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)
\end{array}
@ -365,7 +370,13 @@
\end{tabular}
\end{center}
\end{tcolorbox}
\rmfamily
$\operatorname{mtype}_\mathcal{A}$ est une application qui renvoie le type de la méthode spécifiée de la classe spécifiée \cite[Fig.1]{fjdef}, dans la \eng{class table} $\mathcal{A}$.
$\operatorname{fields}_\mathcal{A}$ est une application qui renvoie la liste complète des attributs de la classe spécifiée \cite[Fig.1]{fjdef}, dans la \eng{class table} $\mathcal{A}$.
$\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}}
\label{fig:tiDefImpl}
\end{figure}
@ -374,9 +385,17 @@
\subsection{Définition du typage et d'un premier préordre}
Maintenant, nous allons définir le typage d'expressions dans une \eng{test interface}. L'opérateur de typage sera noté $\Vdash$ pour la différencier de celle définie dans Featherweight Java, notée $\vdash$. Une expression sera sera typée sous une \eng{test interface} $\mathfrak{T}$, une \eng{class table} $\mathcal{B}$ et un environnement de typage $\Gamma$.
Maintenant, nous allons définir le typage d'expressions dans une \eng{test interface}. L'opérateur de typage sera noté $\Vdash$ pour le différencier de celui défini dans FJ \cite[Fig.2]{fjdef}, notée $\vdash$. Une expression sera typée sous une \eng{test interface} $\mathfrak{T}$, une \eng{class table} $\mathcal{B}$ et un environnement de typage $\Gamma$.
Pour simplifier les définitions, nous allons rajouter une nouvelle application $\operatorname{construct}$ en plus des applications $\operatorname{fields}$, $\operatorname{mtype}$ et $\operatorname{mbody}$ qui sont définies dans le papier original, et que nous allons aussi surcharger. Maintenant, ces fonctions \enquote{recherchent} à la fois dans la \eng{class table} et dans la \eng{test interface}. Les définitions étendues sont présentées \autoref{fig:typops}.
Pour simplifier la définition du typage, nous allons (re)définir les applications suivantes :
\begin{description}
\item[\underline{$\operatorname{fields}$}] renvoie l'ensemble des attributs de la classe spécifiée.
\item[\underline{$\operatorname{mtype}$}] renvoie le type de la méthode spécifiée dans la classe spécifiée.
\item[\underline{$\operatorname{mbody}$}] renvoie le corps de la méthode spécifiée dans la classe spécifiée (donc une expression avec variables).
\item[\underline{$\operatorname{construct}$}] renvoie le type du constructeur de la classe spécifiée, c'est à dire la liste finie des types des paramètres.
\end{description}
Ces applications étaient déjà définies dans le papier original \cite[Fig.1]{fjdef} et \enquote{recherchaient} dans une simple \eng{class table}, notre redéfinition les définit recherchant dans une \eng{class table} mais aussi dans une \eng{test interface}. Les définitions étendues sont présentées \autoref{fig:typops}.
\begin{figure}
@ -397,7 +416,7 @@
{\left[\fj{ C \{ $\overline{\texttt{D}}\;\overline{\texttt{f}}$\}}\right] \in \mathfrak{T}}
& \newtag{\textrm{\textsc{LTi-Attr}}}{rule:lti-fields}\\[1em]
\infer
{\operatorname{fields}(\fj{C}) = \underbrace{\overline{\fj{D}}\;\overline{\fj{f}}}_{\text{\textrm{\fj{f} défini}}} + \bigcup_{C \subclass E}\operatorname{fields}(\fj{E})}
{\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]
\infer
@ -414,7 +433,7 @@
& \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{C0}) = \overline{\fj{D}}\rightarrow\fj{E}\quad \fj{C} \subclass \fj{C0}}
{\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}
\end{tabular}
\end{center}
@ -426,7 +445,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 \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, 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}
@ -468,23 +487,22 @@
\caption{Typage des expressions avec une \eng{test interface} et une \eng{class table}}
\label{fig:typti}
\end{figure}
Nous allons maintenant vérifier la définition de cette opération de typage $\Vdash$ en démontrant le théorème suivant:
\begin{theorem}
\label{thm:tiTyp}
Soit une \eng{test interface} $\mathfrak{T}$, une \eng{class table} $\mathcal{A}$ et un test $(\mathcal{B},e)$ vérifiant
Soit une \eng{test interface} $\mathfrak{T}$, une \eng{class table} $\mathcal{A}$, un couple $(\mathcal{B},e)$ \eng{class table} $\times$ expression fermée appelée \enquote{test}, et un environnement de typage $\Gamma$ vérifiant
\begin{itemize}
\item $\mathcal{A} \triangleright \mathfrak{T}$
\item $\mathcal{B} \OKin \mathfrak{T}$
\item $\mathfrak{T},\mathcal{B} \Vdash e : \fj{D}$
\item $\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D}$
\end{itemize}
Alors il existe \fj{C} tel que $\mathcal{A} \oplus \mathcal{B} \vdash e : \fj{C}$ et $\fj{C} \subclass \fj{D}$.
Cette dernière condition est nécessaire à cause de la tolérance de l'opérateur $\triangleright$.
Alors il existe \fj{C} tel que $\mathcal{A} \oplus \mathcal{B},\Gamma \vdash e : \fj{C}$ et $\fj{C} \subclass \fj{D}$.
\end{theorem}
Cette dernière condition est nécessaire à cause de la tolérance de l'opérateur $\triangleright$.
Ce théorème se prouve par induction sur la preuve de $\mathfrak{T},\mathcal{B} \Vdash e : \fj{D}$. La preuve est donnée en \autoref{anx:proofTyptyp}.
On peut alors définir un préordre sur les \eng{class tables} de la manière suivante.
@ -500,7 +518,7 @@
\mathcal{A}\oplus\mathcal{B} \Downarrow v
\end{array}\right. \implies \mathcal{A'}\oplus\mathcal{B}\Downarrow v\]
\end{definition}
%TODO Ajouter un exemple
\subsection{Renforcement de ce préordre avec les valeurs infinies}
@ -615,10 +633,10 @@
\subsection{Les entiers}
\begin{fjlisting}
\fjclass{Int}{}{
\fjmethod{Bool}{isNull}{}{true}
\fjmethod{Bool}{isZero}{}{true}
}\\
\fjclass{SInt}{\fjattr[Int]{prec}}{
\fjmethod{Bool}{isNull}{}{false}
\fjmethod{Bool}{isZero}{}{false}
}
\end{fjlisting}

1
header.tex
View File

@ -66,6 +66,7 @@
\newcounter{rule}
\addto\extrasfrench{%
\renewcommand{\figureautorefname}{\textsc{Figure}}
\renewcommand{\appendixautorefname}{Annexe}
\providecommand\ruleautorefname{règle}
}