From 2364c0479916f79e21bcbd5c9bf7cccfa5cc9a37 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Thu, 30 Jun 2022 12:43:55 +0200 Subject: [PATCH] =?UTF-8?q?D=C3=A9but=20de=20la=20d=C3=A9finition=20des=20?= =?UTF-8?q?test=20interfacesx.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- NotesStage.tex | 2 +- RapportStage.tex | 163 ++++++++++++++++++++++++++++++++++++++++++++++- header.tex | 8 ++- 3 files changed, 167 insertions(+), 6 deletions(-) diff --git a/NotesStage.tex b/NotesStage.tex index 982e1dc..0a426ba 100644 --- a/NotesStage.tex +++ b/NotesStage.tex @@ -460,7 +460,7 @@ B () - B : B m() + B : A m() \end{fjlisting} & \begin{fjlisting}[width=.2\textwidth] diff --git a/RapportStage.tex b/RapportStage.tex index 1d45f14..59e195c 100644 --- a/RapportStage.tex +++ b/RapportStage.tex @@ -115,6 +115,8 @@ Mais le plus gros problème est de déterminer ce qu'est un contexte. La tâche est d'autant plus difficile en Featherweight Java car un programme n'est pas constitué que d'une expression, comme en λ-calcul ou en π-calcul. Une expression seule n'a même aucun sens sans une \eng{class table} associée. + \subsection{Exemples d'équivalences simples} + \paragraph{Une définition la plus simple} On peut commencer par dire qu'un contexte est simplement une expression à trou $C = h$. L'interpretation d'un programme $P = (\mathcal{A},e)$ dans un contexte $C$ est alors \[C\bracket{P} = (\mathcal{A},h\bracket{e})\] @@ -131,17 +133,172 @@ La relation créée est ainsi robuste, mais inefficace. \paragraph{Une boîte à outils plus puissante} - En essayant de résoudre le premier problème, nous aggravons le second. Afin de permettre aux contextes d'être plus complets, on est d'abord tenté d'y accoler une \eng{class table}. Ainsi, l'application du contexte $C = (\mathcal{C},h)$ au programme donne - \[C\bracket{P} = (\mathcal{A} \oplus CT_P,h\bracket{e_P})\] + Afin de permettre aux contextes d'être plus complets et d'ainsi résoudre le premier problème, on est d'abord tenté d'y accoler une \eng{class table}. Ainsi, l'application du contexte $C = (\mathcal{C},h)$ au programme donne + \[C\bracket{P} = (\mathcal{C} \oplus CT_P,h\bracket{e_P})\] (le $\oplus$ dénote un α-renommage évitant que les définitions s'écrasent les unes les autres) + Hélas, cela renforce le second problème, car il existe alors forcément un trou dégénéré dans une \eng{class table} $\mathcal{C} \oplus CT_P$ (on n'a qu'à rajouter une classe ressemblant à \fj{Paire}). + \paragraph{Restreindre les \eng{class tables}} - \subsection{Définitions et notations globales} + Une dernière définition simple consiste à imposer certaines contraintes sur les \eng{class tables} des programmes comparés. On va d'abord définir le préordre suivant sur les \eng{class tables} : + + \[\mathcal{A} \prec \mathcal{B} \iff \forall e \forall v \quad (\mathcal{A},e)\Downarrow v \implies (\mathcal{B},e)\Downarrow v\] + + Souhaitant garder les contextes les plus puissants possibles, on les définit comme des couples $(\mathcal{C},h)$ et on note alors la contextualisation d'un programme $P = (\mathcal{A},e)$ + \[C\bracket{P} = (\mathcal{C}, h\bracket{e})\qquad \underline{\text{si } \mathcal{A} \prec \mathcal{C}}\] + + Cette condition restreint le nombre de contextes pouvant transformer un programme, et donc transforme le préordre en + \[P \prec Q \iff \forall C\quad + \left|\begin{array}{l}CT_P \prec CT_C\\ CT_Q \prec CT_C \\ + \forall v\quad C\bracket{P}\Downarrow v \implies C\bracket{Q}\Downarrow v\end{array}\right. \] + + Cependant, cette définition pose un problème lorsque l'on cherche à copmarer deux \eng{class tables} qui n'ont aucune \enquote{sur-\eng{class table}} qui convienne aux deux en même temps. C'est le cas des deux classes données \autoref{fig:nosurct} notées $\mathcal{A}$ et $\mathcal{B}$. + + \begin{figure} + \begin{multicols}{2} + \begin{fjlisting} + \fjclass{Get}{ + \fjattr[A]{a} + \fjattr[B]{b} + }{ + \fjmethod{Object}{get}{}{this.a} + } + \end{fjlisting} + \columnbreak + \begin{fjlisting} + \fjclass{Get}{ + \fjattr[A]{a} + \fjattr[B]{b} + }{ + \fjmethod{Object}{get}{}{this.b} + } + \end{fjlisting} + \end{multicols} + \label{fig:nosurct} + \caption{\eng{Class tables} n'ayant pas de sur-\eng{class table} commune} + \end{figure} + + En effet, en notant les expressions suivantes + \[\begin{array}{c} + e_A = \fj{(A)(new Get(new A(), new B()).get())} \\ + e_B = \fj{(B)(new Get(new A(), new B()).get())} + \end{array}\] + + On peut observer les relations suivantes qui montrent que une \eng{class table} qui conviendrait à $\mathcal{A}$ et à $\mathcal{B}$ serait impossible, car elle pourrait et ne pourrait pas évaluer $e_A$ et $e_B$ en une valeur. + \[\begin{array}{cc} + (CL_A,e_A)\Downarrow \new A()& (CL_A,e_B)\nDownarrow \\ + (CL_B,e_A)\nDownarrow & (CL_B,e_B)\Downarrow \new B() + \end{array}\] \section{Des tests plus ciblés} + 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. + + Le terme interface n'est pas anodin, la structure ressemble à une interface Java (ou Featherweigth Java \cite{liquori_fjInterfaces}), mais en plus rigoureuse. Une expression va \enquote{compiler} (c'est à dire être typée) contre l'interface, puis sera \enquote{executée} (c'est à dire réduite) contre des vraies \eng{class tables}. + \subsection{Définition de la structure de \eng{Test Interface}} + + \paragraph{Structure} Nous définissons donc la structure des \eng{test interface rules} dans la \autoref{fig:tigrammaire}. Une teste interface est alors simplement un ensemble de \eng{test interface rules}, et sera noté $\mathfrak{T}$, $\mathfrak{U}$, $\mathfrak{V}$. La règle \autoref{rule:tsg:method} permet de déclarer une méthode dans un classe et de spécifier son type. La \autoref{rule:tsg:attributes} permet de déclarer certains attributs d'une classe, en spécifiant leur nom et leur type. La \autoref{rule:tsg:constructor} permet de déclarer le constructeur de la classe ainsi que les types des attributs, et éventuellement certains noms. Enfin, la \autoref{rule:tsg:cast} permet d'indiquer que une classe doit être un sous-type d'un autre. + + Un exemple concret de \eng{test interface} est donnée \autoref{fig:tiexample}. On y définit des classes \fj{Int}, \fj{Frac}, \fj{Number} et \fj{RichInt} telles que l'on puisse appeler certaines méthodes sur elles. On impose aussi de pouvoir construire les object \fj{Frac} avec deux paramètres de type \fj{Int}, et on impose aussi un attribut nommé \fj{value} dans la classes RichInt. + + \begin{figure} + \ttfamily + \begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue] + \begin{center} + \refstepcounter{rule} + \begin{tabular}{rll} + TR := & C : C m($\overline{\fj{C}}$) & \qquad \newtag{\textrm{\textsc{TSG-Meth}}}{rule:tsg:method} \\ + | & C \{$\overline{\fj{C}}$ $\overline{\fj{f}}$\} & \qquad \newtag{\textrm{\textsc{TSG-Attr}}}{rule:tsg:attributes} \\ + | & C ($\overline{\fj{C}}$ $\overline{\fj{(?|f)}}$) & \qquad \newtag{\textrm{\textsc{TSG-Cstr}}}{rule:tsg:constructor} \\ + | & C :> C & \qquad \newtag{\textrm{\textsc{TSG-Cast}}}{rule:tsg:cast} + \end{tabular} + \end{center} + \end{tcolorbox} + \rmfamily + \caption{Grammaire des \eng{test interface rules}} + \label{fig:tigrammaire} + \end{figure} + + \begin{figure} + \begin{fjlisting} + Int \{\}\\ + Int : Int suivant(Int)\\ + Int : Int add(Int,Int)\medskip + + Frac(Int numerateur, Int denominateur)\\ + Frac : Frac inverted()\\ + Frac : Int floor()\medskip + + Number \{\}\\ + Frac <: Number\\ + Int <: Number\medskip + + RichInt \{Int value\}\\ + RichInt : Int getInt()\\ + RichInt <: Int + \end{fjlisting} + \caption{Exemple de \eng{test interface}} + \label{fig:tiexample} + \end{figure} + + À cette grammaire, nous allons ajouter quelques règles afin que la \eng{test interface} soit considérée comme valide. Dans la suite du document, on considèrera que toutes les \eng{test interfaces} utilisées sont toujours valides. Ces règles sont les suivantes: + + \begin{itemize} + \item Chaque nom de classe est défini au plus une fois par une \autoref{rule:tsg:attributes} ou une \autoref{rule:tsg:constructor}. + \item Chaque nom de methode est défini au plus une fois par nom de classe par une \autoref{rule:tsg:method}. + \item Les noms de classe utilisés sont définis (sauf éventuellement Object). + \end{itemize} + + Les deux règles \ref{rule:tsg:attributes} et \ref{rule:tsg:constructor} sont mutuellement exclusives pour un nom de classe donnée. La différence est que la seconde autorise l'appel au constructeur (l'expression \fj{new C(...)}) et imposant un ordre sur les paramètres là ou la seconde n'autorise pas le constructeur, et n'impose donc pas d'ordre sur les attributs. + + 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 \{\}} + + \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$ + + \begin{figure} + \ttfamily + \begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue] + \refstepcounter{rule} + \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}} + &\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)} + &\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) + } + &\newtag{\textrm{\textsc{(TRI-Cstr)}}}{rule:tri:constructor}\\[1em] + + \infer + {\mathcal{A} \triangleright \left[\fj{C} \subclass \fj{D}\right]} + {\fj{C} \subclass_\mathcal{A} \fj{D}} + &\newtag{\textrm{\textsc{(TRI-Cast)}}}{rule:tri:cast} + \end{tabular} + \end{center} + \end{tcolorbox} + \rmfamily + \caption{Définition de l'implémentation des \eng{test interfaces rule}} + \label{fig:tiDefImpl} + \end{figure} \subsection{Définition du typage et d'un premier préordre} diff --git a/header.tex b/header.tex index bec7f85..302fbd6 100644 --- a/header.tex +++ b/header.tex @@ -43,10 +43,11 @@ \newcommand{\bigO}{\mathcal{O}} \newcommand{\longdash}{\:\textrm{---}\:} \newcommand\hole{\left[\raisebox{-0.25ex}{\scalebox{1.2}{$\cdot$}}\right]} -\newcommand\bracket[1]{\left[#1\right]} +\newcommand\bracket[1]{\!\left[#1\right]} \newcommand{\ssi}{\quad\text{\underline{ssi}}\quad} \newcommand\eng[1]{\textit{\foreignlanguage{english}{#1}}} \newcommand\spacebar{\;|\;} +\def\nDownarrow{\not\mspace{1mu}\Downarrow} \DeclareUnicodeCharacter{03BB}{$\lambda$} \DeclareUnicodeCharacter{03B1}{$\alpha$} @@ -56,8 +57,11 @@ \newtheorem{theorem}{Théorème} \newtheorem{definition}{Definition} \newtheorem{property}{Propriété} + +\newcounter{rule} \addto\extrasfrench{% - \renewcommand{\figureautorefname}{\textsc{Figure}}% + \renewcommand{\figureautorefname}{\textsc{Figure}} + \providecommand\ruleautorefname{règle} } % Commandes logiques globales