Mysaa/stage-2022
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Petites modifications

Browse Source
This commit is contained in:
Mysaa 2022-08-27 19:42:47 +02:00
parent ab247d4e36
commit 48ba118e8d
Signed by: Mysaa
GPG Key ID: DBA23608F23F5A10
1 changed files with 18 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
DiaposSoutenance.tex
View File

@ -245,6 +245,7 @@
\end{center}
\pause
\[\fj{new Paire((D)new B().get(), new C(new A())).snd.apply()}\]
\pdfpcnote{Distinction ouvert/ferme}
\end{frame}
\subsection{Ses structures}
\begin{frame}
@ -267,8 +268,10 @@
\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})
\item $\fj{(C) new D(...)} \rightarrow \fj{new D(...)}$ si $\fj{D}\subclass\fj{C}$ (\textsc{R-Cast})
\item $e \rightarrow^* f \implies h\bracket{e} \rightarrow^* h\bracket{f}$
\end{itemize}
\end{frame}
\subsection{Son typage}
@ -339,7 +342,7 @@
Contextualisation : $C\bracket{P}$
\vspace{2ex}\pause
Préordre : $P \prec Q \iff \forall C\quad C\bracket{P} \implies C\bracket{Q}$
Préordre : $P \prec Q \iff \forall C\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$
@ -357,7 +360,7 @@
\begin{fjlisting}[width=.49\textwidth]
\textbf{class} XXX \textbf{extends} XXX \{\}\\
\vdots\\
\fjmain{expression}
\fjmain{expr}
\end{fjlisting}
\vfill\null
\columnbreak
@ -468,6 +471,7 @@
{\mathcal{A} \triangleright \left[\fj{C} \subclass \fj{D}\right]}
{\fj{C} \subclass_\mathcal{A} \fj{D}}
\]
\pause
\vspace{2ex}
\[
\infer
@ -683,7 +687,17 @@
\subsection{Redéfinition des préordres}
\begin{frame}
\[\mathcal{A}\pprec\mathcal{B} \ssi \forall e \quad (\mathcal{A},e) \pprec (\mathcal{B},e)\]
\[\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}
\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}\]
\end{frame}
\subsection{Propriétés}
\begin{frame}