|
@@ -38,42 +38,54 @@
|
|
|
\begin{document}
|
|
|
|
|
|
\author{Timoth\'ee Haudebourg \and Thibaut Marty}
|
|
|
-\title{PAS}
|
|
|
+\title{Homework PAS/SDL}
|
|
|
+\date{November 18, 2016}
|
|
|
|
|
|
\maketitle
|
|
|
|
|
|
\section{Exercise 1}
|
|
|
|
|
|
-\subsection{Denotational Semantic for expressions}
|
|
|
+\subsection{Domains}
|
|
|
|
|
|
-% $State = Var -> ((Field \rightharpoonup Value) \cup Value)$
|
|
|
+The $State$ domain of evaluation is defined as:
|
|
|
+\[State = (Var \rightharpoonup Value) \cup \bot\]
|
|
|
+Where $Var$ is the set of variables, and $Value$ the set of possible values.
|
|
|
+We use $\bot$ to represent the error state.
|
|
|
+In our model, a record is represented as a partial application $Field \rightharpoonup Value$.
|
|
|
+This means that a record field can contains a record itself.
|
|
|
+To do so, we define the set of value as:
|
|
|
\begin{align*}
|
|
|
- Value &= int \cup (Field \rightharpoonup Value) \\
|
|
|
- State &= Var -> Value
|
|
|
+ Value &= \bigcup_{i\in\mathbb{N}} Value_i \\
|
|
|
+ Value_n &= \mathbb{N} \cup (Field \rightharpoonup Value_{n+1}) \\
|
|
|
\end{align*}
|
|
|
|
|
|
+\subsection{Denotational Semantic for expressions}
|
|
|
+
|
|
|
+We define $\mathcal{A}$ the denotational semantics of arithmetic expressions as:
|
|
|
+
|
|
|
+\[ \mathcal{A}|[ \bullet |] : AExpr \rightarrow State \rightarrow (Value \cup \bot) \]
|
|
|
+where
|
|
|
\begin{align*}
|
|
|
- \mathcal{A} |[ n |] \sigma &= \mathcal{N} |[n|] \sigma \\
|
|
|
+ \mathcal{A} |[ n |] \sigma &= \mathcal{N} |[n|] \\
|
|
|
\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 ]\\
|
|
|
+ \mathcal{A} |[ \{f_1 = e_1 ; \dots ; f_n = e_n\} |] \sigma f_i &= \mathcal{A}|[ e_i |] \sigma \\
|
|
|
\end{align*}
|
|
|
|
|
|
-For the undefined cases, for example when we try to add records, we also note $\mathcal{A}|[e|] \sigma = \bot$.
|
|
|
+For the undefined cases, for example when we try to add two records, we also note $\mathcal{A}|[e|] \sigma = \bot$.
|
|
|
+In the rest of this homwork, we suppose $\mathcal{B}|[ \bullet |]$ the denotational semantic for booleans expressions already defined.
|
|
|
|
|
|
% TODO fin de la question : explications
|
|
|
|
|
|
\subsection{Structural Operational Semantic for commands}
|
|
|
|
|
|
-We note $\mathcal{B}$ the denotational semantic of booleans expressions.
|
|
|
+We define $->$ the structural operational semantics for commands as:
|
|
|
+
|
|
|
+\[ -> : (Statement \times State) \times ((Statement \times State) \cup State) \]
|
|
|
|
|
|
+\subsubsection{Regular execution}
|
|
|
For all $\sigma \neq \bot$:
|
|
|
\[
|
|
|
\inference{}{(skip, \sigma) -> \sigma}
|
|
@@ -100,17 +112,36 @@ For all $\sigma \neq \bot$:
|
|
|
\inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> (S_2, \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{ff}}
|
|
|
\]
|
|
|
|
|
|
-Error cases: % TODO
|
|
|
+\subsubsection{Error handling}
|
|
|
+An error can occurs when one tries to add (or compare) records.
|
|
|
+In that case, according to our definition of arithmetic expressions, $\mathcal{A}|[e|] \sigma$ (or $\mathcal{B}|[b|]$) will returns $\bot$.
|
|
|
+From this point, the execution of the program makes no sense, and we will return the error state.
|
|
|
|
|
|
\[
|
|
|
- \inference{}{(S, \bot) -> \bot}
|
|
|
+ \inference{}{(x := a, \sigma) -> \bot}{\text{if }\mathcal{A}|[a|] \sigma = \bot}
|
|
|
\]
|
|
|
\[
|
|
|
- \inference{}{(x := a, \sigma) -> \bot}{\text{if }\mathcal{A}|[a|] \sigma = \bot}
|
|
|
+ \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> \bot}{\text{if } \mathcal{B}|[b|] \sigma = \bot}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> \bot}{\text{if } \mathcal{B}|[b|] \sigma = \bot}
|
|
|
+\]
|
|
|
+
|
|
|
+To ensure that the error can make it through the end, we also add the error propagation rule:
|
|
|
+
|
|
|
+\[
|
|
|
+ \inference{}{(S, \bot) -> \bot}
|
|
|
\]
|
|
|
|
|
|
\section{Type system}
|
|
|
|
|
|
+We suppose now that every variable in the program is declared with a type satisfying the following syntax:
|
|
|
+\[
|
|
|
+ t\quad::=\quad\text{int }|\ \{f_1 : t_1;\ \dots\ ; f_n : t_n\}
|
|
|
+\]
|
|
|
+
|
|
|
+We note $\Gamma \vdash S$ the type judgment for our language, defined by the following typing rules:
|
|
|
+
|
|
|
\[
|
|
|
\inference{}{\Gamma \vdash n : int}
|
|
|
\]
|