From ab247d4e3641d9a325513cb6e5459f6d889c7650 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Sat, 27 Aug 2022 18:27:47 +0200 Subject: [PATCH] =?UTF-8?q?=C3=89courtage?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- DiaposSoutenance.tex | 157 ++++++++++++++++++++++++++----------------- 1 file changed, 94 insertions(+), 63 deletions(-) diff --git a/DiaposSoutenance.tex b/DiaposSoutenance.tex index 8783974..ef854b3 100644 --- a/DiaposSoutenance.tex +++ b/DiaposSoutenance.tex @@ -27,6 +27,7 @@ \usepackage{amsfonts} \usepackage{mathtools} \usepackage{setspace} +\usepackage{pdfpc} \usepackage{geometry} \usepackage{subcaption} @@ -203,7 +204,9 @@ \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}} +\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} @@ -242,7 +245,6 @@ \end{center} \pause \[\fj{new Paire((D)new B().get(), new C(new A())).snd.apply()}\] - \end{frame} \subsection{Ses structures} \begin{frame} @@ -272,7 +274,7 @@ \subsection{Son typage} \begin{frame} - + \pause \[\infer {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})} {\fj{x} \in \Gamma} @@ -281,6 +283,7 @@ {\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})} \] + \pause \vspace{.2ex} \[ \infer @@ -487,29 +490,38 @@ \end{frame} \subsection{Nouvelles applications de \eng{lookup}} - \begin{frame}[plain] + \placelogofalse + \begin{frame} \ttfamily \vspace{-3ex} + \pause \begin{center} \[ - \infer + \onslide<2->{\infer {\operatorname{construct}(\fj{C}) = \overline{\fj{D}}} - {\left[\fj{C($\overline{\texttt{D}}\;\overline{\texttt{?f}}$)}\right] \in \mathfrak{T}} + {\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})} @@ -529,47 +541,50 @@ {\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}} {\operatorname{mtype}(\fj{m},\fj{C'}) = \overline{\fj{D}}\rightarrow\fj{E}\quad \fj{C} \subclass \fj{C'}} \] + } \end{center} \end{frame} \subsection{Nouveau typage} \begin{frame} - \begin{tcolorbox} - \vspace{-1ex} - \[ - \infer - {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})} - {\fj{x} \in \Gamma} - \qquad - \infer - {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.m($\overline{e_x}$)} : \fj{C}} - {\begin{array}{c}\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \\ \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{mtype}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}} - \] - \[ - \infer - {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{new C(}\overline{e_x}\fj{)} : \fj{C}} - {\mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{constructor}(\fj{C}) = \overline{\fj{D}}} - \] - \vspace{.3ex} - \[ - \infer - {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}} - {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})} - \] - \vspace{.3ex} - \[ - \infer - {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}} - {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}} - \qquad - \infer - {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}} - {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}} - \] - \end{tcolorbox} + \vspace{-2ex} + \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}} + \] + \pause + \[ + \infer + {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{new C(}\overline{e_x}\fj{)} : \fj{C}} + {\mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{constructor}(\fj{C}) = \overline{\fj{D}}} + \] + \vspace{.3ex} + \[ + \infer + {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}} + {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})} + \] + \vspace{.3ex} + \[ + \infer + {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}} + {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}} + \qquad + \infer + {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}} + {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}} + \] \end{frame} + \placelogotrue \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 @@ -585,6 +600,7 @@ \subsection{Définition du préordre} \begin{frame} + \pause \begin{definition} Soit une \eng{test interface} $\mathfrak{T}$. @@ -596,8 +612,6 @@ \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} @@ -606,10 +620,12 @@ \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 \{\\ @@ -617,8 +633,13 @@ \fjmethod{IList}{zeroList}{}{new IList(0, zeroList())} \} \end{fjlisting} - \[e_i = \fj{intList(0)} \quad\text{et}\quad e_0 = \fj{zeroList()}\] + \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} @@ -641,9 +662,23 @@ \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)\] + \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} @@ -652,14 +687,15 @@ \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] \begin{gather*} \forall \mathcal{A} \quad\forall e,f \quad\forall (h,\mathcal{B})\\ @@ -667,35 +703,30 @@ \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} + \subsection{Conclusion} \begin{frame} - \begin{tcolorbox} - \begin{itemize} + \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 Utilisable autre part + \item Concepts réutilisables \end{itemize} - \end{tcolorbox} - \begin{tcolorbox} - \begin{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{tcolorbox} + \end{exampleblock} \end{frame} \begin{frame} - \LARGE\[\mathfrak{FIN}\] + \Huge\[\mathfrak{FIN}\] \end{frame} \end{document} \ No newline at end of file