|
|
@@ -52,20 +52,22 @@
|
|
|
|
|
|
\section{Introduction}
|
|
|
|
|
|
-(...) % 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?
|
|
|
+
|
|
|
+Ensuring that a program do exactly what we want it to do is a hard task.
|
|
|
+Since Rice and his famous theorem, we know that automatically checking that a program respects its specification is impossible (in general).
|
|
|
+It exists some techniques, not to ensure the validity of a program, but at least ensure that a program does not contains a certain type of non-sense.
|
|
|
+Using a type system, and type checking, is one way to ensure that no operation in the program is performed when it has no sense.
|
|
|
+Data-flow analysis for reachability is one other way to ensure that all used objects are defined.
|
|
|
+
|
|
|
+However theses analysis are doomed to be imperfect.
|
|
|
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.
|
|
|
+Such an analysis will always made some assumption that will not be true for every execution.
|
|
|
|
|
|
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.
|
|
|
+Then, we define a type system and a static analysis for this language.
|
|
|
+
|
|
|
+We will see that both of them have different flows. Each complement the other, and none of them are perfect.
|
|
|
|
|
|
\section{Small-step Semantic}
|
|
|
|
Thibaut Marty