% !TeX spellcheck = fr_FR \documentclass[12pt,xcolor={dvipsnames}]{beamer} % Loading packages \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{amsmath} \usepackage{amssymb} \usepackage{bbm} \usepackage{stmaryrd} \usepackage[main=french,english]{babel} \usepackage{csquotes} \usepackage{listings} \usepackage{lstautogobble} \usepackage{algorithm2e} \usepackage{svg} \usepackage{tikz} \usepackage{multirow} \usepackage{multicol} \usepackage{tcolorbox} \usepackage{mdframed} \usepackage{proof} \usepackage{biblatex} \usepackage{xparse} \usepackage{cprotect} \usepackage{xpatch} \usepackage{amsfonts} \usepackage{mathtools} \usepackage{setspace} \usepackage{pdfpc} \usepackage{geometry} \usepackage{subcaption} \usepackage{csquotes} \usepackage[lighttt]{lmodern} \usetikzlibrary{shapes.geometric,positioning} % Macros caractères globales \newcommand{\pgrph}{\P} \newcommand{\hsep}{\vspace{.2cm}\centerline{\rule{0.8\linewidth}{.05pt}}\vspace{.4cm}} \renewcommand{\P}{\mathbb{P}} \newcommand{\E}{\mathbb{E}} \newcommand{\1}{\scalebox{1.2}{$\mathbbm{1}$}} \newcommand{\floor}[1]{\left\lfloor#1\right\rfloor} \newcommand{\littleO}{o} \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{\ssi}{\quad\text{\underline{ssi}}\quad} \newcommand\eng[1]{\textit{\foreignlanguage{english}{#1}}} \newcommand\spacebar{\;|\;} \def\nDownarrow{\not\mspace{1mu}\Downarrow} \let\pprec\preccurlyeq \DeclareUnicodeCharacter{03BB}{$\lambda$} \DeclareUnicodeCharacter{03B1}{$\alpha$} \DeclareUnicodeCharacter{03C0}{$\pi$} % Création des environnement globaux \newtheorem{property}{Propriété} \newcounter{rule} % Commandes logiques globales \newcommand{\ifnullthenelse}[3]{ \ifnum\value{#1}=0 #2 \else #3 \fi } %%% Commande \newtag permettant de changer le label d'une equation \makeatletter \newcommand\newtag[2]{#1\def\@currentlabel{#1}\label{#2}} \makeatother % Macros caractères spécifiques au document \newcommand{\methprec}[1]{\prec\mkern-8mu\left[\fj{#1}\right]} \DeclareMathOperator{\varnull}{varnull} \DeclareMathOperator{\nextop}{next} \DeclareMathOperator{\new}{\text{\textbf{new}}} \DeclareMathOperator{\CT}{CT} \DeclareRobustCommand{\leftsarrow}{\text{\reflectbox{$\;\rightarrow^*$}}} \newcommand\subclass{\mathrel{<:}} \newcommand\superclass{\mathrel{:>}} \newcommand\OKin{\text{\textnormal{\textsc{ OK in }}}} % Création des environnements spécifiques au document %%% Blocs colorés pour le code FeatherweightJava \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} \newtcbox{\fjind}{nobeforeafter,tcbox raise base, rounded corners=all, boxsep=0pt,left=1pt,right=1pt,top=1pt,bottom=1pt,boxrule=0pt,colback=white!52!orange} \newenvironment{fjlisting}[1][] { \begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!96!black,#1] \ttfamily }{ \end{tcolorbox} } % Langage Featherweight Java \makeatletter \newcommand*\idstyle{% \expandafter\id@style\the\lst@token\relax } \def\id@style#1#2\relax{% \ifcat#1\relax\else \ifnum`#1=\lccode`#1% \ttfamily \fi \fi } \makeatother \lstdefinelanguage{FeatherweightJava}{ keywords = {new, this, true, false}, basicstyle=\ttfamily, identifierstyle=\idstyle, literate=% {à}{{\`a}}1 {é}{{\'e}}1 {è}{{\`e}}1 {ù}{{\`u}}1 } \lstset{literate=% {à}{{\`a}}1 {é}{{\'e}}1 {è}{{\`e}}1 {ù}{{\`u}}1} %% Commande 4 \NewDocumentEnvironment{textenv}{b}{\text{\textnormal{#1}}}{} %\lstMakeShortInline[language=FeatherweightJava]| \newcommand{\fj}[1]{\begin{textenv}\lstinline[language=FeatherweightJava,mathescape=true]~#1~\end{textenv}} % Définition des macros pour l'écriture des trucs Featherweight Java \newcommand\fjattr{\GenericWarning{$\backslash$ fjattr doit être utilisé dans une fjclass}} \newcounter{fjargcount} \newcommand{\fjparamattributes}[2][Object]{ \null\qquad #1 #2;\newline } \newcommand{\printcomma}{,} \newcommand{\fjparamconstparameters}[2][Object]{ \ifnullthenelse{fjargcount}{}{,$\text{ }$} \text{#1} \;\text{#2} \stepcounter{fjargcount} } \newcommand{\fjparamconstassign}[2][Object]{ \null\qquad\qquad \textbf{this}.#2 = #2;\newline } \newcommand{\fjmethod}[4]{ \null\qquad #1 #2(#3)\{\newline \null\qquad\qquad \textbf{return} \lstinline[language=FeatherweightJava]{#4};\newline \null\qquad\}\newline } \newcommand{\fjmain}[1]{ \noindent\fjmaincodebox{\lstinline[language=Java]{#1}} } % Premier argument: Nom de la classe % Second argument: \fjattr{x}[Object] \fjattr{attr}[A] % Troisième argument \fjmethod{C}{metname}{Object w, B par}{((D)obj).apply(par)} plusieurs fois % Argument optionnel: la classe que l'on extend \newcommand{\fjclass}[4][Object]{% \noindent \textbf{class} #2 \textbf{extends} #1 \{\newline % Attributs \let\fjattr\fjparamattributes #3 % Constructeur \let\fjattr\fjparamconstparameters \setcounter{fjargcount}{0} \null\qquad #2(\ifx&\else $#3$\fi) \{\newline \null\qquad\qquad \textbf{super}();\newline \let\fjattr\fjparamconstassign% #3 \null\qquad\}\\ % Méthodes #4 \} } \addbibresource{Bilibibio.bib} \usetheme{Madrid} \hypersetup{pdfpagemode=FullScreen} % Transition en fade-in par défaut \addtobeamertemplate{background canvas}{\transfade[duration=0.4]}{} \addtobeamertemplate{frametitle}{ \let\insertframetitle\insertsubsectionhead}{} \makeatletter \CheckCommand*\beamer@checkframetitle{\@ifnextchar\bgroup\beamer@inlineframetitle{}} \renewcommand*\beamer@checkframetitle{\global\let\beamer@frametitle\relax\@ifnextchar\bgroup\beamer@inlineframetitle{}} \makeatother \setbeamertemplate{itemizeitem}{\scriptsize$\diamond$} \newcommand\sectocframe[1][]{ \begin{frame} \pdfpcnote{#1} \tableofcontents[currentsection,hideothersubsections,sections=\value{section}] \end{frame} } \author{Samy Avrillon} \title{Définition d'un préordre sur les programmes Featherweight Java} \subtitle{Notes sur mon stage au LACL} \newif\ifplacelogo % create a new conditional \placelogotrue % set it to true \logo{\ifplacelogo\includesvg[width=1.5cm]{logoEns}\fi} \institute{ENS de Lyon} \begin{document} \begin{frame}[plain] \maketitle \end{frame} \section*{Sommaire} \begin{frame} \begin{multicols}{2} \tableofcontents[pausesections,hideallsubsections] \end{multicols} \end{frame} \section{Featherweight Java} \sectocframe \subsection{Sa grammaire} \begin{frame} \begin{center} \refstepcounter{rule} \begin{tabular}{rll} $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()}\] \pdfpcnote{Distinction ouvert/ferme\\Définition valeur} \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} A \{...\}\\ \textbf{class} Paire \textbf{extends} Object \{\\ \null\qquad A fst;\\ \null\qquad B snd;\\ \null\qquad Paire(A fst, B snd)\{...\}\\ \null\qquad B getBFst()\{\\ \null\qquad\qquad \textbf{return} (B)this.fst;\\ \null\qquad\}\\ \}\\ \pause \fjmain{new Paire(new A(), new B())} \end{fjlisting} \end{frame} \subsection{Sa réduction} \begin{frame} \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) new D(...)} \rightarrow \fj{new D(...)}$ si $\fj{D}\subclass\fj{C}$ (\textsc{R-Cast}) \item $e \rightarrow^* f \implies h\bracket{e} \rightarrow^* h\bracket{f}$ \end{itemize} \end{frame} \subsection{Son typage} \begin{frame} \pause \[\infer {\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})} \] \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}} \] \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}}} \] \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}} \qquad \infer {\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[4:45] \subsection{Qu'est-ce qu'une équivalence} \begin{frame} \begin{exampleblock}{Sens} \pause \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} \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} \begin{center} Contexte : $C$, typiquement $\boxed{\fj{$\hole$.meth(new A())}}$ \vspace{2ex}\pause 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\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{Une nouvelle structure} \sectocframe[7:20] \subsection{Comparer uniquement les CT} \begin{frame} \begin{center} \pause \begin{multicols}{2} \null\vfill \begin{fjlisting}[width=.49\textwidth] \textbf{class} XXX \textbf{extends} XXX \{\}\\ \vdots\\ \fjmain{expr} \end{fjlisting} \vfill\null \columnbreak \pause \begin{fjlisting}[width=.49\textwidth] \textbf{class} XXX \textbf{extends} XXX \{\\ \}\\ \vdots\\ \textbf{class} Main \{\\ \fjmethod{Object}{main}{}{expr} \} \end{fjlisting} \end{multicols} \end{center} \pause \[\fj{new Main().main()}\rightarrow \fj{expr}\] \end{frame} \subsection{Idée d'une structure} \begin{frame} \begin{itemize}[<+->] \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} \pdfpcnote{9:30} \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 de \eng{test interface}} \begin{frame} \begin{fjlisting} Number \{\}\\\null \pause Int \{\}\\ Int : Int add(Int)\\ Int <: Number\\ \pause Frac (Int numerateur, Int)\\ RichInt \{Int value\} \end{fjlisting} \end{frame} \begin{frame} \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} \end{frame} \subsection{Théorème de cohérence} \begin{frame} \pause \begin{theorem} \label{thm:tiTyp} Soit une \eng{test interface} $\mathfrak{T}$, une \eng{class table} $\mathcal{A}$, un couple $(\mathcal{B},e)$ \eng{class table} $\times$ expression fermée appelée \enquote{test}, et un environnement de typage $\Gamma$ vérifiant \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} 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}$ $\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[15:00] \subsection{Qu'est-ce qu'un context lemma} \begin{frame} \pause \[(\mathcal{A},e)\prec(\mathcal{B},f) \implies (\mathcal{A},h\bracket{e})\prec(\mathcal{A},h\bracket{f})\] \end{frame} \subsection{Pourquoi est-il faux ici} \placelogofalse \begin{frame} \begin{fjlisting} public Static \{\\ \fjmethod{IList}{intList}{Int i}{new IList(i, intList(i+1))} \fjmethod{IList}{zeroList}{}{new IList(0, zeroList())} \} \end{fjlisting} \vspace{-3ex} \begin{gather*} e_i = \fj{intList(0)} \rightarrow^*\\ \fj{new IList(0,new IList(1,new IList(2,intList(3))))}\\ e_0 = \fj{zeroList()} \rightarrow^*\\ \fj{new IList(0,new IList(0,new IList(0,zeroList())))} \end{gather*} \end{frame} \placelogotrue \begin{frame} \[ \begin{array}{rcl} h\bracket{e_i} &=& \fj{intList(0).next.obj}\\ &\rightarrow& \fj{new IList(0, intList(0+1)).next.obj}\\ &\rightarrow& \fj{intList(0+1).obj}\\ &\rightarrow& \fj{new IList(0+1, intList(0+1+1)).obj}\\ &\rightarrow& \fj{0+1}\\ &\rightarrow^{\!*}& \fj{1}\\ h\bracket{e_0} &=& \fj{zeroList().next.obj}\\ &\rightarrow& \fj{new IList(0, zeroList()).next.obj}\\ &\rightarrow& \fj{zeroList().obj}\\ &\rightarrow& \fj{new IList(0, zeroList()).obj}\\ &\rightarrow& \fj{0} \end{array} \] \end{frame} \subsection{Idée de valeurs infinies} \subsection{Explication de la formalisation} \begin{frame} \begin{center} Comment capturer ces \enquote{valeurs infinies} ? \vspace{1ex} \pause Valeurs à variable: $\hbar$ \[\fj{new C(x,new S(new S(y,new G()),z))}\] \pause \[\boxed{e\rightarrow^* v \implies f\rightarrow^* v}\Rrightarrow \boxed{\forall \hbar \forall \alpha \; \left(e \rightarrow_\mathcal{A}^* \hbar\bracket{\alpha} \implies \exists \beta\quad f \rightarrow_\mathcal{B}^* \hbar\bracket{\beta}\right)}\] \pause \[e \rightarrow^* \fj{new C(new D(...))} \implies f \rightarrow^* \fj{new C(new D(...))}\] \begin{gather*} \fj{new IList(0,new IList(1,...))}\\ \neq\\ \fj{new IList(0,new IList(0,...))} \end{gather*} \end{center} \end{frame} \subsection{Redéfinition des préordres} \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} \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} \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} \[\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}) \end{gather*} \end{property} \end{frame} \section{Conclusion} \subsection{Conclusion} \begin{frame} \pdfpcnote{18:30} \begin{exampleblock}{Résumé} \begin{itemize}[<+->] \item On a créé un préordre \item Assez puissant (sémantique) \item Assez tolérant \item Context Lemma \item Concepts réutilisables \end{itemize} \end{exampleblock} \begin{exampleblock}{Futur} \begin{itemize}[<+->] \item Formalisation dans un assistant de preuve \item Comparer uniquement certains types de retour \item Théorèmes pour simplifier l'équivalence \item Obtenir des retours \end{itemize} \end{exampleblock} \end{frame} \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}