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

Ajout des commentaires visibles.

Browse Source
This commit is contained in:
Mysaa 2022-07-19 12:30:52 +02:00
parent 235fbfafb5
commit 6252c993e8
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
1 changed files with 14 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
RapportStage.tex
View File

@ -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.