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

Notes jusqu'au 15 juin

Browse Source
This commit is contained in:
Mysaa 2022-06-16 15:28:24 +02:00
parent 16f5177fba
commit 735f2d52b6
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
2 changed files with 306 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.gitignore vendored
View File

@ -2,3 +2,6 @@
*.log
NotesStage.pdf
*.toc
*.synctex.gz
*.bbl
*.blg

352
NotesStage.tex
View File

@ -12,6 +12,8 @@
\usepackage{algorithm2e}
\usepackage{svg}
\usepackage{tikz}
\usepackage{multirow}
\usepackage{multicol}
\usepackage{tcolorbox}
\usepackage{mdframed}
\usepackage{proof}
@ -26,6 +28,13 @@
\newcommand{\littleO}{o}
\newcommand{\bigO}{\mathcal{O}}
\newcommand{\longdash}{\:\textrm{---}\:}
\newcommand{\methprec}[1]{\prec\mkern-8mu\left[\fj{#1}\right]}
\makeatletter
\newcommand\newtag[2]{#1\def\@currentlabel{#1}\label{#2}}
\makeatother
\DeclareMathOperator{\new}{\text{\textbf{new}}}
\DeclareMathOperator{\CT}{CT}
@ -35,20 +44,20 @@
\newcommand{\ssi}{\quad\text{\underline{ssi}}\quad}
\newtheorem{theorem}{Theorem}
\newtheorem{theorem}{Théorème}
\newtheorem{definition}{Definition}
\tcbuselibrary{fitting}
\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}
\newtcolorbox{fjcodebox}{left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!96!black}
\newenvironment{fjlisting}
\newenvironment{fjlisting}[1][]
{
%\begin{center}
\fjcodebox
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!96!black,#1]
\ttfamily
}{
\endfjcodebox
\end{tcolorbox}
%\end{center}
}
\newcommand{\ifnullthenelse}[3]{
@ -147,7 +156,7 @@
Un programme Featherweight Java est composé de deux parties: La première est une liste de définitons de classes, que le papier originel appelait \textit{collection of class definitions}, mais que nous appellerons plutôt \textit{Class Tables} \cite{yingfei_2014}. La seconde est une expression à évaluer (on peut la voir comme le body d'une fonction \fj{main} d'un programmme Java). Nous allons donc considérer qu'un programme FeatherweightJava $P$ est un couple $(\bar{L},e)$, et l'on notera $\CT(P) = \bar{L}$ et $e_P = e$ lorsque nous manipulerons plusieurs programmes.
On note la gramaire à un trou $h$ :
$$h := x | [.] | h.f | h.m(\bar{e}) | e.m(\bar{e},h,\bar{e}) | \new C(\bar{e},h,\bar{e}) | (C) h $$
$$h := \fj{x} | \fj{[.]} | \fj{h.f} | \fj{h.m(}\bar{\fj{e}}\fj{)} | \fj{e.m(}\bar{\fj{e}}\fj{,h,}\bar{\fj{e}}\fj{)} | \fj{new C(}\bar{\fj{e}}\fj{,h,}\bar{\fj{e}}) | \fj{(C) h} $$
On pourra souvent se ramener à la grammaire à plusieurs trous $\tilde{h}$ :
$$\tilde{h} := x | [.] | \tilde{h}.f | \tilde{h}.m(\bar{\tilde{h}}) | \new C(\bar{\tilde{h}}) | (C) h | e $$
@ -462,32 +471,23 @@
\subsection{Définition des structures}
Nous allons tout d'abord définir une grammaire des \textit{Test sets} ou «jeux de tests» à la \textsc{Figure \ref{ts:grammaire}}. Un exemple de tests est donné à la \textsc{Figure \ref{ts:examples}} où l'on définit des classes \fj{Int}, \fj{Frac}, \fj{Number} et \fj{RichInt} tel qu'on puisse appeler certaines méthodes sur elles. On impose aussi de pouvoir construire les object \fj{Frac} avec deux paramètres, et on impose aussi un attribut nommé \fj{value} dans la classes RichInt.
Afin de valider un tests set, il faut simplement que :
\begin{itemize}
\item Chaque nom de classe n'est défini que une fois par une règle de type 2 ou 3.
\item Chaque nom de methode n'est défini que une fois par nom de classe par une règle de type 1.
\item Les noms de classes utilisés sont définis.
\item La relation obtenue par cloture réflexive et transitive des règles de type 4 est antisymétrique
\end{itemize}
Nous allons tout d'abord définir une grammaire des \textit{Test sets} ou «jeux de tests» à la \textsc{Figure \ref{ti:grammaire}}. Un exemple de tests est donné à la \textsc{Figure \ref{ti:examples}} où l'on définit des classes \fj{Int}, \fj{Frac}, \fj{Number} et \fj{RichInt} tel qu'on puisse appeler certaines méthodes sur elles. On impose aussi de pouvoir construire les object \fj{Frac} avec deux paramètres, 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}
\begin{tabular}{rl}
TS := & C : C m(bar{C}) \\
| & C \{bar{C} bar{f}\} \\
| & C (bar{C (? | f)}) \\
| & C :> C
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{rll}
TI := & C : C m(bar{C}) & \qquad \newtag{\textrm{\textsc{TSG-Meth}}}{tsg:method} \\
| & C \{bar{C} bar{f}\} & \qquad \newtag{\textrm{\textsc{TSG-Attr}}}{tsg:attributes} \\
| & C (bar{C (? | f)}) & \qquad \newtag{\textrm{\textsc{TSG-Cstr}}}{tsg:constructor} \\
| & C :> C & \qquad \newtag{\textrm{\textsc{TSG-Cast}}}{tsg:cast}
\end{tabular}
\end{center}
\end{tcolorbox}
\rmfamily
\caption{Grammaire des test sets}
\label{ts:grammaire}
\label{ti:grammaire}
\end{figure}
\begin{figure}
@ -524,33 +524,287 @@
\end{fjlisting}
\caption{Exemple de set de tests}
\label{ts:examples}
\label{ti:examples}
\end{figure}
Afin de valider un tests set, il faut simplement que :
\begin{itemize}
\item Chaque nom de classe n'est défini que une fois par une règle de type \ref{tsg:attributes} et \ref{tsg:constructor}.
\item Chaque nom de methode n'est défini que une fois par nom de classe par une règle de type \ref{tsg:method}.
\item Les noms de classes utilisés sont définis.
\end{itemize}
On pourrait se questionner sur la structure donnée aux règles \ref{tsg:attributes} et \ref{tsg:constructor}. La différence fondamentale entre les deux est que la première n'autorise pas à appeler \fj{new C(...)} alors que la seconde l'autorise. La première autorise seulement l'accès aux champs de la classe. On pourrait alors critiquer que cette façon de définir les règles ne permet pas d'autoriser la création d'un objet avec \fj{new} et d'autoriser certains \textit{field access} sans en imposer l'ordre. Pourtant, autoriser ces deux constructions impose que deux \textit{class tables} qui seraient équivalentes auraient le champ à la même position. Par exemple, on peut construire une expression simple \fj{new C(new P1(), new P2(), new P3(), ...).field} où \fj{P1}, \fj{P2}, \fj{P3} sont des classes créées pour l'occasion, qui ont des paramètes cohérents, etc… Alors cette expression se réduira en la même valeur dans deux \textit{class table} si et seulement si l'attribut \fj{field} est assigné au même indice dans le constructeur de \fj{C} dans les deux class tables.
La troisième règle permet d'éviter des définitions «implicites» de classes, en suivant la convention suivie par la première définition du Featherweight Java \cite{fjdef}. On peut sinon ajouter la règle \fj{A\{\}} pour chaque nom de classe utilisé sans être défini.
Nous allons aussi rajouter trois règles, qui ne sont pas strictement nécessaires, mais qui permettent de restreindre les tests sets aux tests sets «intéréssants», en enlevant certaines contraintes qui feraient apparaître des méthodes ou objets inutilisables.
\begin{itemize}
\item La relation obtenue par cloture réflexive et transitive des règles de type \ref{tsg:cast} est un bon ordre (en ajoutant la classe virtuelle \fj{Object})
\item Dans les ocurrences des règles \ref{tsg:attributes} et \ref{tsg:constructor}, la relation «est le type d'un attribut» induit un bon ordre.
\item Pour chaque règle \ref{tsg:cast} \fj{C :> B}, alors, la propriété adéquate est vérifiée, suivant les règles qui ont défini \fj{C} et \fj{B} selon le tableau suivant:
\vspace{1ex}
\begin{tabular}{c|c|c|}
& \fj{B\{}$\overline{\fj{G}}$ $\overline{\fj{g}}$\fj{\}} & \fj{B(}$\overline{\fj{G}}$ $\overline{\texttt{?}\fj{g}}$\fj{)}\\\hline
\fj{C\{}$\overline{\fj{F}}$ $\overline{\fj{f}}$\fj{\}} & \multirow{2}{*}{$\fj{f}_i = \fj{g}_j \implies \fj{F}_i = \fj{G}_j$} & $\exists \overline{\texttt{?}\fj{f'}}\;\exists \overline{\texttt{?}\fj{g'}}$\\
\fj{C(}$\overline{\fj{F}}$ $\overline{\texttt{?}\fj{f}}$\fj{)} & & $\{\overline{\fj{F}} \; \overline{\left(\texttt{?}\fj{f} \oplus \texttt{?}\fj{f'}\right)}\} \subset \{\overline{\fj{G}} \; \overline{\left(\texttt{?}\fj{g} \oplus \texttt{?}\fj{g'}\right)}\}$
\end{tabular}
\end{itemize}
La première règle semble cohérente, on peut imaginer simplement deux règles \fj{A <: B} et \fj{B <: A} qui n'auraient pas de sens ensemble.
La troisième règle force les contraintes sur les types et noms des attributs à être cohérentes.
On aimerai dire qu'il existe toujours au moins une \textit{class table} qui implémente une \textit{test interface} qui respecte toutes ces règles, mais hélas, ce n'est pas vrai, si l'on considère de manière naïve la relation «est le type d'un attribut» induit par la règle 2, voir troisième exemple de la \textsc{Figure \ref{ti:examplesfaux}}
Cependant, on peut toujours (si la première et la troisième règle sont vérifiées) créer une class table bidon qui ne compile jamais. Pour cela, il suffit d'implémenter naïvement chaque class, sauf que nous remplaçons chaque occurence de \fj{extends Object} par \fj{extends SObject} (où \fj{SObject} est un nom de classe inutilisé). On crée la classe SObject avec un constructeur ne prenant pas de paramètre. Alors, on peut implémenter n'importe quelle méthode du type $\overline{\fj{M}} \rightarrow \fj{T}$ par l'expression \fj{(T) new SObject()}. L'expression est bien typable en \fj{T} puisque SObject est une superclasse de tous les types (sauf Object, auquel cas renvoyer simplement \fj{new SObject()}). Mais bien sûr, ces méthodes ne pourrons jamais renvoyer une valeur car le cast sera toujours impossible.
\begin{figure}
\begin{center}
\begin{tabular}{ccc}
\begin{fjlisting}[width=.2\textwidth]
A \{\}
B ()
C (A)
C :> B
\end{fjlisting}
&
\begin{fjlisting}[width=.2\textwidth]
A (A obj)
B ()
B : B m()
\end{fjlisting}
&
\begin{fjlisting}[width=.2\textwidth]
B \{obj\}
C \{B obj\}
C <: B
C : B m()
\end{fjlisting}
\end{tabular}
\end{center}
\label{ti:examplesfaux}
\caption{Exemples de \textit{test sets} implémentés par aucune \textit{class table} sans cast}
\end{figure}
Maintenant que nous avons notre grammaire, on peut définir plusieurs choses avec elles. Déjà, on va faire une relation $CT \triangleright TI$ pour dire que la class table $CT$ implémente la test interface $TI$, présentée à la \textsc{Figure \ref{ti:defImpl}}. L'implémentation est la plus tolérante possible quant au typage notamment des méthodes, car on ne veut pas comparer les \textit{class tables} sur leur typage, mais bien sur leur fonctionnement, le typage reste un garde-fou qui nous empêche de tester tout et n'importe quoi et d'obtenir une relation inexploitable. Typiquement, les deux \textit{class tables} présentées \textsc{Figure \ref{ti:exempletolerance}} implémenteront toutes deux la test interface jointe, et seront donc équivalentes.
\begin{figure}
\ttfamily
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
\begin{align}
\infer{CT \triangleright \left[\fj{C : D m($\overline{\texttt{E}}$)}\right]}{\operatorname{mtype}_{CT}(\fj{m},\fj{C}) = \fj{$\overline{\texttt{E}}$} \rightarrow \fj{D}}
\end{align}
\begin{align}
\infer{CT \triangleright \left[\fj{ C \{ $\overline{\texttt{E}}\;\overline{\texttt{f}}$\}}\right]}{\bar{\fj{E}}\;\bar{\fj{f}} \subset \operatorname{fields}_{CT}(C)}
\end{align}
\begin{align}
\infer{CT \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]}{\exists \bar{\fj{f'}}\; \bar{\fj{f0}} = \bar{\fj{f}}+\bar{\fj{f'}} \land \bar{\fj{E}}\;\bar{\fj{f0}} = \operatorname{fields}_{CT}(C)}
\end{align}
\begin{align}
\infer{CT \triangleright \left[\fj{C} \subclass \fj{D}\right]}{\fj{C} \subclass_{CT} \fj{D}}
\end{align}
\end{tcolorbox}
\rmfamily
\caption{Grammaire des test sets}
\label{ti:defImpl}
\end{figure}
Maintenant que nous avons notre grammaire, on peut définir plusieurs choses avec elles. Déjà, on va faire une relation $CT \triangleright TS$ pour dire que la class table $CT$ implémente le test set $TS$, présentée à la \textsc{Figure \ref{ts:defImpl}}
\begin{figure}
\begin{center}
\begin{fjlisting}[width=.32\textwidth]
A \{\}
B \{\}
Static ()
Static : A get()
\end{fjlisting}
\begin{multicols}{2}
\begin{fjlisting}[width=.48\textwidth]
\fjclass{A}{}{}
\fjclass[A]{B}{}{}
\fjclass{Static}{}{
\method{A}{get}{}{new B();}
}
\end{fjlisting}
\columnbreak
\begin{fjlisting}[width=.48\textwidth]
\fjclass{A}{}{}
\fjclass[A]{B}{}{}
\fjclass{Static}{}{
\method{B}{get}{}{new B();}
}
\end{fjlisting}
\end{multicols}
\end{center}
\label{ti:exempletolerance}
\caption{Exemple de classes justifiant la tolérance dans la définition de $\triangleright$}
\end{figure}
\begin{figure}
\ttfamily
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
\begin{align}
\infer{CT \triangleright \left[\fj{C : D m($\overline{\texttt{E}}$)}\right]}{\operatorname{mtype}_{CT}(\fj{m},\fj{C}) = \fj{$\overline{\texttt{E}}$} \rightarrow \fj{D}}
\end{align}
\begin{align}
\infer{CT \triangleright \left[\fj{ C \{ $\overline{\texttt{E}}\;\overline{\texttt{f}}$\}}\right]}{\bar{\fj{E}}\;\bar{\fj{f}} \subset \operatorname{fields}_{CT}(C)}
\end{align}
\begin{align}
\infer{CT \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]}{\exists \bar{\fj{f'}}\; \bar{\fj{f0}} = \bar{\fj{f}}+\bar{\fj{f'}} \land \bar{\fj{E}}\;\bar{\fj{f0}} = \operatorname{fields}_{CT}(C)}
\end{align}
\begin{align}
\infer{CT \triangleright \left[\fj{C} \subclass \fj{D}\right]}{\fj{C} \subclass_{CT} \fj{D}}
\end{align}
\end{tcolorbox}
\rmfamily
\caption{Grammaire des test sets}
\label{ts:defImpl}
\end{figure}
Nous allons donc maintenant essayer de typer une expression et une class table sous un test set, dire que une expression $e$ avec sa class table associée $CT$ est «valide» dans un test set $TS$ associé, que l'on note $TS,CT \Rightarrow (\emptyset) \vdash e : T $
Nous allons donc maintenant essayer de typer une expression et une class table sous une test interface, dire que une expression $e$ avec sa class table associée $CT$ est «valide» dans un test interface $TI$ associé, que l'on note $TI,CT \Vdash e : T$ (pour bien différencier de la règle de typage de Featherweight Java, notée $\vdash$).
La présence d'une \textit{class table} associée à l'expression est nécessaire car il existe deux \textit{class tables} implémentant la même \textit{test interfaces} qui ne sont pas différenciables par des expressions seules, mais qui le sont lorsque l'on ajoute un class table (voir exemple \textsc{Figure \ref{ti:exempleneedct}}).
\begin{figure}
\begin{fjlisting}[width=.3\textwidth]
B ()
Static ()
Static : B get(B)
\end{fjlisting}
\begin{fjlisting}[width=.48\textwidth]
\fjclass{B}{}{}
\fjclass{Static}{}{
\method{B}{get}{B in}{in}
}
\end{fjlisting}
\begin{fjlisting}[width=.48\textwidth]
\fjclass{B}{}{}
\fjclass{Static}{}{
\method{B}{get}{B in}{new B()}
}
\end{fjlisting}
\begin{fjlisting}[width=.42\textwidth]
\fjclass[B]{A}{}{}
\fjmain{new State().get(new A())}
\end{fjlisting}
\label{ti:exempleneedct}
\caption{Exemple de class tables différentiables uniquement avec une class table}
\end{figure}
Les règles de typage sont obtenues en modifiant quelque peu les règles de typage de Featherweight java. La première étape est de définir les deux applications \textit{mtype} à partir des règles de type 1 et des déclarations de méthodes, et \textit{fields} qui s'obtient à partir des règles deux et trois et des champs présents dans la \textit{class table}. On rajoute enfin une application $\operatorname{construct(C)}$ qui est défini avec deux règles, l'une à partir de la règle trois et l'autre à partir des constructeurs réels (voir \textsc{Figure \ref{ti:defconstruct}}).
\begin{figure}
\ttfamily
\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
\begin{align}
\infer{\operatorname{construct(C)} = \overline{\fj{D}}}{\fj{C(}\overline{\fj{D}}\;\overline{\fj{f}}\fj{)\{...\}}\in CT}
\end{align}
\begin{align}
\infer{\operatorname{construct(C)} = \overline{\fj{D}}}{\fj{C(}\overline{\fj{D}}\;\overline{\texttt{?}\fj{f}}\fj{)} \in TI}
\end{align}
\end{tcolorbox}
\rmfamily
\caption{Application $\operatorname{construct(C)}$}
\label{ti:defconstruct}
\end{figure}
Nous pouvons alors définir la relation de typage d'une expression sous une \textit{class table} et une \textit{test interface} avec des règles d'inférence présentées \textsc{Figure \ref{ti:deftyp}}. On ajoute aussi toutes les règles de typage d'expression présentées dans la définition du FJ Java \cite[p. 404]{fjdef}, en enlevant la règle \textsc{T-SCast} qui n'ajoute pas grand chose ...
\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}{cr}
\infer{TI,CT,\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}{\fj{x} \in \Gamma}
& \textsc{TI-Var}
\\[3ex]
\infer{TI,CT,\Gamma \Vdash \fj{e.f} : \fj{E}}{TI,CT,\Gamma \Vdash e : \fj{C} \quad \fj{C} \subclass \fj{D} \quad \left[\fj{D(...,E f,...)}\right] \in TI}
& \textsc{TI-Field}
\\[3ex]
\infer{TI,CT,\Gamma \Vdash \fj{e.m(}\overline{\fj{e'}}\fj{)} : \fj{R}}{\begin{array}{c}TI,CT,\Gamma \Vdash \fj{e} : \fj{C} \quad TI,CT,\Gamma \Vdash \overline{\fj{e'}} : \overline{\fj{E}} \\[-1.4ex] \fj{C} \subclass \fj{D} \quad \overline{\fj{E}} \subclass \overline{\fj{G}} \quad \left[\fj{D : R m(}\overline{\fj{G}}\fj{)}\right] \in TI\end{array}}
&
\textsc{TI-Invk}
\\[3ex]
\infer{TI,CT,\Gamma \Vdash \fj{new D(}\overline{\fj{e}}\fj{)} : \fj{D}}{TI,CT,\Gamma \Vdash \overline{\fj{e}} : \overline{\fj{E}} \quad \overline{\fj{E}} \subclass \overline{\fj{G}} \quad \left[\fj{D(}\overline{\fj{G}}\fj{)}\right] \in TI}
&
\textsc{TI-New}
\\[3ex]
\infer{TI,CT,\Gamma \Vdash \fj{(D)e} : \fj{D}}{TI,CT,\Gamma \Vdash \fj{e} : \fj{C} \quad \fj{C} \subclass_{TI} \fj{D}}
&
\textsc{TI-DCast}
\\[3ex]
\infer{TI,CT,\Gamma \Vdash \fj{(D)e} : \fj{D}}{TI,CT,\Gamma \Vdash \fj{e} : \fj{C} \quad \fj{D} \subclass_{TI} \fj{C} \quad \fj{C} \neq \fj{D}}
&
\textsc{TI-UCast}
\end{tabular}
\end{tcolorbox}
\caption{Typage des expressions avec un test set et une class table}
\label{ti:deftyp}
\end{figure}
\paragraph{Le théorème de validité du typage} que nous allons essayer de prouver s'énonce ainsi: Soit une \textit{test interface} $TI$, une \textit{class table} $CT$ et un test $(CT_t,e)$ vérifiant
\begin{itemize}
\item $CT \triangleright TI$
\item $CT_t \text{\textsc{ OK in }} TI$
\item $TS,CT_t \Vdash e : \fj{D}$
\end{itemize}
Alors il existe \fj{C} tel que $CT \oplus CT_t \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$, comme est démontré par l'exemple \textsc{Figure \ref{ti:exempletolth}}.
\begin{figure}
\begin{fjlisting}
E \{\}
D ()
D : E m()
\end{fjlisting}
\begin{fjlisting}
\fjclass{E}{}{}
\fjclass[E]{F}{}{}
\fjclass{F}{}{\method{F}{m}{}{new F()}}
\end{fjlisting}
$$e = \fj{new D().m()}$$
$$TI \Vdash e : \fj{E} \qquad CT \vdash e:\fj{F} \qquad CT \triangleright TS$$
\label{ti:exempletolth}
\caption{Exemple de la nécessité de la seconde clause du théorème}
\end{figure}
\section{Équivalence de méthodes}
\begin{definition}
\slshape
Deux méthodes de même nom \fj{Class.method} dans deux \textit{class tables} sont en préordre lorsque pour toute valeur $V$, valeurs $\overline{v}$ et valeurs $\overline{p}$ :
\begin{gather*}
(CT_1,e) \Downarrow V \implies (CT_2,e) \Downarrow V \\
\text{avec } e=\fj{new Class($p_1$,$p_2$,...,$p_n$).method($v_1$,$v_2$,...,$v_m$)}
\end{gather*}
On note alors $CT_1 \methprec{Class.method} CT_2$
\end{definition}
Alors, nous souhaiterions prouver le théorème suivant:
\begin{theorem}
\slshape
Soient deux \textit{class tables} $CT_1$ et $CT_2$ et une \textit{test interface} $TI$,
$$CT_1 \prec_{TS} CT_2 \iff \forall \left[\fj{Class : D meth(}\overline{\fj{E}}\fj{)}\right] \in TI \quad CT_1 \methprec{Class.meth} CT_2$$
\end{theorem}
\newpage
\bibliography{NotesStage}