wip

dm.tex

@@ -30,6 +30,9 @@
 \usepackage{stmaryrd}
 \usepackage{semantic}
 
+\newtheorem{lemma}{Lemma}
+\newtheorem{definition}{Definition}
+
 %% Commandes du paquet semantic : langage While
 \reservestyle{\command}{\textbf}
 \command{skip,while,do,if,then,else,not,and,or,true,false,int}
@@ -86,7 +89,7 @@ In the rest of this homwork, we suppose $\mathcal{B}|[ \bullet |]$ the denotatio
 
 We define $->$ the structural operational semantics for commands as:
 
-\[ -> \subseteq (Statement \times State) \times ((Statement \times State) \cup State) \]
+\[ ->\ \subseteq (Statement \times State) \times ((Statement \times State) \cup State) \]
 
 \subsubsection{Regular execution}
 For all $\sigma \neq \bot$:
@@ -264,7 +267,50 @@ Note: for the equality test, the rule works for \<int> as well as for records.
 
 \subsection{Correctness}
 
+\begin{definition}[Well typed value]
+A value $v \in Value$ is well typed regarding to a type $T$ (noted $v |- T$) when :
+\begin{align*}
+v |- int &=> v \in \mathbb{N} \\
+v |- \{f_1 : T_1, \dots, f_n : T_n\} &=> v \in Field \rightharpoonup Value\text{ and }\forall f_i, f_i \in dom(v) \land v(t_i) |- T_i
+\end{align*}
+\end{definition}
+
+\begin{definition}[Well typed state]
+A state $\sigma \in State$, $\sigma \neq \bot$ is well typed with regards to a type system $\Gamma$ (noted $\sigma |- \Gamma$) when
+\[\forall x \in Var,\ \Gamma |- x : T => x |- T\]
+\end{definition}
+
+\begin{lemma}[Well typed expressions cannot go wrong]
+$\forall e \in AExpr, \sigma \in State, \Gamma$ such as $\sigma |- \Gamma$ :
+\[\Gamma |- e : T => \mathcal{A}|[e|] \sigma |- T\]
+In particular, $\mathcal{A}|[e|] \neq \bot$.
+\end{lemma}
+
+\begin{proof}
+We demonstrate this property by induction on the structure of the expression $e$.
+First let assume that $\Gamma |- e : T$.
+We can eliminates all trivial cases in contradiction with this assumption (for example when $e = 1 + 1$ and $T = \{\}$).
+Here are the other base cases:
+\begin{itemize}
+\item $e = n, T = int$.
+
+$\mathcal{A}|[e|] = \mathcal{N}|[n|]$.
+
+$\mathcal{N}|[n|] \in \mathbb{N}$ so we have $\mathcal{A}|[e|] \in \mathbb{N}$ which means that $\mathcal{A}|[e|] \sigma |- T$.
+
+\item $e = n, T = int$.
+\item $e = x$.
+\item $e = e_1 o e_2, T = int$.
+\item $e = e_1.f$.
+\item $e = e_1[f \mapto e_2]$.
+\item $e = \{f_1 = e_1; \dots; f_n = e_n\}$.
+
+\end{itemize}
+\end{proof}
+
+\begin{lemma}[Well programs cannot go wrong]
 \[\forall \Gamma P,\quad \Gamma \vdash P \; => \;\forall \sigma,\; (P, \sigma) \not\reduce \bot\]
+\end{lemma}
 
 \begin{proof}
 By induction on the path of $\reduce$, and by induction on the structure/type of the statement at each step of the path.