Arbre et système d'équations de l'analyse statique exeple

dm.tex

@@ -2,6 +2,8 @@
 \usepackage{fullpage}
 \usepackage[bookmarks,hidelinks]{hyperref}
 
+\usepackage{lscape}
+
 %% Corrige quelques erreurs de LaTeX2ε
 \usepackage{fixltx2e}
 \usepackage{xspace}
@@ -336,6 +338,8 @@ We also define an $init$ function returning the first label of a statement where
 
 \subsection{Definition}
 
+% TODO : définir l'opérateur \vdash
+
 \[
   \inference{RF(l) \subseteq RF (init(S)) & RF \vdash (S, l) & RF(l) \subseteq RF(l')}{RF \vdash (\<while>\ [b]^l\ \<do>\ S, l')}
 \]
@@ -369,9 +373,69 @@ We also define an $init$ function returning the first label of a statement where
   \inference{RF(l)[x \mapsto \emptyset] \subseteq RF(l')}{RF \vdash ([x := e.f]^l, l')}
 \]
 
-\subsection{Example}
-
-Example.
+\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$:
+  {
+    \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(l')
+        }
+        {
+          RF \vdash (S, l')
+        }
+      }
+      {
+        RF \vdash (S_1; S, l')
+      }
+    \]
+  }
+
+  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(l')
+  \end{align*}
+\end{landscape}
 
 \subsection{Termination}