wip

dm.tex

@@ -14,6 +14,7 @@
 %% Fonte : cf. http://www.tug.dk/FontCatalogue/
 \usepackage[T1]{fontenc}
 \usepackage{lmodern}
+\usepackage{csquotes}
 
 %% Pour écrire du français
 % \usepackage[frenchb]{babel}
@@ -88,7 +89,7 @@ We define $->$ the structural operational semantics for commands as:
 \subsubsection{Regular execution}
 For all $\sigma \neq \bot$:
 \[
-  \inference{}{(skip, \sigma) -> \sigma}
+  \inference{}{(\<skip>, \sigma) -> \sigma}
 \]
 \[
   \inference{}{(x := a, \sigma) -> \sigma[x \mapsto \mathcal{A}|[a|] \sigma]}{\text{if }\mathcal{A}|[a|] \sigma \neq \bot}
@@ -133,6 +134,9 @@ To ensure that the error can make it through the end, we also add the error prop
   \inference{}{(S, \bot) -> \bot}
 \]
 
+Finally, note that according to the exercise statement, we suppose that all variables are already defined in $\sigma$,
+so that no error can occur because of an undefined variable.
+
 \section{Type system}
 
 We suppose now that every variable in the program is declared with a type satisfying the following syntax:
@@ -140,6 +144,8 @@ We suppose now that every variable in the program is declared with a type satisf
   t\quad::=\quad\text{int }|\ \{f_1 : t_1;\ \dots\ ; f_n : t_n\}
 \]
 
+\subsection{Definition}
+
 We note $\Gamma \vdash S$ the type judgment for our language, defined by the following typing rules:
 
 \[
@@ -151,24 +157,78 @@ We note $\Gamma \vdash S$ the type judgment for our language, defined by the fol
 \[
   \inference{\Gamma \vdash a_1 : int & \Gamma \vdash a_2 : int}{\Gamma \vdash a_1\ o\ a_2 : int}
 \]
+
+Records
+
 \[
-  \inference{\Gamma \vdash e_1 : T_1 & \dots & \Gamma \vdash e_n : T_n}{\Gamma \vdash \{f_1 = e_1 ; \dots ; f_n = e_n\} : \{f_1 : T_1 ; \dots f_n : T_n\}}
+  \inference{\Gamma \vdash e_1 : T_1 & \dots & \Gamma \vdash e_n : T_n}{\Gamma \vdash \{f_1 = e_1 ; \dots ; f_n = e_n\} : \{f_1 : T_1 ; \dots; f_n : T_n\}}
 \]
+
+Field assignment
+
 \[
-  \inference{\Gamma \vdash \{f : T\}}{\Gamma \vdash e.f : T}
+  \inference[append ]{\Gamma \vdash e_2 : T & \Gamma \vdash e_1 : \{f_1 : T_1; \dots; f_n : T_n\}}{\Gamma \vdash e_1[f \mapsto e_2] : \{f : T; f_1 : T_1; \dots; f_n : T_n\}}
 \]
 \[
-  \inference{\Gamma \vdash e_2 : T & \Gamma \vdash e_1 : \{f_1 : T_1 ; \dots ; f_n : T_n\}}{\Gamma \vdash e_1[f \mapsto e_2] : \{f : T ; f_1 : T_1 ; \dots ; f_n : T_n\}}
+  \inference[override ]{\Gamma \vdash e_2 : T & \Gamma \vdash e_1 : \{f_1 : T_1; \dots; f_i : T_i; \dots; f_n : T_n\}}{\Gamma \vdash e_1[f_i \mapsto e_2] : \{f_1 : T_1; \dots; f_i : T; \dots; f_n : T_n\}}
+\]
+
+Field lookup
+
+\[
+  \inference{\Gamma \vdash e : \{f : T\}}{\Gamma \vdash e.f : T}
+\]
+
+As is, the last rule can seems 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.
+
+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:
+
+\[
+  \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\}}
+\]
+
+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$.
+We also introduce a new subsumption typing rule:
+
+\[
+  \inference{\Gamma \vdash e : S & S <: T}{\Gamma \vdash e : T}
 \]
 
-% TODO : règle sub-typing
 % TODO : booléens… (autre photo)
 
+\subsection{Correctness}
+
+\[\forall \Gamma P,\quad \Gamma \vdash P \; => \;\forall \sigma,\; (P, \sigma) \not\reduce \bot\]
+
+\begin{proof}
+By induction on the path of $\reduce$, and by induction on the structure/type of the statement at each step of the path.
+\end{proof}
+
 \section{Static analysis}
 
-$RF : Lab -> Var -> \mathcal{P}(Field)$
+We propose a constraint based static analysis to determine at each instruction which field is defined in each variables.
+Our static analysis is incarnated by the function $RF$ (\enquote{Reachable Fileds}).
+
+\[RF : Lab -> Var -> \mathcal{P}(Field)\]
+
+where $Lab$ is the set of labels.
+One unique label is assigned to each instruction.
+For the sake of simplicity, we note $[I]^l$ the instruction of label $l$.
+We also define an $init$ function returning the first label of a statement where:
+
+\begin{align*}
+	&init([\<skip>]^l) = l\\
+	&init([x := a]^l) = l\\
+	&init(S_1;S_2) = init(S_1)\\
+	&init(\<while>\ [b]^l\ \<do>\ S) = l \\
+	&init(\<if>\ [b]^l\ \<then>\ S_1\ \<else>\ S_2) = l
+\end{align*}
 
-% TODO : définir init
+\subsection{Definition}
 
 \[
   \inference{RF(l) \subseteq RF (init(S)) & RF \vdash (S, l) & RF(l) \subseteq RF(l')}{RF \vdash (\<while>\ [b]^l\ \<do>\ S, l')}
@@ -203,4 +263,17 @@ $RF : Lab -> Var -> \mathcal{P}(Field)$
   \inference{RF(l)[x \mapsto \emptyset] \subseteq RF(l')}{RF \vdash ([x := e.f]^l, l')}
 \]
 
+\subsection{Example}
+
+Example.
+
+\subsection{Termination}
+
+In each premise of each rule, the size of the statement is \emph{strictly} decreasing,
+assuring the termination of the analysis.
+
+\subsection{Safety}
+
+This is a pessimistic static analysis.
+
 \end{document}