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

Ajout de la preuve du premier théorème de typage.

Browse Source
This commit is contained in:
Mysaa 2022-07-15 14:46:29 +02:00
parent a9a5154c1e
commit ac36aa6a5e
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
2 changed files with 279 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

291
RapportStage.tex
View File

@ -192,7 +192,15 @@
\end{array}\]
\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.
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.
\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.
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.
@ -257,6 +265,7 @@
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 \{\}}.
@ -297,7 +306,7 @@
\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$.
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}$).
\begin{figure}
\ttfamily
@ -324,10 +333,12 @@
\infer
{\mathcal{A} \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]}
{\exists \overline{\fj{f'}}\quad
\overline{\fj{f0}} = \overline{\fj{f}}+\overline{\fj{f'}} \land
{\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'}} \\
\overline{\fj{E}} \subclass \overline{\fj{F}} \quad \land \quad
\overline{\fj{F}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)
\quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}}
\end{array}
}
&\newtag{\textrm{\textsc{(TRI-Cstr)}}}{rule:tri:constructor}\\[1em]
@ -347,7 +358,7 @@
\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{A}$ 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 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$.
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}.
@ -359,11 +370,11 @@
\begin{tabular}{c@{\hskip 6em}l}
\infer
{\operatorname{construct}(\fj{C}) = \overline{\fj{D}}}
{\fj{class C\{C($\overline{\texttt{D}}\;\overline{\texttt{f}}$)\{...\} ... \}}\in \mathcal{A}}
{\left[\fj{C($\overline{\texttt{D}}\;\overline{\texttt{?f}}$)}\right] \in \mathfrak{T}}
& \newtag{\textrm{\textsc{LTi-Cstr}}}{rule:lti-construct}\\[1em]
\infer
{\operatorname{construct}(\fj{C}) = \overline{\fj{D}}}
{\left[\fj{C($\overline{\texttt{D}}\;\overline{\texttt{?f}}$)}\right] \in \mathfrak{T}}
{\fj{class C\{C($\overline{\texttt{D}}\;\overline{\texttt{f}}$)\{...\} ... \}}\in \mathcal{B}}
& \newtag{\textrm{\textsc{LCt-Cstr}}}{rule:lct-construct}\\[1em]
\infer
{\operatorname{fields}(\fj{C}) = \overline{\fj{D}}\;\overline{\fj{f}} + \bigcup_{C \subclass E}\operatorname{fields}(\fj{E})}
@ -375,7 +386,7 @@
& \newtag{\textrm{\textsc{LTi-AttrC}}}{rule:lti-fields2}\\[1.5em]
\infer
{\operatorname{fields}(\fj{C}) = \overline{\fj{D}}\;\overline{\fj{f}} + \bigcup_{C \subclass E}\operatorname{fields}(\fj{E})}
{\fj{class C \{$\overline{\texttt{D}}\;\overline{\texttt{f}}$; ...\}} \in \mathcal{A}}
{\fj{class C \{$\overline{\texttt{D}}\;\overline{\texttt{f}}$; ...\}} \in \mathcal{B}}
& \newtag{\textrm{\textsc{LCt-Attr}}}{rule:lct-fields}\\[1em]
\infer
{\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}}
@ -383,7 +394,7 @@
& \newtag{\textrm{\textsc{LTi-MethC}}}{rule:lti-method}\\[1em]
\infer
{\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}}
{\fj{class C \{...; E m($\overline{\texttt{D}}\;\overline{\texttt{x}}$)\}} \in \mathcal{A}}
{\fj{class C \{...; E m($\overline{\texttt{D}}\;\overline{\texttt{x}}$)\}} \in \mathcal{B}}
& \newtag{\textrm{\textsc{LCt-Meth}}}{rule:lct-method}\\[1em]
\infer
{\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}}
@ -393,48 +404,48 @@
\end{center}
\end{tcolorbox}
\rmfamily
$\subclass$ dénote ici la cloture transitive et réflexive de l'union des relations $<:$ sur $\mathfrak{T}$ et $extends$ dans $\mathcal{A}$.
$\subclass$ dénote ici la cloture transitive et réflexive de l'union des relations $<:$ sur $\mathfrak{T}$ et $extends$ dans $\mathcal{B}$.
\caption{Opérateurs supplémentaires pour le typage}
\label{fig:typops}
\end{figure}
Grâce à ces méthodes, nous pouvons réutiliser les règles de typage de Featherweight Java à 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 \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{A}$, 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}. 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 ma définies.
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
\begin{figure}
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
\def\arraystretch{1.5}
\begin{tabular}{c@{\hskip 2em}l}
\infer
{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}
{\fj{x} \in \Gamma}
& \newtag{\textrm{\textsc{TI-Var}}}{rule:ti:variable}
\\[3ex]
\infer
{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{e.f} : \fj{E}}
{\mathfrak{T},\mathcal{A},\Gamma \Vdash e : \fj{C} \quad \fj{E}\;\fj{f} \in \operatorname{fields}(\fj{C})}
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}}
{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{C0} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{C0})}
& \newtag{\textrm{\textsc{TI-Field}}}{rule:ti:field}
\\[3ex]
\infer
{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{e.m($\overline{\texttt{e'}}$)} : \fj{R}}
{\begin{array}{c}\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{e} : \fj{C} \quad \mathfrak{T},\mathcal{A},\Gamma \Vdash \overline{\fj{e'}} : \overline{\fj{E}} \\[-1.4ex] \overline{\fj{E}} \subclass \overline{\fj{G}} \quad \operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{G}} \rightarrow \fj{R} \end{array}}
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.m($\overline{e_x}$)} : \fj{C}}
{\begin{array}{c}\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{C0} \quad \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \\[-1.4ex] \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{mtype}(\fj{m},\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}}
& \newtag{\textrm{\textsc{TI-Invk}}}{rule:ti:invoke}
\\[3ex]
\infer
{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{new D(}\overline{\fj{e}}\fj{)} : \fj{D}}
{\mathfrak{T},\mathcal{A},\Gamma \Vdash \overline{\fj{e}} : \overline{\fj{E}} \quad \overline{\fj{E}} \subclass \overline{\fj{G}} \quad \operatorname{constructor}(\fj{D}) = \overline{\fj{G}}}
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{new C(}\overline{e_x}\fj{)} : \fj{C}}
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{constructor}(\fj{C}) = \overline{\fj{D}}}
& \newtag{\textrm{\textsc{TI-New}}}{rule:ti:new}
\\[3ex]
\infer
{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{(D)e} : \fj{D}}
{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{e} : \fj{C} \quad \fj{C} \subclass \fj{D}}
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}}
& \newtag{\textrm{\textsc{TI-DCast}}}{rule:ti:downCast}
\\[3ex]
\infer
{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{(D)e} : \fj{D}}
{\mathfrak{T},\mathcal{A},\Gamma \Vdash \fj{e} : \fj{C} \quad \fj{D} \subclass \fj{C} \quad \fj{C} \neq \fj{D}}
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}}
& \newtag{\textrm{\textsc{TI-UCast}}}{rule:ti:upCast}
\end{tabular}
\end{tcolorbox}
@ -442,40 +453,60 @@
\label{fig:typti}
\end{figure}
Nous allons maintinant vérifier la définition de cette opération de typage $\Vdash$ en démontrant le théorème suivant:
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}
Soit une \eng{test interface} $\mathfrak{T}$, une \eng{class table} $\mathcal{A}$ et un test $(\mathcal{C},e)$ vérifiant
\label{thm:tiTyp}
Soit une \eng{test interface} $\mathfrak{T}$, une \eng{class table} $\mathcal{A}$ et un test $(\mathcal{B},e)$ vérifiant
\begin{itemize}
\item $\mathcal{A} \triangleright \mathfrak{T}$
\item $\mathcal{C} \text{\textsc{ OK in }} \mathfrak{T}$
\item $\mathfrak{T},\mathcal{C} \Vdash e : \fj{D}$
\item $\mathcal{B} \OKin \mathfrak{T}$
\item $\mathfrak{T},\mathcal{B} \Vdash e : \fj{D}$
\end{itemize}
Alors il existe \fj{C} tel que $\mathcal{A} \oplus \mathcal{C} \vdash e : \fj{C}$ et $\fj{C} \subclass \fj{D}$.
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$.
\end{theorem}
Ce théorème se prouve par induction sur la preuve de $\mathfrak{T},\mathcal{C} \Vdash e : \fj{D}$. La preuve est donnée en \autoref{anx:proofTyptyp}.
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 donc définir un préordre sur les \eng{class tables} de la manière suivante.
On peut alors définir un préordre sur les \eng{class tables} de la manière suivante.
\begin{definition}
Soit une \eng{test interface} $\mathfrak{T}$.
Soit deux \eng{class tables} $\mathcal{A}$ et $\mathcal{B}$ qui implémentent toutes deux $\mathfrak{T}$
\[\mathcal{A} \prec \mathcal{B} \ssi \forall (\mathcal{C},e) \left|\begin{array}{l}
\mathcal{C} \text{\textsc{ OK in }} \mathfrak{T}\\
\mathfrak{T},\mathcal{C} \Vdash e : \fj{D}\\
\mathcal{A}\oplus\mathcal{C} \Downarrow v
\end{array}\right. \implies \mathcal{B}\oplus\mathcal{C}\Downarrow v\]
\[\mathcal{A} \prec \mathcal{A'} \ssi \forall (\mathcal{B},e) \left|\begin{array}{l}
\mathcal{B} \OKin \mathfrak{T}\\
\mathfrak{T},\mathcal{B} \Vdash e : \fj{D}\\
\mathcal{A}\oplus\mathcal{B} \Downarrow v
\end{array}\right. \implies \mathcal{A'}\oplus\mathcal{B}\Downarrow v\]
\end{definition}
\subsection{Renforcage 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$
\[(\mathcal{A},e)\prec(\mathcal{B},f) \implies (\mathcal{A},h\bracket{e})\prec(\mathcal{A},h\bracket{f})\]
Cependant, cela est généralement faux, puisque il est possible en Featherweight Java de considérer des expressions qui vont se réduire à l'infini, mais que l'on peut \enquote{utiliser} avec des appels à méthodes ou des attributs. Nous pouvons par exemples utiliser les listes infinies, définies en annexe (\autoref{anx:classes:listes}). Cette classe définie deux attributs, dont un de son propre type.
\begin{figure}
\begin{fjlisting}
\fjclass{Static}{}{
\fjmethod{IList}{intList}{Int i}{new IList(i, intList(i+1))}
\fjmethod{IList}{zeroList}{}{new IList(0, zeroList())}
}
\end{fjlisting}
\label{fig:ilistsDefs}
\caption{Définitions de listes infinies}
\end{figure}
Par exemple, avec la \eng{class table} définie \autoref{fig:ilistsDefs}, nous pouvons considérer les deux expressions $e = \fj{intList(0)}$ et $e' = \fj{zeroList()}$.
\section{Vers des équivalences plus pratiques}
\subsection{Une équivalence entre les expressions}
@ -500,7 +531,7 @@
\begin{fjlisting}
\fjclass{Bool}{}{
\fjmethod{Object}{ite}{Object oTrue, Object oFalse}{oTrue}
}
}\\
\fjclass[Bool]{OBool}{}{
\fjmethod{Object}{ite}{Object oTrue, Object oFalse}{oFalse}
}
@ -513,7 +544,7 @@
\begin{fjlisting}
\fjclass{Int}{}{
\fjmethod{Bool}{isNull}{}{true}
}
}\\
\fjclass{SInt}{\fjattr[Int]{prec}}{
\fjmethod{Bool}{isNull}{}{false}
}
@ -523,7 +554,191 @@
\[\fj{0} = \fj{new Int()}\]
\[n = \fj{new SInt(n-1)}\]
\subsection{Les listes}
\label{anx:classes:listes}
\begin{fjlisting}
// Listes Infinies\\
\fjclass{IList}{\fjattr[IList]{next}\fjattr{obj}}{}\\
// Listes Finies\\
\fjclass{List}{}{
\fjmethod{Bool}{isEmpty}{}{true}
}\\
\fjclass[List]{Cons}{\fjattr[List]{queue}\fjattr{head}}{
\fjmethod{Bool}{isEmpty}{}{false}
}
\end{fjlisting}
On ajoute aussi les notations des listes :
\[\fj{[]} = \fj{new List()}\]
\[\fj{$o$::$e$} = \fj{new Cons($e$,$o$)}\]
\section{Preuve du théorème de cohérence du typage des \eng{test interfaces}}
\label{anx:proofTyptyp}
Cette section a pour but de présenter la preuve complète du \autoref{thm:tiTyp}, sur la cohérence du typage des \eng{test interfaces}.
Nous avons $\mathfrak{T}$ une \eng{test interface}, $\mathcal{C}$ une \eng{class table} telle que $\mathcal{A} \triangleright \mathfrak{T}$ et $(\mathcal{B}, e)$ un programme test, tel que $\mathcal{B}\OKin\mathfrak{T}$.
Nous allons donc essayer de montrer, par induction sur la preuve de la prémisse, la propriété suivante
\[\mathfrak{T},\mathcal{B}, \Gamma \Vdash e : \fj{C} \implies \exists \fj{C'}\quad \mathcal{A}\oplus\mathcal{B},\Gamma \vdash e : \fj{C'} \quad\text{et}\quad \fj{C'} \subclass \fj{C}\]
\subsection{Propriétés sur les fonctions utilitaires}
La définition de $\vdash$ dans Featherweight Java de base utilise les fonctions utilitaires non surchargées. Afin de bien les différencier, nous allons noter avec un prime les versions surchargées définies \autoref{fig:typops}.
Par exemple, $(\operatorname{fields'})$ correspond à la définition surchargée dans la \eng{test interface} $\mathfrak{T}$ et la \eng{class table} de tests $\mathcal{B}$, et $(\operatorname{fields})$ correspond à la définition originale dans la \eng{class table} $\mathcal{A} \oplus \mathcal{B}$. Il en va de même pour l' opérateur $(\subclass')$, qui dénotera la cloture transitive et réflexive de l'union des relations \fj{<:} sur $\mathfrak{T}$ et \fj{extends} dans $\mathcal{B}$ et l'opérateur $(\subclass)$ qui dénotera la relation de sous-typage sur la \eng{class table} $\mathcal{A} \oplus \mathcal{B}$.
Nous allons déjà montrer les trois propriétés suivantes sur ces fonctions utilitaires:
\[
\begin{array}{rcl}
\fj{C}\;\fj{f} \in \operatorname{fields'}(\fj{C0}) &\implies& \exists \fj{C'}\subclass\fj{C}\quad\fj{C'}\;\fj{f} \in \operatorname{fields}(\fj{C0}) \\
\operatorname{mtype'}(\fj{m},\fj{C0}) = \overline{\fj{D}}\rightarrow\fj{C} & \implies& \exists \fj{C'}\subclass \fj{C}\ \exists \overline{\fj{D'}} \superclass \overline{\fj{D}}\quad \operatorname{mtype}(\fj{m},\fj{C0}) = \overline{\fj{D'}}\rightarrow\fj{C'}\\
\operatorname{construct'}(\fj{C0}) = \overline{\fj{D}} & \implies & \exists \overline{\fj{D'}} \superclass \overline{\fj{D}}\quad\exists \overline{\fj{f}} \quad \operatorname{fields}(\fj{C0}) = \overline{\fj{D'}}\;\overline{\fj{f}}
\end{array}
\]
\paragraph{Première propriété}
Montrons cette propriété par induction sur la relation $\subclass'$.
En inversant la règle qui a permis de prouver $\fj{C}\;\fj{f} \in \operatorname{fields'}(\fj{C0})$, il y a quatre possibilités.
\subparagraph{Cas $\fj{C}\;\fj{f} \in \bigcup_{\fj{C}\subclass'\fj{E}}\operatorname{fields'}(\fj{E})$}
On applique alors directement l’hypothèse d'induction.
\subparagraph{Cas $\fj{class C0 \{C f;...\}} \in \mathcal{B}$ (\textnormal{\ref{rule:lct-fields})}}
Alors, par construction de $\operatorname{fields}$, on a $\fj{C}\;\fj{f} \in \operatorname{fields}(C0)$
\subparagraph{Cas $\left[\fj{C0 \{C f, ...\}}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-fields})}}
Alors, puisque $\mathcal{A} \triangleright \mathfrak{T}$, c'est nécessairement par la règle \ref{rule:tri:attributes}, et on a donc
\[\fj{C'} \fj{f} \in \operatorname{fields}_\mathcal{A}(\fj{C0})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\]
\subparagraph{Cas $\left[\fj{C0 (..., C f, ...)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-fields2})}}
Alors, puisque $\mathcal{A} \triangleright \mathfrak{T}$, c'est nécessairement par la règle \ref{rule:tri:constructor}, et on a donc, puisque le field \fj{f} est défini,
\[\fj{C'} \fj{f} \in \operatorname{fields}_\mathcal{A}(\fj{C0})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\]
\paragraph{Seconde propriété}
Procédons un peu de la même manière, par induction sur la définition de $\operatorname{mtype'}$.
Nous avons comme hypotèse $\operatorname{mtype'}(\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{C}$.
\subparagraph{Cas $\left[\fj{C0 : C m($\overline{\texttt{D}}$)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-method})}}
Alors, puisque $\mathcal{A} \triangleright \mathfrak{T}$, c'est nécessairement par la règle \ref{rule:tri:method}, et on a donc.
\[\operatorname{mtype}_\mathcal{A}(\fj{m},\fj{C}) = \overline{\fj{D'}} \rightarrow \fj{C'}\quad;\quad\overline{\fj{D}} \subclass \overline{\fj{D'}}\quad;\quad \fj{C'}\subclass\fj{C}\]
CQFD.
\subparagraph{Cas $\fj{class C0 \{...,C m($\overline{\texttt{D}}\;\overline{\texttt{x}}$)\}}\in \mathcal{B}$ (\textnormal{\ref{rule:lct-method}})}
Alors, par définition de $\operatorname{mtype}$, on a que
\[\operatorname{mtype}_\mathcal{B}(\fj{m},\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{E}\quad\text{et}\quad\fj{C0}\subclass\fj{C0}\]
CQFD.
\subparagraph{Cas $\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}} \rightarrow \fj{E}$ et $\fj{C}\subclass'\fj{C0}$ (\textnormal{\ref{rule:lup-method}})}
\label{proof:mtype:cchain}
Puisque $\fj{C}\subclass'\fj{C0}$, alors, il existe une chaine de classes
\[\fj{C} = \fj{C}_0 , \fj{C}_1 , \dots , \fj{C}_n = \fj{C0}\]
telles que $\fj{C}_k\;\fj{extends}\;\fj{C}_{k+1}$ dans $\mathcal{A}$ ou $\mathcal{B}$.
Or, on sait que les défintions de $\mathcal{A}$ et $\mathcal{B}$ sont $\textsc{OK}$ (c'est imposé par la définition de $\mathcal{A}\triangleright\mathfrak{T})$.
On a donc que pour chacune de ces classes:
\[\operatorname{mtype}(\fj{m},\fj{C}_n) = \operatorname{mtype}(\fj{m},\fj{C}_{n-1}) = \cdots = \operatorname{mtype}(\fj{m},\fj{C}_0)\]
Donc $\operatorname{mtype}(\fj{m},\fj{C0}_n) = \overline{\fj{D}}\rightarrow \fj{E}$. CQFD
\paragraph{Troisième propritété}
Une dernière fois, inversons la règle qui a permis de prouver $\operatorname{construct'}(\fj{C0}) = \overline{\fj{D}}$.
\subparagraph{Cas $\left[\fj{C0 ($\overline{\texttt{D}}\;\overline{\texttt{f}}$)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-construct})}}
Alors, puisque $\mathcal{A} \triangleright \mathfrak{T}$, c'est nécessairement par la règle (\ref{rule:tri:constructor}), et on a donc
\[\exists \overline{\fj{D'}}\quad\overline{\fj{D'}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)\]
CQFD
\subparagraph{Cas $\fj{class C0\{C0($\overline{\texttt{D}}\;\overline{\texttt{f}}$)\{...\} ... \}}\in \mathcal{B}$ (\textnormal{\ref{rule:lct-construct}})}
Alors, puisqu'en Featherweight Java, les objets sont immuables et les constructeurs définissent tous les fields, on sait que les paramètres du constructeurs sont \emph{exactement} les champs de la classe. Et donc
\[\operatorname{fields}(\fj{C0}) = \overline{\fj{D}} \quad\text{et}\quad \overline{\fj{D}} \subclass \overline{\fj{D}}\]
\subsection{Corps de la preuve}
Démarrons l'induction sur la preuve de la propriété présentée au début de la section.
\subparagraph{\textnormal{\textsc{\ref{rule:ti:variable}}}}
\begin{hyps}
\item e = \fj{x}
\item \fj{C} = \Gamma(\fj{x})
\item \fj{x} \in \operatorname{dom}(\Gamma)
\end{hyps}
Alors, d'après la règle FJ \textsc{T-Var}
\[\mathcal{A}\oplus\mathcal{B},\Gamma \vdash \fj{x} : \Gamma(\fj{x})\]
\subparagraph{\textnormal{\textsc{\ref{rule:ti:field}}}}
\begin{hyps}
\item e = \fj{$e_0$.f}
\item \fj{C} = \fj{C}
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash e_0 : \fj{C0} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash e_0 : \fj{C0'}\quad\text{et}\quad \fj{C0'}\subclass\fj{C0}
\item \fj{C}\;\fj{f} \in \operatorname{fields'}(\fj{C0})
\end{hyps}
On peut alors appliquer la première propriété sur la quatrième hypotèse qui nous donne
\[\exists\fj{C'}\subclass \fj{C} \quad \fj{C'}\;\fj{f} \in \operatorname{fields}(\fj{C0})\]
Alors, on peut directement appliquer la règle FJ \textsc{T-Field}
\subparagraph{\textnormal{\textsc{\ref{rule:ti:invoke}}}}
\begin{hyps}
\item e = \fj{$e_0$.m($\overline{e_x}$)}
\item \fj{C} = \fj{C}
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash e_0 : \fj{C0} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash e_0 : \fj{C0'}\quad\text{et}\quad \fj{C0'}\subclass\fj{C0}
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash \overline{e_x} : \overline{\fj{CX'}}\quad\text{et}\quad \overline{\fj{CX'}}\subclass\overline{\fj{CX}}
\item \operatorname{mtype'}(\fj{m},\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{C}
\item \overline{\fj{CX}} \subclass \overline{\fj{C}}
\end{hyps}
On peut alors appliquer la seconde propriété sur la cinquième hypothèse, on obtient que
\[\operatorname{mtype}(\fj{m}, \fj{C0}) = \overline{\fj{D'}} \rightarrow \fj{C'} \quad\text{et}\quad \overline{\fj{D}}\subclass\overline{\fj{D'}}\quad\text{et}\quad\fj{C'}\subclass\fj{C}\]
Alors, en utilisant la même preuve que pendant la preuve de la sous propriété (\autoref{proof:mtype:cchain})
\[\operatorname{mtype}(\fj{m},\fj{C0'}) = \overline{\fj{D'}}\rightarrow\fj{C'} \quad\text{et}\quad \overline{\fj{CX'}} \subclass \overline{\fj{CX}} \subclass \overline{\fj{D}} \subclass \overline{\fj{D'}}\]
On peut maintenant appliquer la règle FJ \textsc{T-Invk} et obtenir le résultat.
\subparagraph{\textnormal{\textsc{\ref{rule:ti:new}}}}
\begin{hyps}
\item e = \fj{new C($\overline{e_x}$)}
\item \fj{C} = \fj{C}
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash \overline{e_x} : \overline{\fj{CX'}}\quad\text{et}\quad \overline{\fj{CX'}}\subclass\overline{\fj{CX}}
\item \operatorname{construct'}(\fj{C}) = \overline{\fj{D}}
\item \overline{\fj{CX}} \subclass \overline{\fj{D}}
\end{hyps}
On peut appliquer la troisième propriété sur la quatrième hypothèse. On obtient alors que :
\[\operatorname{fields}(\fj{C}) = \overline{\fj{D'}}\;\overline{\fj{f}} \quad\text{et}\quad \overline{\fj{CX'}} \subclass \overline{\fj{CX}} \subclass \overline{\fj{D}} \subclass \overline{\fj{D'}}\]
On peut maintenant appliquer la règle FJ \textsc{T-New} et obtenir le résultat.
\subparagraph{\textnormal{\textsc{\ref{rule:ti:upCast}}}}
\begin{hyps}
\item e = \fj{(C)$e_0$}
\item \fj{C} = \fj{C}
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash e_0 : \fj{C} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash e_0 : \fj{D}\quad\text{et}\quad \fj{D}\subclass\fj{C}
\item \fj{D} \subclass \fj{C}
\end{hyps}
On a alors l'inégalité suivante :
\[\fj{D'} \subclass \fj{D} \subclass \fj{C}\]
On peut donc appliquer directement la règle \textsc{T-UCast}
\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}
\end{document}

27
header.tex
View File

@ -27,6 +27,10 @@
\usepackage{biblatex}
\usepackage{xparse}
\usepackage{cprotect}
\usepackage{titlesec}
\usepackage{xpatch}
\usepackage{enumitem}
\usepackage{amsfonts}
\usepackage{csquotes}
\usepackage[lighttt]{lmodern}
@ -86,9 +90,30 @@
\DeclareMathOperator{\new}{\text{\textbf{new}}}
\DeclareMathOperator{\CT}{CT}
\DeclareRobustCommand{\leftsarrow}{\text{\reflectbox{$\;\rightarrow^*$}}}
\newcommand\subclass{<:}
\newcommand\subclass{\mathrel{<:}}
\newcommand\superclass{\mathrel{:>}}
\newcommand\OKin{\text{\textnormal{\textsc{ OK in }}}}
% Création des environnements spécifiques au document
\newcounter{hyp}
\makeatletter
\newif\if@mathitemize
\newif\if@closemathitem
\let\orig@item=\item
\newenvironment{hypenumerate}{\enumerate}{\endenumerate}
\newcommand{\hypitem}{\if@closemathitem$\fi\orig@item\if@mathitemize\@closemathitemtrue$\fi}
\newenvironment{hyps}{\let\item\hypitem \@mathitemizetrue\hypenumerate\@closemathitemfalse}{$\endhypenumerate}
\makeatother
%%% Subparaghaphs box
\newtcbox{\subparaghaphbox}{nobeforeafter,tcbox raise base, arc=9pt, outer arc=9pt, boxsep=2pt,left=2pt,right=2pt,top=2pt,bottom=2pt,boxrule=1pt,colback=white!85!orange}
\newcommand{\subparaghaphboxedcontent}[1]{\subparaghaphbox{#1}\newline}
\titleformat{\subparagraph}[runin]
{\normalfont\normalsize\bfseries}{}{0em}{\subparaghaphboxedcontent}
\titlespacing*{\subparagraph}{0pt}{3.25ex plus 1ex minus .2ex}{0.5em}
%%% Blocs colorés pour le code FeatherweightJava
\newtcbox{\fjmaincodebox}{nobeforeafter,tcbox raise base, arc=0pt, outer arc=0pt, boxsep=0pt,left=2pt,right=2pt,top=2pt,bottom=2pt,boxrule=0pt,colback=white!85!black}