|
@@ -0,0 +1,164 @@
|
|
|
+\subsection{Correctness}
|
|
|
+
|
|
|
+\begin{definition}[Well typed value]
|
|
|
+\label{wt-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(f_i) |- T_i
|
|
|
+\end{align*}
|
|
|
+\end{definition}
|
|
|
+
|
|
|
+\begin{definition}[Well typed state]
|
|
|
+\label{wt-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 => \sigma 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|] \sigma \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|] \sigma = \mathcal{N}|[n|] \sigma$.
|
|
|
+
|
|
|
+$\mathcal{N}|[n|] \sigma \in \mathbb{N}$ so we have $\mathcal{A}|[e|] \sigma \in \mathbb{N}$ which means that $\mathcal{A}|[e|] \sigma |- T$.
|
|
|
+
|
|
|
+\item $e = x$.
|
|
|
+
|
|
|
+By definition $\mathcal{A}|[x|]\sigma = \sigma x$.
|
|
|
+
|
|
|
+$\sigma$ is well typed, so by definition \ref{wt-state}, $\sigma x |- T$.
|
|
|
+So we have $\mathcal{A}|[e|] \sigma |- T$.
|
|
|
+\end{itemize}
|
|
|
+
|
|
|
+Now the inductive cases:
|
|
|
+\begin{itemize}
|
|
|
+\item $e = e_1\ o\ e_2, T = int$.
|
|
|
+
|
|
|
+By definition $\mathcal{A}|[e|]\sigma = \mathcal{A}|[e_1|]\sigma\ o\ \mathcal{A}|[e_2|]\sigma$.
|
|
|
+
|
|
|
+We also know that $\Gamma |- e_1 : int$ and $\Gamma |- e_2 : int$ (by definition of $|-$).
|
|
|
+So by our hypothesis of induction, we have $\mathcal{A}|[e_1|]\sigma |- int$ and $\mathcal{A}|[e_2|]\sigma |- int$.
|
|
|
+
|
|
|
+This means that both $\mathcal{A}|[e_1|]\sigma$ and $\mathcal{A}|[e_2|]\sigma$ are in $\mathbb{N}$,
|
|
|
+$\mathcal{A}|[e_1|]\sigma\ o\ \mathcal{A}|[e_2|]\sigma$ is defined and returns a value in $\mathbb{N}$.
|
|
|
+
|
|
|
+So we have $\mathcal{A}|[e|] \sigma |- T$.
|
|
|
+
|
|
|
+\item $e = e_1.f$.
|
|
|
+
|
|
|
+By definition, $\mathcal{A} |[ e |] \sigma = \mathcal{A}|[e_1|] \sigma f$.
|
|
|
+But is it defined?
|
|
|
+
|
|
|
+By definition of $|-$,
|
|
|
+\[
|
|
|
+ \inference{\Gamma \vdash e_1 : \{f : T\}}{\Gamma \vdash e_1.f : T}
|
|
|
+\]
|
|
|
+
|
|
|
+By our hypothesis of induction, we have $\mathcal{A}|[e_1|]\sigma |- T$.
|
|
|
+So by definition \ref{wt-state} we have :
|
|
|
+\begin{itemize}
|
|
|
+\item $\mathcal{A}|[e_1|]\sigma \in Field \rightharpoonup Value$
|
|
|
+\item $f \in dom(\mathcal{A}|[e_1|]\sigma)$
|
|
|
+\item $\mathcal{A}|[e_1|]\sigma f |- T$
|
|
|
+\end{itemize}
|
|
|
+
|
|
|
+This means that $\mathcal{A} |[ e |] \sigma = \mathcal{A}|[e_1|] \sigma f$ is defined,
|
|
|
+and $\mathcal{A}|[e|] \sigma |- T$.
|
|
|
+
|
|
|
+\item $e = e_1[f \mapsto e_2]$.
|
|
|
+
|
|
|
+By definition, $\mathcal{A} |[ e |] \sigma = \mathcal{A}|[ e_1 |] \sigma [f \mapsto \mathcal{A}|[ e_2 |] \sigma ]$.
|
|
|
+We need to ensure that it is defined, and well typed.
|
|
|
+
|
|
|
+By definition of $|-$,
|
|
|
+\[
|
|
|
+ \inference[append ]{\Gamma \vdash e_2 : T' & \Gamma \vdash e_1 : \{f_1 : T_1; \dots; f_n : T_n\}}{\Gamma \vdash e_1[f \mapsto e_2] : T = \{f : T'; f_1 : T_1; \dots; f_n : T_n\}}
|
|
|
+\]
|
|
|
+
|
|
|
+or
|
|
|
+
|
|
|
+\[
|
|
|
+ \inference[override ]{\Gamma \vdash e_2 : T' & \Gamma \vdash e_1 : \{f_1 : T_1; \dots; f_i : T_i; \dots; f_n : T_n\}}{\Gamma \vdash e_1[f_i \mapsto e_2] : T = \{f_1 : T_1; \dots; f_i : T'; \dots; f_n : T_n\}}
|
|
|
+\]
|
|
|
+
|
|
|
+Let consider the first case (the other case works the same).
|
|
|
+By our hypothesis of induction, we have $\mathcal{A}|[e_1|]\sigma |- \{f_1 : T_1; \dots; f_n : T_n\}$.
|
|
|
+So by definition \ref{wt-state} we have :
|
|
|
+\begin{itemize}
|
|
|
+\item $\mathcal{A}|[e_1|]\sigma \in Field \rightharpoonup Value$
|
|
|
+\item $f \in dom(\mathcal{A}|[e_1|]\sigma)$
|
|
|
+%\item $\mathcal{A}|[e_1|]\sigma f |- T$
|
|
|
+\end{itemize}
|
|
|
+
|
|
|
+We also have (by induction again), $\mathcal{A}|[e_2|]\sigma |- T'$.
|
|
|
+
|
|
|
+So $\mathcal{A} |[ e |] \sigma = \mathcal{A}|[ e_1 |] \sigma [f \mapsto \mathcal{A}|[ e_2 |]]$ is defined,
|
|
|
+and moreover:
|
|
|
+\begin{itemize}
|
|
|
+\item $\mathcal{A}|[e|] \sigma \in Field \rightharpoonup Value$
|
|
|
+\item $\forall f_i, 1 \leq i \leq n, f_i \in dom(\mathcal{A}|[e|]\sigma)$ (because it is in $dom(\mathcal{A}|[e_1|]\sigma)$)
|
|
|
+\item $f \in dom(\mathcal{A}|[e|]\sigma)$ (because it has just been added), and finally,
|
|
|
+\item $\mathcal{A}|[e|]\sigma f |- T'$.
|
|
|
+\end{itemize}
|
|
|
+
|
|
|
+This match the definition of $\mathcal{A}|[e|] \sigma |- T = \{f : T'; f_1 : T_1; \dots; f_n : T_n\}$.
|
|
|
+
|
|
|
+\item $e = \{f_1 = e_1; \dots; f_n = e_n\}$.
|
|
|
+
|
|
|
+By definition,
|
|
|
+\[\mathcal{A} |[e|] \sigma f_i = \mathcal{A}|[e_i|] \sigma\]
|
|
|
+This means that, $\forall f_i, 1 \leq i \leq n$:
|
|
|
+\begin{itemize}
|
|
|
+\item $\mathcal{A}|[e|] \sigma \in Field \rightharpoonup Value$
|
|
|
+\item $f_i \in dom(\mathcal{A}|[e|]\sigma)$
|
|
|
+\item $\mathcal{A}|[e|]\sigma f_i = \mathcal{A}|[e_i|]\sigma |- T_i$ (by induction).
|
|
|
+\end{itemize}
|
|
|
+
|
|
|
+This match the definition for $\mathcal{A}|[e|] \sigma |- T$.
|
|
|
+
|
|
|
+\end{itemize}
|
|
|
+\end{proof}
|
|
|
+
|
|
|
+\begin{lemma}[Well typed programs cannot go wrong]
|
|
|
+\label{wt-state-dgw}
|
|
|
+\[\forall \Gamma P,\quad \Gamma \vdash P \; => \;\forall \sigma |- \Gamma,\; ((P, \sigma) \reduce \sigma' => \sigma' |- \Gamma) \land ((P, \sigma) \reduce (S, \sigma') => \sigma' |- \Gamma)\]
|
|
|
+In particular this also means that:
|
|
|
+\[\forall \Gamma P,\quad \Gamma \vdash P \; => \;\forall \sigma |- \Gamma,\; (P, \sigma) \not\reduce \bot \land (P, \sigma) \not\reduce (S, \bot)\]
|
|
|
+\end{lemma}
|
|
|
+
|
|
|
+\begin{proof}
|
|
|
+This proof can be done by induction on the length of the execution path of the program $P$.
|
|
|
+Let's consider $\Gamma |- P$ and a state $\sigma |- \Gamma$.
|
|
|
+\begin{itemize}
|
|
|
+\item Let's proove that if $(P, \sigma) \rightarrow^0 \sigma' or (P, \sigma) \rightarrow^0 (S, \sigma')$ then $\sigma' |- \Gamma$.
|
|
|
+Because $\sigma = (S, \sigma')$ is impossible, we are in the case where $\sigma = \sigma'$.
|
|
|
+By hypothesis, $\sigma |- \Gamma$, so $\sigma' |- \Gamma$.
|
|
|
+
|
|
|
+\item We name $s$ the intermediate state such as $(P, \sigma) \rightarrow^k s$ for any $k$.
|
|
|
+We have two cases:
|
|
|
+\begin{itemize}
|
|
|
+\item $s = \sigma'' \in State$
|
|
|
+Let consider
|
|
|
+There is no transition from a terminal state, so this is trivially true.
|
|
|
+\item $s = (S, \sigma'')$
|
|
|
+By induciton we know that $\sigma'' |- \Gamma$.
|
|
|
+
|
|
|
+We can proove by induction on the structure of $S$ that
|
|
|
+$(S, \sigma'') \rightarrow \sigma' => \sigma' |- \Gamma$ and
|
|
|
+$(S, \sigma'') \rightarrow (S', \sigma') => \sigma' |- \Gamma$.
|
|
|
+
|
|
|
+Sadely, We don't have time to terminate the proof...
|
|
|
+\end{itemize}
|
|
|
+\end{itemize}
|
|
|
+\end{proof}
|