From 6252c993e89b2589009bcd75584836e138076b70 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Tue, 19 Jul 2022 12:30:52 +0200 Subject: [PATCH] Ajout des commentaires visibles. --- RapportStage.tex | 34 ++++++++++++++-------------------- 1 file changed, 14 insertions(+), 20 deletions(-) diff --git a/RapportStage.tex b/RapportStage.tex index 1fa8ee9..d926ad5 100644 --- a/RapportStage.tex +++ b/RapportStage.tex @@ -94,7 +94,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} - + \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}\] @@ -412,7 +412,7 @@ 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. - Nous vérifions aussi évidement la \eng{class table} $\mathcal{B}$, en vérifiant que le corps de chaque méthode est bien typé par le type attendu dans la méthode, que les champs de la \eng{class table} ne contredisent pas la \eng{test interface}. On note alors $\mathcal{B} \OKin \mathfrak{T}$. Les seules contradictions sont grammaticales si l'on a déjà vérifié que les applications $\operatorname{fields}$, $\operatorname{construct}$ et $\operatorname{mtype}$ n'étaient pas redéfinies ou mal définies.%TODO à prouver + 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} \begin{figure} \begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue] @@ -533,13 +533,13 @@ La grammaire est la suivante, on définit également l'opération de remplissage des trous, comme fait pour la définition des expressions à trou. \[\hbar := \hole \spacebar \fj{new C($\overline{\hbar}$)}\] - %TODO y a t'il besoin de redéfinir le remplissage des trous ? + \marginpar{y a t'il besoin de redéfinir le remplissage des trous ?} Nous alons alors pouvoir redéfinir le préordre sur deux programmes : \[(\mathcal{A},e)\pprec(\mathcal{B},f) \ssi \forall \hbar \forall \overline{e'} \quad \left(e \rightarrow_\mathcal{A}^* \hbar\left[\overline{e'}\right] \implies \exists \overline{e''}\quad f \rightarrow_\mathcal{B}^* \hbar \left[\overline{e''}\right]\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. - %TODO Cette expression me semble peu claire. + \marginpar{Cette expression me semble peu claire.} On redéfit ainsi 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)\] @@ -550,7 +550,7 @@ $$\forall \hbar \forall \overline{e} \quad \hbar\left[\overline{e}\right]\rightarrow e' \implies \exists \overline{e''}\quad e' = \hbar\left[\overline{e''}\right]$$ On peut prouver cette propriété inductivement en montrant qu'une expression ayant un nœud \enquote{\fj{new}} en nœud racine se réduira forcément en une expression ayant un nœud racine du même type, en inversant la relation de réduction. - %TODO y a t'il besoin d'une preuve plus complète ? + \marginpar{y a t'il besoin d'une preuve plus complète ?} \end{property} \begin{property} @@ -568,7 +568,7 @@ \end{gather*} La démonstration est présentée en annexe (\autoref{anx:proofHValCL}) - %TODO Présenter rapidement la preuve + \marginpar{Besoin de présenter rapidement la preuve} \end{property} @@ -807,7 +807,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} - \subsection{Preuve du \eng{context lemma} avec les valeurs infinies} + \section{Preuve du \eng{context lemma} avec les valeurs infinies} \label{anx:proofHValCL} La première étape est de décomposer l'opérateur $\pprec$, et de changer l'ordre des opérateurs. Nous cherchons donc à prouver que @@ -821,7 +821,7 @@ On écrit $\rightarrow$ au lieu de $\rightarrow_{\mathcal{A}\oplus\mathcal{B}}$, afin d'alléger les notations. Nous allons montrer un peu plus en considérant que $h$ est une expression avec un nombre quelconque de trous (mais tous remplacés par la même expression). - %TODO: Y a t'il besoin de préciser le remplissage de ces expressions ? + \marginpar{Y a t'il besoin de préciser le remplissage de ces expressions ?} Nous allons montrer le théorème en deux temps. D'abord, nous allons imposer comme contrainte que la réduction $h\bracket{e} \rightarrow^* \hbar\bracket{\overline{e'}}$ s'effectue sans application de méthode (\textsc{R-Meth}) à un appel à méthode contenu dans $h$. (C'est à dire que les appels à méthode de $h$ ne \enquote{servent à rien}, ils pourraient être remplacés par \fj{null} sans modifier la réduction). @@ -837,23 +837,17 @@ \subparagraph{$h = \hole$} On applique dirèctement $H_0$ - \subparagraph{$h = \fj{new D($e_1$,...,$e_{i-1}$,$h^\prime$,$e_{i+1}$,...,$e_{k^\prime}$)}$} + \subparagraph{$h = \fj{new D($h^\prime_1$,...,$h^\prime_{k^\prime}$)}$} Alors, \fj{D}=\fj{C} et $k'=k$ car $\fj{new D(...$\null_{k^\prime}$)} \rightarrow^* \fj{new C(...$\null_k$)}$ - Aussi, on a pour chaque $j$, $e_j \rightarrow^* \hbar_j\bracket{\overline{e'}^j}$ + Or, pour chaque $i$, $h'_i\bracket{e} \rightarrow^*\hbar_i\bracket{\overline{e'}^i}$, qui n'utilise pas de réduction de méthode (car sinon, la réduction de $h\bracket{e_1}$ en utiliserai). - Donc \[h\bracket{f} = \fj{new C($e_1$,...,$e_{i-1}$,$h^\prime\bracket{e_2}$,$e_{i+1}$,...,$e_k$)}\] + Donc, en appliquant l'hypothèse d'induction à chaque $h'_i$, on obtient que \[h'_i\bracket{f} \rightarrow^*\hbar_i\bracket{\overline{f'_i}}\]. - Donc \[h\bracket{f}\rightarrow^*\fj{new C($\hbar_1\bracket{\overline{e^\prime}^1}$,...,$h'\bracket{f}$,...,$\hbar_k\bracket{\overline{e^\prime}^k}$)}\] + Donc \[h\bracket{f} \rightarrow^* \fj{new C($\hbar_i\bracket{\overline{f^\prime_1}}$,...,$\hbar_i\bracket{\overline{f^\prime_k}}$)} = \hbar\bracket{\overline{f''}}\] - Or, $h'\bracket{e} \rightarrow^*\hbar_i\bracket{\overline{e'}^i}$, qui n'utilise pas de réduction de méthode (car sinon, la réduction de $h\bracket{e_1}$ en utiliserai). - - Donc, en appliquant l'hypothèse d'induction à $h'$, on obtient que \[h'\bracket{f} \rightarrow^*\hbar_i\bracket{\overline{f'}}\]. - - Donc \[h\bracket{f} \rightarrow^* \fj{new C($\hbar_1\bracket{\overline{e^\prime}^1}$,...,$\hbar_i\bracket{\overline{f^\prime}}$,...,$\hbar_k\bracket{\overline{e^\prime}^k}$)} = \hbar\bracket{\overline{f''}}\] - - \[\overline{f''} = \overline{e'}^1 \| \dots \| \overline{e'}^{i-1} \| \overline{f'} \| \overline{e'}^{i+1} \| \dots \| \overline{e'}^k\] + \[\overline{f''} = \overline{f'_1} \| \dots \| \overline{f'_k}\] \subparagraph{$h = \fj{$h^\prime$.f}$} @@ -879,7 +873,7 @@ On a donc démontré le lemme pour tous les cas, il nous manque d'inclure les appels à méthode. - %TODO: Faut-il préciser cette notion de «appel à méthode dans h' + \marginpar{Faut-il préciser cette notion de «appel à méthode dans h'} \paragraph{Mélange de réduction} Nous allons maintenant transformer notre réduction afin de former une chaine sans appel à méthode dans l'expression à trou.