Petites correction du diapo
This commit is contained in:
parent
48ba118e8d
commit
671c64867e
GPG Key ID:
DBA23608F23F5A10
@ -221,8 +221,6 @@
|
||||
\tableofcontents[pausesections,hideallsubsections]
|
||||
\end{multicols}
|
||||
\end{frame}
|
||||
|
||||
\section{Introduction}
|
||||
|
||||
\section{Featherweight Java}
|
||||
|
||||
@ -253,8 +251,15 @@
|
||||
\textbf{Class table} \only<3>{$+$ \textbf{Expression} = \textbf{Programme}}
|
||||
\begin{fjlisting}
|
||||
\textbf{class} A \textbf{extends} Object \{...\}\\
|
||||
\textbf{class} B \textbf{extends} Object \{...\}\\
|
||||
\fjclass{Paire}{\fjattr{fst} \fjattr{snd}}{}\\
|
||||
\textbf{class} B \textbf{extends} A \{...\}\\
|
||||
\textbf{class} Paire \textbf{extends} Object \{\\
|
||||
\null\qquad A fst;\\
|
||||
\null\qquad B snd;\\
|
||||
\null\qquad Paire(A fst, B snd)\{...\}\\
|
||||
\null\qquad B getBFst()\{\\
|
||||
\null\qquad\qquad \textbf{return} (B)this.fst;\\
|
||||
\null\qquad\}\\
|
||||
\}\\
|
||||
\pause
|
||||
\fjmain{new Paire(new A(), new B())}
|
||||
\end{fjlisting}
|
||||
@ -279,35 +284,35 @@
|
||||
\begin{frame}
|
||||
\pause
|
||||
\[\infer
|
||||
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}
|
||||
{\mathcal{A},\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})}
|
||||
{\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
|
||||
{\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}}
|
||||
{\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
|
||||
{\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}}}
|
||||
{\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
|
||||
{\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}}
|
||||
{\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
|
||||
{\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}}
|
||||
{\mathcal{A},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
|
||||
{\mathcal{A},\Gamma \Vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}}
|
||||
\]
|
||||
\end{frame}
|
||||
|
||||
@ -381,7 +386,7 @@
|
||||
\subsection{Idée d'une structure}
|
||||
\begin{frame}
|
||||
\begin{itemize}[<+->]
|
||||
\item Besoin de restreindre les contextes
|
||||
\item Spécifier ce que l'on veut tester
|
||||
\item Empêcher au test d'accéder à tout
|
||||
\item Utiliser un mécanisme déjà là
|
||||
\item Inspiration: \eng{header file} en C
|
||||
@ -395,22 +400,12 @@
|
||||
\pause
|
||||
|
||||
Int \{\}\\
|
||||
Int : Int suivant(Int)\\
|
||||
Int : Int add(Int,Int)\\
|
||||
Int <: Number
|
||||
\end{fjlisting}
|
||||
\end{frame}
|
||||
\begin{frame}
|
||||
\begin{fjlisting}
|
||||
Frac(Int numerateur, Int denominateur)\\
|
||||
Frac : Frac inverted()\\
|
||||
Frac : Int floor()\\
|
||||
Frac <: Number\\\null
|
||||
Int : Int add(Int)\\
|
||||
Int <: Number\\
|
||||
\pause
|
||||
|
||||
RichInt \{Int value\}\\
|
||||
RichInt : Int getInt()\\
|
||||
RichInt <: Int
|
||||
Frac (Int numerateur, Int)\\
|
||||
RichInt \{Int value\}
|
||||
\end{fjlisting}
|
||||
\end{frame}
|
||||
\begin{frame}
|
||||
@ -458,6 +453,25 @@
|
||||
\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]}
|
||||
@ -471,25 +485,7 @@
|
||||
{\mathcal{A} \triangleright \left[\fj{C} \subclass \fj{D}\right]}
|
||||
{\fj{C} \subclass_\mathcal{A} \fj{D}}
|
||||
\]
|
||||
\pause
|
||||
\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}}
|
||||
}\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}
|
||||
}
|
||||
\]
|
||||
|
||||
|
||||
\end{frame}
|
||||
|
||||
@ -555,6 +551,13 @@
|
||||
\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
|
||||
@ -562,7 +565,7 @@
|
||||
{\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
|
||||
\vspace{.3ex}
|
||||
\[
|
||||
\infer
|
||||
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{new C(}\overline{e_x}\fj{)} : \fj{C}}
|
||||
@ -571,12 +574,6 @@
|
||||
\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
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user