|
@@ -54,9 +54,9 @@
|
|
|
|
|
|
Some programs of a language can be incorrect, that is programs which their execution will make no sense.
|
|
|
|
|
|
-Ensuring that a program do exactly what we want it to do is a hard task.
|
|
|
+Ensuring that a program does 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.
|
|
|
+There 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 nonsense.
|
|
|
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.
|
|
|
|
|
@@ -69,7 +69,7 @@ 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}
|
|
|
+\section{Small-step Semantics}
|
|
|
|
|
|
\subsection{Domains}
|
|
|
|
|
@@ -104,7 +104,7 @@ where
|
|
|
\end{align*}
|
|
|
|
|
|
For the undefined cases, for example when we try to add two records, we also note $\mathcal{A}|[e|] \sigma = \bot$.
|
|
|
-In the rest of this homwork, we suppose $\mathcal{B}|[ \bullet |]$ the denotational semantic for booleans expressions already defined.
|
|
|
+In the rest of this work, we suppose $\mathcal{B}|[ \bullet |]$ the denotational semantic for booleans expressions already defined.
|
|
|
|
|
|
\subsection{Structural Operational Semantic for commands}
|
|
|
|
|
@@ -205,9 +205,9 @@ Field lookup
|
|
|
\inference{\Gamma \vdash e : \{f : T\}}{\Gamma \vdash e.f : T}
|
|
|
\]
|
|
|
|
|
|
-As is, the last rule can seems too restrictive.
|
|
|
+As is, the last rule can seem too restrictive.
|
|
|
Indeed, an expression $e$ does not have to match \emph{exactly} the type $\{f : T\}$ to provide the field $f$.
|
|
|
-It can contains some other fields.
|
|
|
+It can contain some other fields.
|
|
|
|
|
|
We want the type $\{f : T\}$ to express \enquote{any record with a field $f$ of type $T$}.
|
|
|
To do this, we introduce the following sub-typing relation:
|
|
@@ -215,7 +215,6 @@ To do this, we introduce the following sub-typing relation:
|
|
|
\[
|
|
|
\inference{}{\{f_1 : T_1; \dots ; f_n : T_n; g_1 : S_1; \dots ; g_k : S_k\} <: \{f_1 : T_1; \dots ; f_n : T_n\}}
|
|
|
\]
|
|
|
-% FIXME on avait noté la relation <: dans l'autre sens
|
|
|
|
|
|
Note that in order to assure the reflexivity of our relation,
|
|
|
a type $S$ is a sub-type of $T$ if all the fields of $T$ are included in $S$.
|
|
@@ -245,7 +244,7 @@ Condition
|
|
|
\inference{\Gamma \vdash b & \Gamma \vdash S_1 & \Gamma \vdash S_2}{\Gamma \vdash \<if>\ b\ \<then>\ S_1\ \<else>\ S_2}
|
|
|
\]
|
|
|
|
|
|
-As the booleans expressions can contain expressions which can contain variables, they are not necessarily well typed. Hence we need to define typing rules on booleans:
|
|
|
+As the boolean expressions can contain expressions which can contain variables, they are not necessarily well typed. Hence we need to define typing rules on booleans:
|
|
|
\[
|
|
|
\inference{}{\Gamma \vdash \<true>}
|
|
|
\]
|
|
@@ -362,9 +361,9 @@ RF(5) &= RF(2) = \{x \mapsto \{f_1\}\}
|
|
|
\subsection{Termination}
|
|
|
|
|
|
We can design an algorithm to solve this equation system under the hypothesis that there is no label $l$ such as $(l, l) \in flow(P)$.
|
|
|
-At each step we can :
|
|
|
+At each step we can:
|
|
|
\begin{itemize}
|
|
|
-\item Rewrite a $RF(l)$ as $\bigcap_{(l', l) \in flow(P)} RF_{out}(l')$, where $RF_{out}(l')$ can be simplified into a term that does not contains $RF(l)$ (because $(l, l) \not\in flow(P)$).
|
|
|
+\item Rewrite a $RF(l)$ as $\bigcap_{(l', l) \in flow(P)} RF_{out}(l')$, where $RF_{out}(l')$ can be simplified into a term that does not contain $RF(l)$ (because $(l, l) \not\in flow(P)$).
|
|
|
\item Because a program contains a finite number of instructions, it exists a time when no $RF(l)$ is left. The system is solved.
|
|
|
\end{itemize}
|
|
|
|
|
@@ -386,7 +385,7 @@ Indeed, the expression $3 + x$ is not well typed as the type of $x$ is $\{f: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$.
|
|
|
+The static analysis will take the worst case of the two branches of the \<if> statement, that is the \<else> branch when $x$ does not 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}
|
|
@@ -395,9 +394,4 @@ A better solution of the two previous approaches is the union of them.
|
|
|
In other words, we could extend the static analysis by using the result of the type checking.
|
|
|
In this way, the two previous examples will be rightly rejected by the new analysis.
|
|
|
|
|
|
-% An other improvement could be made the analysis of the expressions.
|
|
|
-% Expressions are defined inductively and can contain sub-epxressions.
|
|
|
-% But the current static analysis only process one level of expression.
|
|
|
-% For instance, if we have an expression % TODO
|
|
|
-
|
|
|
\end{document}
|