diff --git a/DiaposSoutenance.tex b/DiaposSoutenance.tex index 3a775b1..8783974 100644 --- a/DiaposSoutenance.tex +++ b/DiaposSoutenance.tex @@ -24,9 +24,9 @@ \usepackage{xparse} \usepackage{cprotect} \usepackage{xpatch} -\usepackage{enumitem} \usepackage{amsfonts} \usepackage{mathtools} +\usepackage{setspace} \usepackage{geometry} \usepackage{subcaption} @@ -198,6 +198,8 @@ \renewcommand*\beamer@checkframetitle{\global\let\beamer@frametitle\relax\@ifnextchar\bgroup\beamer@inlineframetitle{}} \makeatother +\setbeamertemplate{itemizeitem}{\scriptsize$\diamond$} + \author{Samy Avrillon} \title{Définition d'un préordre sur les programmes Featherweight Java} \subtitle{Notes sur mon stage au LACL} @@ -227,20 +229,25 @@ \begin{center} \refstepcounter{rule} \begin{tabular}{rll} - $e$ $:=$ & \fj{x} & \qquad \textrm{\textsc{E-Var}} \\ + $e$ $:=$\pause & \fj{x} & \qquad \textrm{\textsc{E-Var}} \\ + \pause | & \fj{new C($\overline{e}$)} & \qquad \newtag{\textrm{\textsc{E-Cstr}}}{rule:expr:constructor} \\ + \pause | & \fj{$e$.f} & \qquad \newtag{\textrm{\textsc{E-Field}}}{rule:expr:field} \\ + \pause | & \fj{$e$.m($\overline{e}$)} & \qquad \newtag{\textrm{\textsc{E-Meth}}}{rule:expr:method} \\ + \pause | & \fj{(C)$e$} & \qquad \newtag{\textrm{\textsc{E-Cast}}}{rule:expr:cast} \end{tabular} \end{center} - + \pause \[\fj{new Paire((D)new B().get(), new C(new A())).snd.apply()}\] \end{frame} \subsection{Ses structures} \begin{frame} - + \pause + \textbf{Class table} \only<3>{$+$ \textbf{Expression} = \textbf{Programme}} \begin{fjlisting} \textbf{class} A \textbf{extends} Object \{...\}\\ \textbf{class} B \textbf{extends} Object \{...\}\\ @@ -254,11 +261,12 @@ \subsection{Sa réduction} \begin{frame} - \begin{itemize} - \item $\fj{new C(e1,e2,...,en).field} \rightarrow \fj{ek}$ (\textsc{R-Field}) - \item $\fj{new C(e1,e2,...,en).meth(f1,f2,...,fn)} \rightarrow e_{\fj{C.meth}}\bracket{\fj{new C(e1,e2,...,en)}\middle/ \fj{this},\fj{f1}\middle/\fj{x1},\fj{f2}\middle/\fj{x2},...,\fj{fn}\middle/\fj{xn}}$ (\textsc{R-Invk}) - \item $\fj{(C) expr} \rightarrow \fj{expr}$ (\textsc{R-Cast}) - \end{itemize} + \pause + \begin{itemize}[<+->] + \item $\fj{new C(e1,e2,...,en).field} \rightarrow \fj{ek}$ (\textsc{R-Field}) + \item $\fj{new C(e1,e2,...,en).meth(f1,f2,...,fn)} \rightarrow e_{\fj{C.meth}}\bracket{\fj{new C(e1,e2,...,en)}\middle/ \fj{this},\fj{f1}\middle/\fj{x1},\fj{f2}\middle/\fj{x2},...,\fj{fn}\middle/\fj{xn}}$ (\textsc{R-Invk}) + \item $\fj{(C) expr} \rightarrow \fj{expr}$ (\textsc{R-Cast}) + \end{itemize} \end{frame} \subsection{Son typage} @@ -268,166 +276,79 @@ \[\infer {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})} {\fj{x} \in \Gamma} - \]\[ + \qquad \infer {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}} {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})} - \]\[ + \] + \vspace{.2ex} + \[ \infer {\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{Cc} \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{Cc}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}} - \]\[ + {\begin{array}{c}\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \\ \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{mtype}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}} + \] + \vspace{.2ex} + \[ \infer {\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}}} + \] + \vspace{.2ex} + \[ + \infer {\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}} - \]\[ + \qquad \infer {\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}} \] - \end{frame} \section{Notre problème} \subsection{Qu'est-ce qu'une équivalence} \begin{frame} - \begin{itemize} - \item Deux programmes «font la même chose» - \item Assez stricte - \item Assez large - \end{itemize} - \begin{itemize} - \item Utiliser un autre algorithme (complexités) - \item Utiliser une version plus sécurisée - \item Effectuer une optimisation - \end{itemize} + \begin{exampleblock}{Sens} + \pause + \begin{itemize}[<+->] + \item Deux programmes «font la même chose» + \item Assez stricte + \item Assez large + \end{itemize} + \end{exampleblock} + \pause + \begin{exampleblock}{Utilisations} + \pause + \begin{itemize}[<+->] + \item Utiliser un autre algorithme (complexités) + \item Utiliser une version plus sécurisée + \item Effectuer une optimisation + \end{itemize} + \end{exampleblock} \end{frame} \subsection{La méthode classique} \begin{frame} - \[C\] - - \[C\bracket{P}\] - - \[P \prec Q \iff \forall C\quad C\bracket{P} \implies C\bracket{Q}\] - - \[P \equiv Q \iff P \prec Q \land Q \prec P\] - \end{frame} - \section{Équivalences simples} - - \subsection{Expressions à trou} - \begin{frame} - \[h := \hole \spacebar \fj{new C($\overline{e}$,$h$,$\overline{e}$)} \spacebar \fj{$h$.f} \spacebar \fj{$h$.m($\overline{e}$)} \spacebar \fj{$e$.m($\overline{e}$,$h$,$\overline{e}$)} \spacebar \fj{(C) $h$}\] - - \pause - - \begin{align*} - \hole[e] &= e\\ - (\fj{new C($\overline{e_1}$,$h$,$\overline{e_2}$)})[e] &= \fj{new C($\overline{e_1}$,$h[e]$,$\overline{e_2}$)}\\ - (\fj{$h$.f})[e] &= \fj{$h[e]$.f}\\ - (\fj{$h$.m($\overline{e_1}$)})[e] &= \fj{$h[e]$.m($\overline{e_1}$)}\\ - (\fj{$e_1$.m($\overline{e_2}$,$h$,$\overline{e_3}$)})[e] &= \fj{$e_1$.m($\overline{e_2}$,$h[e]$,$\overline{e_3}$)}\\ - (\fj{(C) $h$})[e] &= \fj{(C) $h[e]$} - \end{align*} - \end{frame} - \begin{frame} - \[C = h \qquad C\bracket{P} = (\mathcal{A},h\bracket{e})\] - \pause - \begin{fjlisting} - class A \{\}\\ - class B \{\}\\ - ...\\ - \only<2>{\fjmain{expr}} - \only<3>{\fjmain{expr.field}} - \only<4>{\fjmain{expr.meth()}} - \only<5>{\fjmain{new Z().meth(expr)}} - \only<6>{\fjmain{new K(expr).snd}} - \only<7>{\fjmain{new K().snd.get(expr.snd)}} - \end{fjlisting} - \end{frame} - \subsection{Premier problème} - \begin{frame} - \begin{tcolorbox} - \small - \lstinputlisting[language=FeatherweightJava,breaklines=true,linerange=1-8]{NeedTestCT.java} - \} - \end{tcolorbox} - \end{frame} - \begin{frame} - \begin{tcolorbox} - \small - \lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={1-4,9-13}]{NeedTestCT.java} - \end{tcolorbox} - \end{frame} - \subsection{Second problème} - \begin{frame} - \[\forall e \exists h \forall p \quad h\bracket{p} \rightarrow^*e\] - - \begin{tcolorbox} \begin{center} - $\fj{new Paire($\hole$,$e$).snd} \rightarrow e$ + Contexte : $C$ + \vspace{2ex}\pause + + Contextualisation : $C\bracket{P}$ + \vspace{2ex}\pause + + Préordre : $P \prec Q \iff \forall C\quad C\bracket{P} \implies C\bracket{Q}$ + \vspace{2ex}\pause + + Équivalence : $P \equiv Q \iff P \prec Q \land Q \prec P$ \end{center} - \end{tcolorbox} - - \[\fj{new C(new D(...), ..., new E(...))}\] - \end{frame} - \subsection{Tentatives de correction} - \begin{frame} - \begin{itemize} - \item Ajout d'une \eng{class table} de test - \item Restreindre les \eng{class tables} - \end{itemize} - - \[\mathcal{A} \prec \mathcal{B} \iff \forall e \forall v \quad (\mathcal{A},e)\Downarrow v \implies (\mathcal{B},e)\Downarrow v\] - - \[C\bracket{P} = (\mathcal{C}, h\bracket{e})\qquad \underline{\text{si } \mathcal{A} \prec \mathcal{C}}\] - - \begin{tcolorbox} - \[P = (\mathcal{A}, e_P) \prec Q = (\mathcal{B}, e_Q) \ssi\] - \[\forall C=(\mathcal{C}, e_C)\quad - \begin{dcases}\mathcal{A} \prec \mathcal{C}\\ \mathcal{B} \prec \mathcal{C} \\ - \forall v\quad C\bracket{P}\Downarrow v \implies C\bracket{Q}\Downarrow v\end{dcases} \] - \end{tcolorbox} \end{frame} - \begin{frame} - \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} - \end{frame} - \begin{frame} - \[\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}\] - \[\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}\] - \end{frame} \section{Idée d'une nouvelle structure} \subsection{Comparer uniquement les CT} \begin{frame} \begin{center} + \pause \begin{multicols}{2} \null\vfill \begin{fjlisting}[width=.49\textwidth] @@ -437,6 +358,7 @@ \end{fjlisting} \vfill\null \columnbreak + \pause \begin{fjlisting}[width=.49\textwidth] \textbf{class} XXX \textbf{extends} XXX \{\\ \}\\ @@ -447,11 +369,12 @@ \end{fjlisting} \end{multicols} \end{center} + \pause \[\fj{new Main().main()}\rightarrow \fj{expr}\] \end{frame} - \subsection{Idées d'une structure} + \subsection{Idée d'une structure} \begin{frame} - \begin{itemize} + \begin{itemize}[<+->] \item Besoin de restreindre les contextes \item Empêcher au test d'accéder à tout \item Utiliser un mécanisme déjà là @@ -463,11 +386,12 @@ \begin{frame} \begin{fjlisting} Number \{\}\\\null + \pause Int \{\}\\ Int : Int suivant(Int)\\ Int : Int add(Int,Int)\\ - Int <: Number\\\null + Int <: Number \end{fjlisting} \end{frame} \begin{frame} @@ -476,6 +400,7 @@ Frac : Frac inverted()\\ Frac : Int floor()\\ Frac <: Number\\\null + \pause RichInt \{Int value\}\\ RichInt : Int getInt()\\ @@ -483,14 +408,19 @@ \end{fjlisting} \end{frame} \begin{frame} - - \begin{itemize} - \item Opérateur d'implémentation ($\triangleright$) - \item Typage avec la TI ($\Vdash$) - \item Validation d'une CT dans une TI - \end{itemize} - + \begin{exampleblock}{Relations à créer} + \pause + \begin{itemize} + \item Opérateur d'implémentation ($\triangleright$) + \pause + \item Typage avec la TI ($\Vdash$) + \pause + \item Validation d'une CT dans une TI + \end{itemize} + \end{exampleblock} + \pause \begin{theorem} + \pause \begin{itemize} \item $\mathcal{A} \triangleright \mathfrak{T}$ \item $\mathcal{B} \OKin \mathfrak{T}$ @@ -505,28 +435,24 @@ \subsection{Leur grammaire} \begin{frame} - \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{TIG-Meth}}}{rule:tsg:method} \\ - | & C \{$\overline{\fj{C}}$ $\overline{\fj{f}}$\} & \qquad \newtag{\textrm{\textsc{TIG-Attr}}}{rule:tsg:attributes} \\ - | & C ($\overline{\fj{C}}$ $\overline{\fj{?}\fj{f}}$) & \qquad \newtag{\textrm{\textsc{TIG-Cstr}}}{rule:tsg:constructor} \\ - | & C <: C & \qquad \newtag{\textrm{\textsc{TIG-Cast}}}{rule:tsg:cast} - \end{tabular} - \end{center} - \end{tcolorbox} - \begin{itemize} - \item Chaque nom de classe est défini au plus une fois par ou bien une \autoref{rule:tsg:attributes} ou bien 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 \fj{Object}). - \end{itemize} + \pause + \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 \textrm{\textsc{TIG-Meth}} \\ + | & C \{$\overline{\fj{C}}$ $\overline{\fj{f}}$\} & \qquad \textrm{\textsc{TIG-Attr}} \\ + | & C ($\overline{\fj{C}}$ $\overline{\fj{?}\fj{f}}$) & \qquad \textrm{\textsc{TIG-Cstr}} \\ + | & C <: C & \qquad \textrm{\textsc{TIG-Cast}} + \end{tabular} + \end{center} + \end{tcolorbox} \end{frame} \subsection{L'opérateur d'implémentation} \begin{frame} - \begin{exampleblock}{} + \[ \infer {\mathcal{A} \triangleright \left[\fj{C : G m($\overline{\texttt{F}}$)}\right]} { @@ -534,16 +460,19 @@ \quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}} \quad \fj{H}\subclass_\mathcal{A}\fj{G} } - \end{exampleblock} - \begin{exampleblock}{} + \qquad + \infer + {\mathcal{A} \triangleright \left[\fj{C} \subclass \fj{D}\right]} + {\fj{C} \subclass_\mathcal{A} \fj{D}} + \] + \vspace{2ex} + \[ \infer {\mathcal{A} \triangleright \left[\fj{ C \{ $\overline{\texttt{E}}\;\overline{\texttt{f}}$\}}\right]} { \overline{\fj{F}}\;\overline{\fj{f}} \subset \operatorname{fields}_\mathcal{A}(C) \quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}} - } - \end{exampleblock} - \begin{exampleblock}{} + }\qquad \infer {\mathcal{A} \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]} {\begin{array}{l} @@ -553,100 +482,90 @@ \overline{\fj{F}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C) \end{array} } - \end{exampleblock} - \begin{exampleblock}{} - \infer - {\mathcal{A} \triangleright \left[\fj{C} \subclass \fj{D}\right]} - {\fj{C} \subclass_\mathcal{A} \fj{D}} - \end{exampleblock} + \] \end{frame} \subsection{Nouvelles applications de \eng{lookup}} - \begin{frame} + \begin{frame}[plain] \ttfamily + \vspace{-3ex} \begin{center} - \begin{multicols}{2} - \begin{exampleblock}{} - \infer - {\operatorname{construct}(\fj{C}) = \overline{\fj{D}}} - {\left[\fj{C($\overline{\texttt{D}}\;\overline{\texttt{?f}}$)}\right] \in \mathfrak{T}} - \end{exampleblock} - \begin{exampleblock}{} - \infer - {\operatorname{construct}(\fj{C}) = \overline{\fj{D}}} - {\fj{class C\{C($\overline{\texttt{D}}\;\overline{\texttt{f}}$)\{...\} ... \}}\in \mathcal{B}} - \end{exampleblock} - \begin{exampleblock}{} - \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}} - \end{exampleblock} - \begin{exampleblock}{} - \infer - {\operatorname{fields}(\fj{C}) = \underbrace{\overline{\fj{D}}\;\overline{\fj{f}}}_{\text{\textrm{pour \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}} - \end{exampleblock} - \begin{exampleblock}{} - \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{B}} - \end{exampleblock} - \begin{exampleblock}{} - \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}} - \end{exampleblock} - \begin{exampleblock}{} - \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{B}} - - \end{exampleblock} - \begin{exampleblock}{} - \infer - {\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}} - {\operatorname{mtype}(\fj{m},\fj{C'}) = \overline{\fj{D}}\rightarrow\fj{E}\quad \fj{C} \subclass \fj{C'}} - \end{exampleblock} - \end{multicols} + \[ + \infer + {\operatorname{construct}(\fj{C}) = \overline{\fj{D}}} + {\left[\fj{C($\overline{\texttt{D}}\;\overline{\texttt{?f}}$)}\right] \in \mathfrak{T}} + \qquad + \infer + {\operatorname{fields}(\fj{C}) = \underbrace{\overline{\fj{D}}\;\overline{\fj{f}}}_{\text{\textrm{pour \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}} + \] + \[ + \infer + {\operatorname{construct}(\fj{C}) = \overline{\fj{D}}} + {\fj{class C\{C($\overline{\texttt{D}}\;\overline{\texttt{f}}$)\{...\} ... \}}\in \mathcal{B}} + \quad + \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}} + \] + \vspace{.2ex} + \[ + \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{B}} + \qquad + \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}} + \] + \vspace{.2ex} + \[ + \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{B}} + \qquad + \infer + {\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}} + {\operatorname{mtype}(\fj{m},\fj{C'}) = \overline{\fj{D}}\rightarrow\fj{E}\quad \fj{C} \subclass \fj{C'}} + \] \end{center} \end{frame} \subsection{Nouveau typage} \begin{frame} - \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{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{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}} - {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})} - & \newtag{\textrm{\textsc{(TI-Field)}}}{rule:ti:field} - \\[3ex] - \infer - {\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{Cc} \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{Cc}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}} - & \newtag{\textrm{\textsc{(TI-Invk)}}}{rule:ti:invoke} - \\[3ex] - \infer - {\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{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} - \\[3ex] - \infer - {\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} - \end{tabular} + \begin{tcolorbox} + \vspace{-1ex} + \[ + \infer + {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})} + {\fj{x} \in \Gamma} + \qquad + \infer + {\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{Cc} \quad \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \\ \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{mtype}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}} + \] + \[ + \infer + {\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}}} + \] + \vspace{.3ex} + \[ + \infer + {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}} + {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})} + \] + \vspace{.3ex} + \[ + \infer + {\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}} + \qquad + \infer + {\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}} + \] \end{tcolorbox} \end{frame} \subsection{Théorème de cohérence}