diff --git a/.gitignore b/.gitignore index 567609b..345ad9a 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ build/ +svg-inkscape/ diff --git a/DiaposSoutenance.tex b/DiaposSoutenance.tex new file mode 100644 index 0000000..3a775b1 --- /dev/null +++ b/DiaposSoutenance.tex @@ -0,0 +1,782 @@ +% !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} \ No newline at end of file diff --git a/logoEns.svg b/logoEns.svg new file mode 100644 index 0000000..39dfb4e --- /dev/null +++ b/logoEns.svg @@ -0,0 +1,19 @@ + + + + + + +