Analyse statique

dm.tex

@@ -56,7 +56,7 @@
   \mathcal{A} |[ n |] \sigma &= \mathcal{N} |[n|] \sigma \\
   \mathcal{A} |[ x |] \sigma &= \sigma x \\
   \mathcal{A} |[ e_1\ o\ e_2 |] \sigma &= \mathcal{A} |[ e_1 |] \sigma\ \bar{o}\ \mathcal{A} |[ e_2 |] \sigma \\
-  \mathcal{A} |[ {f_1 = e_1 ; \dots ; f_n = e_n} |] \sigma f &=
+  \mathcal{A} |[ \{f_1 = e_1 ; \dots ; f_n = e_n\} |] \sigma f &=
     \begin{cases}
       \mathcal{A}|[ e_1 |] \sigma \text{ if } f = f_1 \\
       \hspace{1cm} \vdots \\
@@ -109,7 +109,47 @@ Error cases: % TODO
   \inference{}{(x := a, \sigma) -> \bot}{\text{if }\mathcal{A}|[a|] \sigma = \bot}
 \]
 
-\subsection{Type system}
+\section{Type system}
 
+% TODO
+
+\section{Static analysis}
+
+$RF : Lab -> Var -> \mathcal{P}(Field)$
+
+% TODO : définir init
+
+\[
+  \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')}
+\]
 
 \end{document}