Avancement du rapport, jeudi.
This commit is contained in:
parent
2364c04799
commit
f0ae7ca42f
GPG Key ID:
7054D5D6A90F084F
155
RapportStage.tex
155
RapportStage.tex
@ -258,11 +258,46 @@
|
||||
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}\]
|
||||
|
||||
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 \{\}}
|
||||
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}
|
||||
|
||||
\begin{figure}
|
||||
\begin{center}
|
||||
\begin{tabular}{ccc}
|
||||
\begin{fjlisting}[width=.3\textwidth]
|
||||
\begin{multicols}{2}
|
||||
A \{\}\\
|
||||
B \{\}\\
|
||||
C \{\}\\
|
||||
A <: B\\
|
||||
B <: C\\
|
||||
C <: A
|
||||
\end{multicols}
|
||||
\end{fjlisting}
|
||||
&
|
||||
\begin{fjlisting}[width=.2\textwidth]
|
||||
A \{\}\\
|
||||
B \{A f\}\\
|
||||
C ()\\
|
||||
C <: B
|
||||
\end{fjlisting}
|
||||
&
|
||||
\begin{fjlisting}[width=.3\textwidth]
|
||||
A \{\}\\
|
||||
B \{A f\}\\
|
||||
C (A f1, A f2)\\
|
||||
C <: B
|
||||
\end{fjlisting}
|
||||
\end{tabular}
|
||||
\end{center}
|
||||
\label{fig:tiUnsolvable}
|
||||
\caption{Exemples de \textit{test interfaces} implémentés par aucune \textit{class table}}
|
||||
\end{figure}
|
||||
|
||||
\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$.
|
||||
|
||||
\begin{figure}
|
||||
\ttfamily
|
||||
@ -271,20 +306,28 @@
|
||||
\begin{center}
|
||||
\begin{tabular}{cr}
|
||||
\infer
|
||||
{\mathcal{A} \triangleright \left[\fj{C : D m($\overline{\texttt{E}}$)}\right]}
|
||||
{\operatorname{mtype}_\mathcal{A}(\fj{m},\fj{C}) = \fj{$\overline{\texttt{E}}$} \rightarrow \fj{D}}
|
||||
{\mathcal{A} \triangleright \left[\fj{C : G m($\overline{\texttt{F}}$)}\right]}
|
||||
{
|
||||
\operatorname{mtype}_\mathcal{A}(\fj{m},\fj{C}) = \fj{$\overline{\texttt{E}}$} \rightarrow \fj{H}
|
||||
\quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}}
|
||||
\quad \fj{H}\subclass_\mathcal{A}\fj{G}
|
||||
}
|
||||
&\newtag{\textrm{\textsc{(TRI-Meth)}}}{rule:tri:method}\\[1em]
|
||||
|
||||
\infer
|
||||
{\mathcal{A} \triangleright \left[\fj{ C \{ $\overline{\texttt{E}}\;\overline{\texttt{f}}$\}}\right]}
|
||||
{\overline{\fj{E}}\;\overline{\fj{f}} \subset \operatorname{fields}_\mathcal{A}(C)}
|
||||
{
|
||||
\overline{\fj{F}}\;\overline{\fj{f}} \subset \operatorname{fields}_\mathcal{A}(C)
|
||||
\quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}}
|
||||
}
|
||||
&\newtag{\textrm{\textsc{(TRI-Attr)}}}{rule:tri:attributes}\\[1em]
|
||||
|
||||
\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
|
||||
\overline{\fj{E}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)
|
||||
\overline{\fj{F}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)
|
||||
\quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}}
|
||||
}
|
||||
&\newtag{\textrm{\textsc{(TRI-Cstr)}}}{rule:tri:constructor}\\[1em]
|
||||
|
||||
@ -300,7 +343,105 @@
|
||||
\label{fig:tiDefImpl}
|
||||
\end{figure}
|
||||
|
||||
L'implémentation a été choisie la plus large possible, par exemple, une méthode \fj{C.m} typée par $\fj{Object} \rightarrow \fj{Number}$ implémentera une règle $\left[\fj{C : Int m(A)}\right]$. En effet, cette construction n'a pas pour objectif d'étudier le \emph{typage} de Featherweight Java, mais bien son \emph{fonctionnement}.
|
||||
|
||||
\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$.
|
||||
|
||||
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}.
|
||||
|
||||
|
||||
\begin{figure}
|
||||
\ttfamily
|
||||
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
|
||||
\begin{center}
|
||||
\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}}
|
||||
& \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}}
|
||||
& \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})}
|
||||
{\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})}
|
||||
{\left[\fj{ C ( $\overline{\texttt{D}}\;\overline{\texttt{f}}$)}\right] \in \mathfrak{T}}
|
||||
& \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}}
|
||||
& \newtag{\textrm{\textsc{LCt-Attr}}}{rule:lct-fields}\\[1em]
|
||||
\infer
|
||||
{\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}}
|
||||
{\left[\fj{ C : E m( $\overline{\texttt{D}}$)}\right] \in \mathfrak{T}}
|
||||
& \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}}
|
||||
& \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}}
|
||||
& \newtag{\textrm{\textsc{LUp-Meth}}}{rule:lup-method}
|
||||
\end{tabular}
|
||||
\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}$.
|
||||
|
||||
\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.
|
||||
|
||||
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.
|
||||
|
||||
\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})}
|
||||
{\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})}
|
||||
& \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}}
|
||||
& \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}}}
|
||||
& \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}}
|
||||
& \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}}
|
||||
& \newtag{\textrm{\textsc{TI-UCast}}}{rule:ti:upCast}
|
||||
\end{tabular}
|
||||
\end{tcolorbox}
|
||||
\caption{Typage des expressions avec une \eng{test interface} et une \eng{class table}}
|
||||
\label{fig:typti}
|
||||
\end{figure}
|
||||
|
||||
|
||||
\subsection{Renforcage de ce préordre avec les valeurs infinies}
|
||||
|
||||
@ -315,7 +456,7 @@
|
||||
\section{Conclusion}
|
||||
|
||||
|
||||
\newpage
|
||||
\clearpage
|
||||
\section{Bibliographie}
|
||||
\printbibliography
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user