Ajout de pauses
This commit is contained in:
parent
741155f474
commit
9c00e37561
GPG Key ID:
DBA23608F23F5A10
@ -24,9 +24,9 @@
|
||||
\usepackage{xparse}
|
||||
\usepackage{cprotect}
|
||||
\usepackage{xpatch}
|
||||
\usepackage{enumitem}
|
||||
\usepackage{amsfonts}
|
||||
\usepackage{mathtools}
|
||||
\usepackage{setspace}
|
||||
|
||||
\usepackage{geometry}
|
||||
\usepackage{subcaption}
|
||||
@ -198,6 +198,8 @@
|
||||
\renewcommand*\beamer@checkframetitle{\global\let\beamer@frametitle\relax\@ifnextchar\bgroup\beamer@inlineframetitle{}}
|
||||
\makeatother
|
||||
|
||||
\setbeamertemplate{itemizeitem}{\scriptsize$\diamond$}
|
||||
|
||||
\author{Samy Avrillon}
|
||||
\title{Définition d'un préordre sur les programmes Featherweight Java}
|
||||
\subtitle{Notes sur mon stage au LACL}
|
||||
@ -227,20 +229,25 @@
|
||||
\begin{center}
|
||||
\refstepcounter{rule}
|
||||
\begin{tabular}{rll}
|
||||
$e$ $:=$ & \fj{x} & \qquad \textrm{\textsc{E-Var}} \\
|
||||
$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()}\]
|
||||
|
||||
\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} Object \{...\}\\
|
||||
@ -254,11 +261,12 @@
|
||||
\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}
|
||||
\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) expr} \rightarrow \fj{expr}$ (\textsc{R-Cast})
|
||||
\end{itemize}
|
||||
\end{frame}
|
||||
|
||||
\subsection{Son typage}
|
||||
@ -268,166 +276,79 @@
|
||||
\[\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$.f} : \fj{C}}
|
||||
{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})}
|
||||
\]\[
|
||||
\]
|
||||
\vspace{.2ex}
|
||||
\[
|
||||
\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}}
|
||||
\]\[
|
||||
{\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{.2ex}
|
||||
\[
|
||||
\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{.2ex}
|
||||
\[
|
||||
\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}
|
||||
|
||||
\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}
|
||||
\begin{exampleblock}{Sens}
|
||||
\pause
|
||||
\begin{itemize}[<+->]
|
||||
\item Deux programmes «font la même chose»
|
||||
\item Assez stricte
|
||||
\item Assez large
|
||||
\end{itemize}
|
||||
\end{exampleblock}
|
||||
\pause
|
||||
\begin{exampleblock}{Utilisations}
|
||||
\pause
|
||||
\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}
|
||||
\[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$
|
||||
Contexte : $C$
|
||||
\vspace{2ex}\pause
|
||||
|
||||
Contextualisation : $C\bracket{P}$
|
||||
\vspace{2ex}\pause
|
||||
|
||||
Préordre : $P \prec Q \iff \forall C\quad C\bracket{P} \implies C\bracket{Q}$
|
||||
\vspace{2ex}\pause
|
||||
|
||||
Équivalence : $P \equiv Q \iff P \prec Q \land Q \prec P$
|
||||
\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}
|
||||
\pause
|
||||
\begin{multicols}{2}
|
||||
\null\vfill
|
||||
\begin{fjlisting}[width=.49\textwidth]
|
||||
@ -437,6 +358,7 @@
|
||||
\end{fjlisting}
|
||||
\vfill\null
|
||||
\columnbreak
|
||||
\pause
|
||||
\begin{fjlisting}[width=.49\textwidth]
|
||||
\textbf{class} XXX \textbf{extends} XXX \{\\
|
||||
\}\\
|
||||
@ -447,11 +369,12 @@
|
||||
\end{fjlisting}
|
||||
\end{multicols}
|
||||
\end{center}
|
||||
\pause
|
||||
\[\fj{new Main().main()}\rightarrow \fj{expr}\]
|
||||
\end{frame}
|
||||
\subsection{Idées d'une structure}
|
||||
\subsection{Idée d'une structure}
|
||||
\begin{frame}
|
||||
\begin{itemize}
|
||||
\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à
|
||||
@ -463,11 +386,12 @@
|
||||
\begin{frame}
|
||||
\begin{fjlisting}
|
||||
Number \{\}\\\null
|
||||
\pause
|
||||
|
||||
Int \{\}\\
|
||||
Int : Int suivant(Int)\\
|
||||
Int : Int add(Int,Int)\\
|
||||
Int <: Number\\\null
|
||||
Int <: Number
|
||||
\end{fjlisting}
|
||||
\end{frame}
|
||||
\begin{frame}
|
||||
@ -476,6 +400,7 @@
|
||||
Frac : Frac inverted()\\
|
||||
Frac : Int floor()\\
|
||||
Frac <: Number\\\null
|
||||
\pause
|
||||
|
||||
RichInt \{Int value\}\\
|
||||
RichInt : Int getInt()\\
|
||||
@ -483,14 +408,19 @@
|
||||
\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{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}
|
||||
\pause
|
||||
\begin{theorem}
|
||||
\pause
|
||||
\begin{itemize}
|
||||
\item $\mathcal{A} \triangleright \mathfrak{T}$
|
||||
\item $\mathcal{B} \OKin \mathfrak{T}$
|
||||
@ -505,28 +435,24 @@
|
||||
|
||||
\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}
|
||||
\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}
|
||||
\begin{exampleblock}{}
|
||||
\[
|
||||
\infer
|
||||
{\mathcal{A} \triangleright \left[\fj{C : G m($\overline{\texttt{F}}$)}\right]}
|
||||
{
|
||||
@ -534,16 +460,19 @@
|
||||
\quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}}
|
||||
\quad \fj{H}\subclass_\mathcal{A}\fj{G}
|
||||
}
|
||||
\end{exampleblock}
|
||||
\begin{exampleblock}{}
|
||||
\qquad
|
||||
\infer
|
||||
{\mathcal{A} \triangleright \left[\fj{C} \subclass \fj{D}\right]}
|
||||
{\fj{C} \subclass_\mathcal{A} \fj{D}}
|
||||
\]
|
||||
\vspace{2ex}
|
||||
\[
|
||||
\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}{}
|
||||
}\qquad
|
||||
\infer
|
||||
{\mathcal{A} \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]}
|
||||
{\begin{array}{l}
|
||||
@ -553,100 +482,90 @@
|
||||
\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}
|
||||
\begin{frame}[plain]
|
||||
\ttfamily
|
||||
\vspace{-3ex}
|
||||
\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}
|
||||
\[
|
||||
\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}
|
||||
|
||||
\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}
|
||||
\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}
|
||||
\end{frame}
|
||||
\subsection{Théorème de cohérence}
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user