proof and static analysis (new)

dm.tex

@@ -265,56 +265,8 @@ Note: for the equality test, the rule works for \<int> as well as for records.
   S,S_1,S_2 \in Statement
 \]
 
-\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.
-\end{proof}
+\input{sections/correctness.tex}
 
 \section{Static analysis}
 
@@ -326,50 +278,25 @@ Our static analysis is incarnated by the function $RF$ (\enquote{Reachable Field
 where $Lab$ is the set of labels.
 One unique label is assigned to each instruction.
 For the sake of simplicity, we note $[I]^l$ the instruction of label $l$.
-We also define an $init$ function returning the first label of a statement where:
-
-\begin{align*}
-	&init([\<skip>]^l) = l\\
-	&init([x := a]^l) = l\\
-	&init(S_1;S_2) = init(S_1)\\
-	&init(\<while>\ [b]^l\ \<do>\ S) = l \\
-	&init(\<if>\ [b]^l\ \<then>\ S_1\ \<else>\ S_2) = l
-\end{align*}
 
 \subsection{Definition}
 
-\[
-  \inference{RF(l) \subseteq RF (init(S)) & RF \vdash (S, l) & RF(l) \subseteq RF(l')}{RF \vdash (\<while>\ [b]^l\ \<do>\ S, l')}
-\]
-\[
-  \inference{RF(l) \subseteq RF(init(S_1)) & RF \vdash (S_1, l') \\ RF(l) \subseteq RF(init(S_2)) & RF \vdash (S_2, l')}{RF \vdash (\<if>\ [b]^l\ \<then>\ S_1\ \<else>\ S_2, l')}
-\]
-\[
-  \inference{RF(l) \subseteq RF(l')}{RF \vdash ([skip]^l, l')}
-\]
-\[
-  \inference{RF \vdash (S_1, init(S_2)) & RF \vdash (S_2, l')}{RF \vdash (S_1 ; S_2, l')}
-\]
-\[
-  \inference{RF(l)[x \mapsto \{f_1, \dots, f_n\}] \subseteq RF(l')}{RF \vdash ([x := \{f_1 = e_1 ; \dots ; f_n = e_n\}]^l, l')}
-\]
-\[
-  % TODO : il faudrait évaluer statiquement e_1 pour être moins pessimiste
-  \inference{RF(l)[x \mapsto \{f\}] \subseteq RF(l')}{RF \vdash ([x := e_1[f \mapsto e_2]]^l, l')}
-\]
-% autres affectations
-\[
-  \inference{RF(l)[x \mapsto \emptyset] \subseteq RF(l')}{RF \vdash ([x := n]^l, l')}
-\]
-\[
-  \inference{RF(l)[x \mapsto RF(l)(y)] \subseteq RF(l')}{RF \vdash ([x := y]^l, l')}
-\]
-\[
-  \inference{RF(l)[x \mapsto \emptyset] \subseteq RF(l')}{RF \vdash ([x := e_1\ o\ e_2]^l, l')}
-\]
-\[
-  \inference{RF(l)[x \mapsto \emptyset] \subseteq RF(l')}{RF \vdash ([x := e.f]^l, l')}
-\]
+Here is the definition of the static analysis.
+We suppose that we dispose of the control flow graph $flow(P)$ of the program.
+
+\[RF(l) = \bigcap_{(l', l) \in flow(P)} RF_{out}(l')\]
+
+Where $RF_{out}$ is defined by:
+
+\begin{align*}
+RF_{out}([\<skip>]^l) &= RF(l) \\
+RF_{out}([b]^l) &= RF(l)\quad(b \in BExp)\\
+RF_{out}([x := n]^l) &= RF(l)[x \mapsto \{\}]\quad(n \in \mathbb{N})\\
+RF_{out}([x := y]^l) &= RF(l)[x \mapsto (RF(l) y)]\quad(y \in Var)\\
+RF_{out}([x := \{f_1 = e_1; \dots; f_n = e_n\}]^l) &= RF(l)[x \mapsto \{f_1, \dots, f_n\}]\\
+RF_{out}([x := e_1[f \mapsto e_2]]^l) &= RF(l)[x \mapsto \{f\}] \\
+RF_{out}([x := e.f]^l) &= RF(l)[x \mapsto \{\}]
+\end{align*}
 
 \subsection{Example}
 

sections/correctness.tex

@@ -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}