diff --git a/DiaposSoutenance.tex b/DiaposSoutenance.tex index c694aec..796e925 100644 --- a/DiaposSoutenance.tex +++ b/DiaposSoutenance.tex @@ -1,5 +1,5 @@ % !TeX spellcheck = fr_FR -\documentclass[12pt]{beamer} +\documentclass[12pt,xcolor={dvipsnames}]{beamer} % Loading packages \usepackage[T1]{fontenc} @@ -28,7 +28,6 @@ \usepackage{mathtools} \usepackage{setspace} \usepackage{pdfpc} - \usepackage{geometry} \usepackage{subcaption} @@ -200,6 +199,11 @@ \makeatother \setbeamertemplate{itemizeitem}{\scriptsize$\diamond$} +\newcommand\sectocframe{ + \begin{frame} + \tableofcontents[currentsection,hideothersubsections,sections=\value{section}] + \end{frame} +} \author{Samy Avrillon} \title{Définition d'un préordre sur les programmes Featherweight Java} @@ -223,7 +227,7 @@ \end{frame} \section{Featherweight Java} - + \sectocframe \subsection{Sa grammaire} \begin{frame} @@ -284,54 +288,55 @@ \begin{frame} \pause \[\infer - {\mathcal{A},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})} + {\mathcal{A},\Gamma \vdash \fj{x} : \Gamma(\fj{x})} {\fj{x} \in \Gamma} \qquad \infer - {\mathcal{A},\Gamma \Vdash \fj{$e$.f} : \fj{C}} - {\mathcal{A},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})} + {\mathcal{A},\Gamma \vdash \fj{$e$.f} : \fj{C}} + {\mathcal{A},\Gamma \vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})} \] \pause \vspace{.2ex} \[ \infer - {\mathcal{A},\Gamma \Vdash \fj{$e$.m($\overline{e_x}$)} : \fj{C}} - {\begin{array}{c}\mathcal{A},\Gamma \Vdash e : \fj{Cc} \quad \mathcal{A},\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}} + {\mathcal{A},\Gamma \vdash \fj{$e$.m($\overline{e_x}$)} : \fj{C}} + {\begin{array}{c}\mathcal{A},\Gamma \vdash e : \fj{Cc} \quad \mathcal{A},\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 - {\mathcal{A},\Gamma \Vdash \fj{new C(}\overline{e_x}\fj{)} : \fj{C}} - {\mathcal{A},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{constructor}(\fj{C}) = \overline{\fj{D}}} + {\mathcal{A},\Gamma \vdash \fj{new C(}\overline{e_x}\fj{)} : \fj{C}} + {\mathcal{A},\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 - {\mathcal{A},\Gamma \Vdash \fj{(C)$e$} : \fj{C}} - {\mathcal{A},\Gamma \Vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}} + {\mathcal{A},\Gamma \vdash \fj{(C)$e$} : \fj{C}} + {\mathcal{A},\Gamma \vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}} \qquad \infer - {\mathcal{A},\Gamma \Vdash \fj{(C)$e$} : \fj{C}} - {\mathcal{A},\Gamma \Vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}} + {\mathcal{A},\Gamma \vdash \fj{(C)$e$} : \fj{C}} + {\mathcal{A},\Gamma \vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}} \] \end{frame} \section{Notre problème} - + \sectocframe \subsection{Qu'est-ce qu'une équivalence} \begin{frame} \begin{exampleblock}{Sens} \pause - \begin{itemize}[<+->] + \begin{itemize} \item Deux programmes «font la même chose» + \pause \item Assez stricte + \pause \item Assez large \end{itemize} \end{exampleblock} \pause \begin{exampleblock}{Utilisations} - \pause - \begin{itemize}[<+->] + \begin{itemize} \item Utiliser un autre algorithme (complexités) \item Utiliser une version plus sécurisée \item Effectuer une optimisation @@ -341,21 +346,21 @@ \subsection{La méthode classique} \begin{frame} \begin{center} - Contexte : $C$ + Contexte : $C$, typiquement $\boxed{\fj{$\hole$.meth(new A())}}$ \vspace{2ex}\pause - Contextualisation : $C\bracket{P}$ + Contextualisation : $C\bracket{P}$, exemple $\boxed{(\mathcal{A},\fj{e.meth(new A())})}$ \vspace{2ex}\pause - Préordre : $P \prec Q \iff \forall C\quad C\bracket{P}\rightarrow^* v \implies C\bracket{Q}\rightarrow^* v$ + Préordre : $P \prec Q \iff \forall C\quad\exists v\quad C\bracket{P}\rightarrow^* v \implies C\bracket{Q}\rightarrow^* v$ \vspace{2ex}\pause Équivalence : $P \equiv Q \iff P \prec Q \land Q \prec P$ \end{center} \end{frame} - \section{Idée d'une nouvelle structure} - + \section{Une nouvelle structure} + \sectocframe \subsection{Comparer uniquement les CT} \begin{frame} \begin{center} @@ -386,14 +391,51 @@ \subsection{Idée d'une structure} \begin{frame} \begin{itemize}[<+->] - \item Spécifier ce que l'on veut tester + \item Les simples expressions à trou + \begin{itemize}[<+->] + \item Pas assez puissant + \item Bloque sur les différences syntaxiques + \end{itemize} + \item Inclure une \eng{class table} de tests \item Empêcher au test d'accéder à tout \item Utiliser un mécanisme déjà là \item Inspiration: \eng{header file} en C \end{itemize} \end{frame} + \begin{frame} + \begin{center} + \large\only<1>{Compilation (typage)}\only<2>{Execution (réduction)} + \end{center} + \begin{tcolorbox}[colback=SpringGreen] + \begin{tcolorbox}[colback=cyan] + \begin{center} + \only<1>{Test interface $\mathfrak{T}$ + \begin{itemize} + \item classe \fj{List} + \item méthode \fj{Sort.sort} + \end{itemize} + } + \only<2>{Class table $\mathcal{A}$ + \begin{itemize} + \item classe \fj{List} + \item méthode \fj{Sort.sort} + \item classe \fj{Map} + \end{itemize} + } + \end{center} + \end{tcolorbox} + \begin{tcolorbox}[colback=orange] + \begin{center} + Class table $\mathcal{B}$ + \end{center} + \end{tcolorbox} + \begin{center} + \fj{expression de test} + \end{center} + \end{tcolorbox} + \end{frame} - \subsection{Exemple et théorème} + \subsection{Exemple de \eng{test interface}} \begin{frame} \begin{fjlisting} Number \{\}\\\null @@ -419,171 +461,9 @@ \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}$ - \item $\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D}$ - \end{itemize} - - \[\mathcal{A} \oplus \mathcal{B},\Gamma \vdash e : \fj{C}\quad\text{et}\quad\fj{C} \subclass \fj{D}\] - \end{theorem} \end{frame} - \section{Formalisation des \eng{test interfaces}} - - \subsection{Leur grammaire} - \begin{frame} - \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} - \[ - \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}} - }\qquad - \pause - \infer - {\mathcal{A} \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]} - {\begin{array}{l} - \exists \overline{\fj{f'}}\quad \overline{\fj{f0}} = \overline{\fj{f}}\boxplus\overline{\fj{f'}} \\ - \overline{\fj{F}} = \overline{\fj{E}} \quad\text{où \fj{f} est défini} \\ - \overline{\fj{E}} \subclass \overline{\fj{F}} \quad \land \quad - \overline{\fj{F}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C) - \end{array} - } - \] - \vspace{2ex} - \[ - \infer - {\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} - } - \qquad - \infer - {\mathcal{A} \triangleright \left[\fj{C} \subclass \fj{D}\right]} - {\fj{C} \subclass_\mathcal{A} \fj{D}} - \] - - - \end{frame} - - \subsection{Nouvelles applications de \eng{lookup}} - \placelogofalse - \begin{frame} - \ttfamily - \vspace{-3ex} - \pause - \begin{center} - \[ - \onslide<2->{\infer - {\operatorname{construct}(\fj{C}) = \overline{\fj{D}}} - {\left[\fj{C($\overline{\texttt{D}}\;\overline{\texttt{?f}}$)}\right] \in \mathfrak{T}}} - \qquad - \onslide<3->{ - \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}} - } - \] - \[ - \onslide<2->{ - \infer - {\operatorname{construct}(\fj{C}) = \overline{\fj{D}}} - {\fj{class C\{C($\overline{\texttt{D}}\;\overline{\texttt{f}}$)\{...\} ... \}}\in \mathcal{B}} - } - \quad - \onslide<3->{ - \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} - \onslide<3->{ - \[ - \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} - \vspace{-2ex} - \pause - \[ - \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} - \pause - \[ - \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}} - \] - \vspace{.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}}} - \] - \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{frame} - \placelogotrue - \subsection{Théorème de cohérence} + \subsection{Théorème de cohérence} \begin{frame} \pause \begin{theorem} @@ -598,26 +478,25 @@ Alors il existe \fj{C} tel que $\mathcal{A} \oplus \mathcal{B},\Gamma \vdash e : \fj{C}$ et $\fj{C} \subclass \fj{D}$. \end{theorem} \end{frame} - - \subsection{Définition du préordre} - \begin{frame} - \pause - \begin{definition} - Soit une \eng{test interface} $\mathfrak{T}$. - - Soient deux \eng{class tables} $\mathcal{A}$ et $\mathcal{B}$ qui implémentent toutes deux $\mathfrak{T}$ - - Alors - \[\mathcal{A} \prec_\mathfrak{T} \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} - \end{frame} - + + \subsection{Définition du préordre} + \begin{frame} + \pause + \begin{definition} + Soit une \eng{test interface} $\mathfrak{T}$. + + Soient deux \eng{class tables} $\mathcal{A}$ et $\mathcal{B}$ qui implémentent toutes deux $\mathfrak{T}$ + + $\mathcal{A} \prec_\mathfrak{T} \mathcal{A'}$ si et seulement si + + Pour tout test $(\mathcal{B},e)$ tel que $\mathcal{B} \OKin \mathfrak{T}$ et $\mathfrak{T},\mathcal{B} \Vdash e : \fj{D}$ + \[\exists v \quad \mathcal{A}\oplus\mathcal{B} \rightarrow^* v \implies \mathcal{A'}\oplus\mathcal{B}\rightarrow^* v\] + \end{definition} + \end{frame} + + \section{Les valeurs infinies} - + \sectocframe \subsection{Qu'est-ce qu'un context lemma} \begin{frame} @@ -686,28 +565,27 @@ \begin{frame} \[\boxed{\mathcal{A} \prec_\mathfrak{T} \mathcal{A'}}\qquad \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\] - - \[\boxed{\mathcal{A} \pprec_\mathfrak{T} \mathcal{A'}}\quad \forall \hbar,\alpha,(\mathcal{B},e) \left|\begin{array}{l} + \mathfrak{T},\mathcal{B} \Vdash e : \fj{D} + \end{array}\right.\] + \[ + \mathcal{A}\oplus\mathcal{B} \Downarrow v \implies \mathcal{A'}\oplus\mathcal{B}\Downarrow v\] + \rule{.95\textwidth}{1px} + \[\boxed{\mathcal{A} \pprec_\mathfrak{T} \mathcal{A'}}\qquad \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} \rightarrow^*\hbar\bracket{\alpha} - \end{array}\right. \implies \exists\beta\quad \mathcal{A'}\oplus\mathcal{B}\rightarrow^* \hbar\bracket{\beta}\] + \mathfrak{T},\mathcal{B} \Vdash e : \fj{D} + \end{array}\right.\] + \[\forall \hbar,\alpha \quad \mathcal{A}\oplus\mathcal{B} \rightarrow^*\hbar\bracket{\alpha} + \implies \exists\beta\quad \mathcal{A'}\oplus\mathcal{B}\rightarrow^* \hbar\bracket{\beta}\] \end{frame} \subsection{Propriétés} \begin{frame} - \pause - \begin{property} - \[\forall \hbar \forall \alpha \quad \hbar\bracket{\alpha}\rightarrow^* e' \implies \exists \beta\quad e' = \hbar\bracket{\beta}\] - \end{property} \pause \begin{property} \[\mathcal{A} \pprec \mathcal{B} \implies \mathcal{A} \prec \mathcal{B}\] \end{property} \pause \begin{property}[Context Lemma] + \vspace{-3ex} \begin{gather*} \forall \mathcal{A} \quad\forall e,f \quad\forall (h,\mathcal{B})\\ (e,\mathcal{A})\pprec(f,\mathcal{B}) \implies (h[e],\mathcal{A} \oplus \mathcal{B})\pprec(h[f],\mathcal{A}\oplus\mathcal{B}) @@ -740,4 +618,144 @@ \begin{frame} \Huge\[\mathfrak{FIN}\] \end{frame} + + \appendix + \section{Formalisation des \eng{test interfaces}} + + \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 \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} + \[ + \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}} + }\qquad + \infer + {\mathcal{A} \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]} + {\begin{array}{l} + \exists \overline{\fj{f'}}\quad \overline{\fj{f0}} = \overline{\fj{f}}\boxplus\overline{\fj{f'}} \\ + \overline{\fj{F}} = \overline{\fj{E}} \quad\text{où \fj{f} est défini} \\ + \overline{\fj{E}} \subclass \overline{\fj{F}} \quad \land \quad + \overline{\fj{F}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C) + \end{array} + } + \] + \vspace{2ex} + \[ + \infer + {\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} + } + \qquad + \infer + {\mathcal{A} \triangleright \left[\fj{C} \subclass \fj{D}\right]} + {\fj{C} \subclass_\mathcal{A} \fj{D}} + \] + + + \end{frame} + + \subsection{Nouvelles applications de \eng{lookup}} + \placelogofalse + \begin{frame} + \ttfamily + \vspace{-3ex} + \begin{center} + \[ + \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} + \placelogotrue + \subsection{Nouveau typage} + \begin{frame} + \vspace{-2ex} + \[ + \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{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}} + \] + \vspace{.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}}} + \] + \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{frame} + \end{document} \ No newline at end of file