static analysis

dm.tex

@@ -294,15 +294,19 @@ 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 \{\}]
+RF_{out}([x := e]^l) &= RF(l)[x \mapsto \mathcal{A}^\#|[e|] RF(l)]
 \end{align*}
 
+Where $\mathcal{A}^\#$ is defined by:
+
+\[\mathcal{A}^\#|[\bullet|] : AExpr -> (Var -> \mathcal{P}(Field)) -> \mathcal{P}(Field)\]
+
 \begin{align*}
-\mathcal{A}
+\mathcal{A}^\#|[n|] \sigma &= \emptyset \\
+\mathcal{A}^\#|[x|] \sigma &= \sigma x \\
+\mathcal{A}^\#|[\{f_1 = e_1; \dots; f_n = e_n\}|] \sigma &= \{f_1; \dots; f_n\} \\
+\mathcal{A}^\#|[e_1[f \mapsto e_2]|] \sigma &= \mathcal{A}^\#|[e_1|] \sigma \cup \{f\} \\
+\mathcal{A}^\#|[e.f|] \sigma &= \emptyset
 \end{align*}
 
 \subsection{Example}
@@ -316,20 +320,42 @@ We perform the static analysis for the program $[S_1 ; S]^5$:
 Let's begin with the initial state:
 
 \begin{align*}
-RF(1) &= \{\}
-RF(2) &= RF(1) \cap RF(4)
-RF(3) &= RF(2)[y \mapsto \{f_1\}]
-RF(4) &= 
+RF(1) &= \emptyset \\
+RF(2) &= RF_{out}(1) \cap RF(4)_{out} \\
+RF(3) &= RF(2)_{out} \\
+RF(4) &= RF(3)_{out} \\
+RF(5) &= RF(2)_{out}
+\end{align*}
+
+\begin{align*}
+RF_{out}(1) &= RF(1)[x \mapsto \{f_1, f_2\}] \\
+RF_{out}(2) &= RF(2) \\
+RF_{out}(3) &= RF(3)[y \mapsto \{f_1\}] \\
+RF_{out}(4) &= RF(4)[x \mapsto \{f_1\}]
+\end{align*}
+
+Now we can solve those equations and found:
+
+\begin{align*}
+RF(1) &= \emptyset \\
+RF(2) &= RF(1)[x \mapsto \{f_1, f_2\}] \cap RF(4)[x \mapsto \{f_1\}] = \{x \mapsto \{f_1\}\} \\
+RF(3) &= RF(2) = \{x \mapsto \{f_1\}\} \\
+RF(4) &= RF(3)[y \mapsto \{f_1\}] = \{x \mapsto \{f_1\}, y \mapsto \{f_1\}\} \\
+RF(5) &= RF(2) = \{x \mapsto \{f_1\}\}
 \end{align*}
 
 \subsection{Termination}
 
-In each premise of each rule, the size of the statement is \emph{strictly} decreasing,
-assuring the termination of the analysis.
+We can design an algorithm to solve this equation system under the hypothesis that there is no label $l$ such as $(l, l) \in flow(P)$.
+At each step we can :
+\begin{itemize}
+\item Rewrite a $RF(l)$ as $\bigcap_{(l', l) \in flow(P)} RF_{out}(l')$, where $RF_{out}(l')$ can be simplified into a term that does not contains $RF(l)$ (because $(l, l) \not\in flow(P)$).
+\item Because a program contains a finite number of instructions, it exists a time when no $RF(l)$ is left. The system is solved.
+\end{itemize}
 
 \subsection{Safety}
 
-This is a pessimistic static analysis.
+This is a pessimistic static analysis. Due to the intersection, we know that $RF(l)$ contains no field that is never defined during the execution (...need some material to do the proof).
 
 \section{Discussion of the type system and static analysis}