wip

dm.tex

@@ -301,78 +301,26 @@ 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*}
 
-\begin{landscape}
-  \subsection{Example}
-  Let $S_1 = [x := \{f_1 = 0; f_2 = 42\}]^1$,
-  $S_3 = [y := \{f_1 = x.f_1 + 1\}]^3$,
-  $S_4 = [x := y]^4$,
-  and $S = \<while>\ ([x.f_1 \le 100]^2)\ \<do>\ (S_3 ; S_4)$.
-
-  We perform the static analysis for the program $[S_1 ; S]^5$:
-  {
-    \footnotesize\[
-      \inference
-      {
-        \inference
-        {
-          RF(1)[x \mapsto \{f_1, f_2\}] \subseteq RF(2)
-        }
-        {
-          RF \vdash (S_1, 2)
-        } &
-        \inference
-        {
-          RF(2) \subseteq RF(3) &
-          \inference
-          {
-            \inference
-            {
-              RF(3)[y \mapsto \{f_1\}] \subseteq RF(4)
-            }
-            {
-              RF \vdash (S_3, 4)
-            } &
-            \inference
-            {
-              RF(4)[x \mapsto RF(4)(y)] \subseteq RF(2)
-            }
-            {
-              RF \vdash (S_4, 2)
-            }
-          }
-          {
-            RF \vdash (S_3 ; S_4, 2)
-          } &
-          RF(2) \subseteq RF(5)
-        }
-        {
-          RF \vdash (S, 5)
-        }
-      }
-      {
-        RF \vdash (S_1; S, 5)
-      }
-    \]
-  }
-
-  So the equation system is:
-  \begin{align*}
-    RF(1)[x \mapsto \{f_1, f_2\}] &\subseteq RF(2) \\
-    RF(2) &\subseteq RF(3) \\
-    RF(3)[y \mapsto \{f_1\}] &\subseteq RF(4) \\
-    RF(4)[x \mapsto RF(4)(y)] &\subseteq RF(2) \\
-    RF(2) &\subseteq RF(5)
-  \end{align*}
-
-  % FIXME : notation
-  The minimal solution is:
-  \begin{align*}
-    1 &: \text{no records}\\
-    2 &: x \mapsto \{f_1, f_2\}\\
-    3 &: x \mapsto \{f_1\}\\
-    4 &: x \mapsto \{f_1\}, y \mapsto \{f_1\}\\
-  \end{align*}
-\end{landscape}
+\begin{align*}
+\mathcal{A}
+\end{align*}
+
+\subsection{Example}
+
+Let $S_1 = [x := \{f_1 = 0; f_2 = 42\}]^1$,
+$S_3 = [y := \{f_1 = x.f_1 + 1\}]^3$,
+$S_4 = [x := y]^4$, and
+\[S = \<while>\ ([x.f_1 \le 100]^2)\ \<do>\ (S_3 ; S_4)\].
+
+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) &= 
+\end{align*}
 
 \subsection{Termination}