|
@@ -16,7 +16,7 @@
|
|
|
\usepackage{lmodern}
|
|
|
|
|
|
%% Pour écrire du français
|
|
|
-\usepackage[frenchb]{babel}
|
|
|
+% \usepackage[frenchb]{babel}
|
|
|
|
|
|
%% Pour composer des mathématiques
|
|
|
\usepackage{mathtools}
|
|
@@ -30,17 +30,84 @@
|
|
|
|
|
|
%% Commandes du paquet semantic : langage While
|
|
|
\reservestyle{\command}{\textbf}
|
|
|
-\command{skip,while,do,if,then,else,not,and,or,true,false}
|
|
|
+\command{skip,while,do,if,then,else,not,and,or,true,false,int}
|
|
|
%% -> Utiliser \<begin> Pour styliser le mot-clé
|
|
|
|
|
|
\newcommand{\reduce}{\rightarrow^{*}}
|
|
|
|
|
|
\begin{document}
|
|
|
|
|
|
-\author{Timothée Haudebourg \and Thibaut Marty}
|
|
|
+\author{Timoth\'ee Haudebourg \and Thibaut Marty}
|
|
|
\title{PAS}
|
|
|
|
|
|
\maketitle
|
|
|
|
|
|
+\section{Exercise 1}
|
|
|
+
|
|
|
+\subsection{Denotational semantic for expressions}
|
|
|
+
|
|
|
+% $State = Var -> ((Field \rightharpoonup Value) \cup Value)$
|
|
|
+\begin{align*}
|
|
|
+ Value &= int \cup (Field \rightharpoonup Value) \\
|
|
|
+ State &= Var -> Value
|
|
|
+\end{align*}
|
|
|
+
|
|
|
+\begin{align*}
|
|
|
+ \mathcal{A} |[ n |] \sigma &= \mathcal{N} |[n|] \sigma \\
|
|
|
+ \mathcal{A} |[ x |] \sigma &= \sigma x \\
|
|
|
+ \mathcal{A} |[ e_1\ o\ e_2 |] \sigma &= \mathcal{A} |[ e_1 |] \sigma\ \bar{o}\ \mathcal{A} |[ e_2 |] \sigma \\
|
|
|
+ \mathcal{A} |[ {f_1 = e_1 ; \dots ; f_n = e_n} |] \sigma f &=
|
|
|
+ \begin{cases}
|
|
|
+ \mathcal{A}|[ e_1 |] \sigma \text{ if } f = f_1 \\
|
|
|
+ \hspace{1cm} \vdots \\
|
|
|
+ \mathcal{A}|[ e_n |] \sigma \text{ if } f = f_n
|
|
|
+ \end{cases} \\
|
|
|
+ \mathcal{A} |[ e.f |] \sigma &= \mathcal{A}|[e|] \sigma f\\
|
|
|
+ \mathcal{A} |[ e_1{f \mapsto e_2} |] \sigma f &= \mathcal{A}|[ e_1 |] \sigma [f \mapsto \mathcal{A}|[ e_2 |] \sigma ]\\
|
|
|
+\end{align*}
|
|
|
+
|
|
|
+For the undefined cases, for example when we try to add records, we also note $\mathcal{A}|[e|] = \bot$.
|
|
|
+
|
|
|
+\subsection{Structural Operational Semantic for commands}
|
|
|
+
|
|
|
+We note $\mathcal{B}$ the denotational semantic of booleans expressions.
|
|
|
+
|
|
|
+For all $\sigma \neq \bot$:
|
|
|
+\[
|
|
|
+ \inference{}{(skip, \sigma) -> \sigma}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{}{(x := a, \sigma) -> \sigma[x \mapsto \mathcal{A}|[a|] \sigma]}{\mathcal{A}|[a|] \sigma \neq \bot}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{(S_1, \sigma) -> (S_1', \sigma')}{(S_1 ; S_2, \sigma) -> (S_1' ; S_2, \sigma')}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{(S_1, \sigma) -> \sigma'}{(S_1 ; S_2, \sigma) -> (S_2, \sigma')}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> (S ; \<while>\ b\ \<do> S, \sigma')}{\text{if } \mathcal{B}|[b|] = \text{tt}}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> \sigma)}{\text{if } \mathcal{B}|[b|] = \text{ff}}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> (S_1, \sigma)}{\text{if } \mathcal{B}|[b|] = \text{tt}}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> (S_2, \sigma)}{\text{if } \mathcal{B}|[b|] = \text{ff}}
|
|
|
+\]
|
|
|
+
|
|
|
+Error cases: % TODO
|
|
|
+
|
|
|
+\[
|
|
|
+ \inference{}{(S, \bot) -> \bot}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{}{(x := a, \sigma) -> \bot}{\mathcal{A}|[a|] \sigma = \bot}
|
|
|
+\]
|
|
|
+
|
|
|
+\subsection{Système de type}
|
|
|
+
|
|
|
|
|
|
\end{document}
|