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

Ajout de la preuve de la première propriété.

Browse Source
This commit is contained in:
Mysaa 2022-08-13 20:02:38 +02:00
parent c6e5368993
commit 396db085ec
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
2 changed files with 55 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

61
RapportStage.tex
View File

@ -483,8 +483,9 @@
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.
%TODO prouver l'affirmation
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}$.
%XXX Si le temps, rajouter cette ligne et la prouver
%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.
\begin{figure}
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
@ -617,11 +618,12 @@
Nous allons maintenant étudier les propriétés de cette nouvelle définition du préordre.
\begin{property}
\[\forall \hbar \forall \alpha \quad \hbar\bracket{\alpha}\rightarrow e' \implies \exists \beta\quad e' = \hbar\bracket{\beta}\]
\label{thm:hnewnew}
\[\forall \hbar \forall \alpha \quad \hbar\bracket{\alpha}\rightarrow^* e' \implies \exists \beta\quad e' = \hbar\bracket{\beta}\]
\end{property}
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 Preuve complète
La preuve complète est présentée \autoref{anx:proofPt1Val}.
\begin{property}
\[\mathcal{A} \pprec \mathcal{B} \implies \mathcal{A} \prec \mathcal{B}\]
@ -762,11 +764,11 @@
\begin{fjlisting}
\fjclass{Optional}{}{
\fjmethod{Object}{orElse}{Object e}{e}
}
}\\
\fjclass[Optional]{Some}{\fjattr{value}}{
\fjmethod{Object}{orElse}{Object e}{this.value}
}\\
\fjclass[Optional]{None}{}{}\\
\fjclass[Optional]{None}{}{}
\end{fjlisting}
Ces trois classes définissent la notion d'\fj{Optional} qui fonctionne comme \lstinline[language=Caml]|a' option| en OCaml, et qui peut contenir une valeur ou non. La méthode \fj{orElse} permet de récupérer la valeur contenue si elle est présente, ou de renvoyer le paramètre dans le cas contraire.
@ -793,7 +795,7 @@
Notez que le problème est le même sans la présence de la méthode \fj{getList}, on n'aurait alors pas pû discriminer les deux méthodes \fj{contains} pour un même argument, puisqu'il n'aurait alors pas été possible d'instancier un argument.
Bien sûr, avec une class table de tests, il est possible de créer des objets \fj{IList} de la forme que l'on souhaite, et donc de discriminer ces deux méthodes, par exemple avec une liste infinie de \fj{0}.
Bien sûr, avec une \eng{class table} de tests, il est possible de créer des objets \fj{IList} de la forme que l'on souhaite, et donc de discriminer ces deux méthodes, par exemple avec une liste infinie de \fj{0}.
\section{Preuve du théorème de cohérence du typage des \eng{test interfaces}}
\label{anx:proofTyptyp}
@ -960,7 +962,52 @@
\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-DCast}
\section{Preuve de la \autoref{thm:hnewnew} sur les valeurs infinies}
\label{anx:proofPt1Val}
Nous allons d'abord montrer la propriété sur les expressions suivante:
\begin{property}
\label{thm:enewnew}
Soit $e$ et $f$ des expressions fermées, telles que $e \rightarrow^* f$,
Alors, si $e = \fj{new C($\overline{e'}$)}$
On a $f = \fj{new C($\overline{f'}$)}$ et $\overline{e'} \rightarrow^* \overline{f'}$.
\end{property}
Montrons cette propriété par récurrence sur la taille de la relation $e \rightarrow^* f$.
\subparagraph{Initialisation}
Dans le cas $e = f$, on a simplement $f = \fj{new C($\overline{e'}$)}$ et $\overline{e'} \rightarrow^0 \overline{e'}$.
\subparagraph{Hérédité}
Nous sommes dans l'hypothèse que $e \rightarrow^n f$
Observons la première relation. Elle se fait nécessairement sur un nœud de type \ref{rule:expr:method}, \ref{rule:expr:field} ou \ref{rule:expr:cast}, qui est donc contenu dans l'un des $\overline{e'}$. Donc, on a $e'_i \rightarrow e''_i$. On note $e''_k = e'_k$ pour $k$ différent de $i$, et on obtient que
\[e = \fj{new C($\overline{e'}$)} \rightarrow \fj{new C($\overline{e''}$)} \rightarrow^{n-1} f\]
On peut donc appliquer l'hypothèse de récurrence à la dernière relation $\rightarrow^{n-1}$, et nous obtenons bien que
\[f = \fj{new C($\overline{f'}$)} \quad\text{et}\quad \overline{e'} \rightarrow^* \overline{e''} \rightarrow^* \overline{f'}\]
La récurrence est bouclée.
Nous allons donc pouvoir facilement montrer la \autoref{thm:hnewnew} par induction sur le paramètre $\hbar$.
\subparagraph{$\hbar = \fj{x}$}
Alors, en notant $\beta$ tel que $\beta(\fj{x}) = e'$.
Alors,
\[\hbar\bracket{\alpha} = \alpha(\fj{x}) \rightarrow e' = \hbar\bracket{\beta}\]
\subparagraph{$\hbar = \fj{new C($\overline{\hbar'}$)}$}
Alors, par application de la \autoref{thm:enewnew}, on obtient que
\[e' = \fj{new C($\overline{e}$)} \quad\text{et}\quad \overline{\hbar\bracket{\alpha}} \rightarrow^* \overline{e}\]
On peut alors appliquer l'hypothèse d'induction, et obtenir que
\[\overline{e} = \overline{\hbar\bracket{\beta_x}}\]
Donc, en notant $\beta$ la concaténation des $\beta_x$, qui est possible puisque les noms de variables utilisés dans $\hbar$ sont tous distincts, on obtient le résultat
\[e' = \hbar\bracket{\beta}\]
\section{Preuve du \eng{context lemma} avec valeurs infinies}
\label{anx:proofHValCL}

1
header.tex
View File

@ -70,6 +70,7 @@
\renewcommand{\figureautorefname}{\textsc{Figure}}
\renewcommand{\appendixautorefname}{Annexe}
\renewcommand{\theoremautorefname}{Théorème}
\providecommand\propertyautorefname{Propriété}
\providecommand\ruleautorefname{règle}
}