|
@@ -370,10 +370,12 @@ At each step we can :
|
|
|
|
|
|
This is a pessimistic static analysis. Due to the intersection, we know that $RF(l)$ contains no field that is never defined during the execution (...need some material to do the proof).
|
|
|
|
|
|
-\section{Discussion of the type system and static analysis}
|
|
|
+\section{Discussion on 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 absence of undefined field reading is performed by two different ways by the type system and the static analysis.
|
|
|
+On one hand the type system focuses on the expressions of a program, i.\,e. a statement is well typed if its expressions are well typed.
|
|
|
+On the other hand the static analysis focuses one the commands.
|
|
|
+Therefore, they are complementary.
|
|
|
|
|
|
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.
|