Petites corrections de fin.
This commit is contained in:
parent
671c64867e
commit
d4eb15cbe0
GPG Key ID:
DBA23608F23F5A10
@ -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}
|
||||
Loading…
x
Reference in New Issue
Block a user