% !TeX spellcheck = fr_FR \documentclass[12pt]{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{enumitem} \usepackage{amsfonts} \usepackage{mathtools} \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 \author{Samy Avrillon} \title{Définition d'un préordre sur les programmes Featherweight Java} \subtitle{Notes sur mon stage au LACL} \logo{\includesvg[width=1.5cm]{logoEns}} \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{Introduction} \section{Featherweight Java} \subsection{Sa grammaire} \begin{frame} \begin{center} \refstepcounter{rule} \begin{tabular}{rll} $e$ $:=$ & \fj{x} & \qquad \textrm{\textsc{E-Var}} \\ | & \fj{new C($\overline{e}$)} & \qquad \newtag{\textrm{\textsc{E-Cstr}}}{rule:expr:constructor} \\ | & \fj{$e$.f} & \qquad \newtag{\textrm{\textsc{E-Field}}}{rule:expr:field} \\ | & \fj{$e$.m($\overline{e}$)} & \qquad \newtag{\textrm{\textsc{E-Meth}}}{rule:expr:method} \\ | & \fj{(C)$e$} & \qquad \newtag{\textrm{\textsc{E-Cast}}}{rule:expr:cast} \end{tabular} \end{center} \[\fj{new Paire((D)new B().get(), new C(new A())).snd.apply()}\] \end{frame} \subsection{Ses structures} \begin{frame} \begin{fjlisting} \textbf{class} A \textbf{extends} Object \{...\}\\ \textbf{class} B \textbf{extends} Object \{...\}\\ \fjclass{Paire}{\fjattr{fst} \fjattr{snd}}{}\\ \pause \fjmain{new Paire(new A(), new B())} \end{fjlisting} \end{frame} \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} \end{frame} \subsection{Son typage} \begin{frame} \[\infer {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})} {\fj{x} \in \Gamma} \]\[ \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})} \]\[ \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}} \]\[ \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}}} {\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}} \]\[ \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} \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$ \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} \begin{multicols}{2} \null\vfill \begin{fjlisting}[width=.49\textwidth] \textbf{class} XXX \textbf{extends} XXX \{\}\\ \vdots\\ \fjmain{expression} \end{fjlisting} \vfill\null \columnbreak \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} \[\fj{new Main().main()}\rightarrow \fj{expr}\] \end{frame} \subsection{Idées d'une structure} \begin{frame} \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à \item Inspiration: \eng{header file} en C \end{itemize} \end{frame} \subsection{Exemple et théorème} \begin{frame} \begin{fjlisting} Number \{\}\\\null Int \{\}\\ Int : Int suivant(Int)\\ Int : Int add(Int,Int)\\ Int <: Number\\\null \end{fjlisting} \end{frame} \begin{frame} \begin{fjlisting} Frac(Int numerateur, Int denominateur)\\ Frac : Frac inverted()\\ Frac : Int floor()\\ Frac <: Number\\\null RichInt \{Int value\}\\ RichInt : Int getInt()\\ RichInt <: Int \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{theorem} \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} \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} \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]} { \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} } \end{exampleblock} \begin{exampleblock}{} \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}{} \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} } \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} \ttfamily \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} \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} \end{tcolorbox} \end{frame} \subsection{Théorème de cohérence} \begin{frame} \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} \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\] où $\mathcal{A} \oplus \mathcal{B}$ dénote l'ensemble des classes de $\mathcal{A}$ auquel on a ajouté les classes de $\mathcal{B}$ dont les noms n'étaient pas déjà dans $\mathcal{A}$. \end{definition} \end{frame} \section{Les valeurs infinies} \subsection{Qu'est-ce qu'un context lemma} \begin{frame} \[(\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} \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} \[e_i = \fj{intList(0)} \quad\text{et}\quad e_0 = \fj{zeroList()}\] \end{frame} \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} \textsc{E-Var} et \textsc{E-Cstr} \[\fj{new C(x,new S(new S(y,new G()),z))}\] \[(\mathcal{A},e)\pprec(\mathcal{B},f) \ssi \forall \hbar \forall \alpha \quad \left(e \rightarrow_\mathcal{A}^* \hbar\bracket{\alpha} \implies \exists \beta\quad f \rightarrow_\mathcal{B}^* \hbar\bracket{\beta}\right)\] \end{frame} \subsection{Redéfinition des préordres} \begin{frame} \[\mathcal{A}\pprec\mathcal{B} \ssi \forall e \quad (\mathcal{A},e) \pprec (\mathcal{B},e)\] \end{frame} \subsection{Propriétés} \begin{frame} \begin{property} \[\forall \hbar \forall \alpha \quad \hbar\bracket{\alpha}\rightarrow^* e' \implies \exists \beta\quad e' = \hbar\bracket{\beta}\] \end{property} \begin{property} \[\mathcal{A} \pprec \mathcal{B} \implies \mathcal{A} \prec \mathcal{B}\] \end{property} \begin{property}[Context Lemma] \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{Exemple concret} \begin{frame} \begin{tcolorbox} \lstinputlisting[language=Java,breaklines=true,linerange={2-26}]{FinalExample.java} \lstinputlisting[language=Java,breaklines=true,linerange={29-62}, texcl]{FinalExample.java} \lstinputlisting[language=FeatherweightJava,breaklines=true,linerange={65-78}]{FinalExample.java} \end{tcolorbox} \end{frame} \section{Conclusion} \begin{frame} \begin{tcolorbox} \begin{itemize} \item On a créé un préordre \item Assez puissant (sémantique) \item Assez tolérant \item Context Lemma \item Utilisable autre part \end{itemize} \end{tcolorbox} \begin{tcolorbox} \begin{itemize} \item Comparer uniquement certains types de retour \item Théorèmes pour simplifier l'équivalence \end{itemize} \end{tcolorbox} \end{frame} \begin{frame} \LARGE\[\mathfrak{FIN}\] \end{frame} \end{document}