Deux exemples pour l'analyse statique vs le système de type

dm.tex

@@ -460,4 +460,21 @@ assuring the termination of the analysis.
 
 This is a pessimistic static analysis.
 
+\section{Discussion of the type system and static analysis}
+
+% The static analysis and the type system are complementary to prove
+% is pessimistic by nature, so it will reject some programs which are legals.
+
+The static analysis of the program $x := \{f = 1\} ; y := 3 + x$ works because there is no undefined field reading.
+The variable $x$ contains one field $f$, and no other fields are read.
+However, the type system rejects this program.
+Indeed, the expression $3 + x$ is not well typed as the type of $x$ is $\{f:int\}$, not $int$.
+
+The program $x := \{\}; \<if>\ b\ \<then>\ x.f := 1\ \<else>\ \<skip>; y := x.f$ is well typed because the type $\{\}$ is a sub-type of the type $\{f:int\}$.
+However, its static analysis fails.
+The static analysis will take the worst case of the two branches of the \<if> statement, that is the \<else> branch when $x$ doesn't get the extra field $f$.
+Thus, the last statement, $y := x.f$, tries to reach the undefined (according to the analysis) field $f$.
+
+\subsection{Extension of the static analysis}
+
 \end{document}