|
|
@@ -52,7 +52,20 @@
|
|
|
|
|
|
\section{Introduction}
|
|
|
|
|
|
-% TODO
|
|
|
+(...) % TODO
|
|
|
+
|
|
|
+Some programs of a language can be incorrect, that is programs which their execution will make no sense.
|
|
|
+% example?
|
|
|
+There exists some \emph{static} analysis of a program to detect if it is correct or not.
|
|
|
+Theses analysis can not be perfect.
|
|
|
+% theorem?
|
|
|
+That means they will either reject or accept programs even if they are respectively correct or not.
|
|
|
+Here, we do not want analysis to accept incorrect programs.
|
|
|
+Hence, analysis must be correct, but will not be complete.
|
|
|
+
|
|
|
+In this work, we first define a semantic for a small imperative language, \emph{While}.
|
|
|
+This semantic must handle errors, i.\,e. incorrect programs.
|
|
|
+Then, we define a type system and a static analysis for the language.
|
|
|
|
|
|
\section{Small-step Semantic}
|
|
|
|
Thibaut Marty