Fin analyse statique (pas bon)

dm.tex

@@ -370,6 +370,7 @@ 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_1\ o\ e_2]^l, l')}
 \]
 \[
+  % TODO : il faudrait évaluer statiquement e.f pour être moins pessimiste
   \inference{RF(l)[x \mapsto \emptyset] \subseteq RF(l')}{RF \vdash ([x := e.f]^l, l')}
 \]
 
@@ -380,7 +381,7 @@ We also define an $init$ function returning the first label of a statement where
   $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$:
+  We perform the static analysis for the program $[S_1 ; S]^5$:
   {
     \footnotesize\[
       \inference
@@ -415,14 +416,14 @@ We also define an $init$ function returning the first label of a statement where
           {
             RF \vdash (S_3 ; S_4, 2)
           } &
-          RF(2) \subseteq RF(l')
+          RF(2) \subseteq RF(5)
         }
         {
-          RF \vdash (S, l')
+          RF \vdash (S, 5)
         }
       }
       {
-        RF \vdash (S_1; S, l')
+        RF \vdash (S_1; S, 5)
       }
     \]
   }
@@ -433,7 +434,16 @@ We also define an $init$ function returning the first label of a statement where
     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')
+    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}