m2-pas-dm/dm.tex

\documentclass[11pt]{article}
\usepackage{fullpage}
\usepackage[bookmarks,hidelinks]{hyperref}

\usepackage{lscape}

%% Corrige quelques erreurs de LaTeX2ε
\usepackage{fixltx2e}
\usepackage{xspace}
\usepackage{microtype}

%% Pour ne pas commettre les erreurs fréquentes décrites dans l2tabu
\usepackage[l2tabu,abort]{nag}

%% Saisie en UTF-8
\usepackage[utf8]{inputenc}
%% Fonte : cf. http://www.tug.dk/FontCatalogue/
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{csquotes}

%% Pour écrire du français
% \usepackage[frenchb]{babel}

%% Pour composer des mathématiques
\usepackage{mathtools}

\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}

\usepackage{stmaryrd}
\usepackage{semantic}

\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}

%% Commandes du paquet semantic : langage While
\reservestyle{\command}{\textbf}
\command{skip,while,do,if,then,else,not,and,or,true,false,int}
%% -> Utiliser \<begin> Pour styliser le mot-clé

\newcommand{\reduce}{\rightarrow^{*}}

\begin{document}

\author{Timoth\'ee Haudebourg \and Thibaut Marty}
\title{Homework PAS/SDL}
\date{November 18, 2016}

\maketitle

\section{Small-step Semantic}

\subsection{Domains}

The $State$ domain of evaluation is defined as:
\[State = (Var \rightharpoonup Value) \cup \bot\]
Where $Var$ is the set of variables, and $Value$ the set of possible values.
We use $\bot$ to represent the error state.
In our model, a record is represented as a partial application $Field \rightharpoonup Value$.
This means that a record field can contains a record itself.
To do so, we define the set of value as:
\begin{align*}
	Value &= \bigcup_{i\in\mathbb{N}} Value_i \\
	Value_n &= \mathbb{N} \cup (Field \rightharpoonup Value_{n+1}) \\
\end{align*}

Because the variables are updated by copying, the codomain of the partial application is merely $Value$.
There is no references system.

\subsection{Denotational Semantic for expressions}

We define $\mathcal{A}$ the denotational semantics of arithmetic expressions as:

\[ \mathcal{A}|[ \bullet |] : AExpr \rightarrow State \rightarrow (Value \cup \bot) \]
where
\begin{align*}
  \mathcal{A} |[ n |] \sigma &= \mathcal{N} |[n|] \\
  \mathcal{A} |[ x |] \sigma &= \sigma x \\
  \mathcal{A} |[ e_1\ o\ e_2 |] \sigma &= \mathcal{A} |[ e_1 |] \sigma\ \bar{o}\ \mathcal{A} |[ e_2 |] \sigma, o \in \{+, -, \times\} \\
  \mathcal{A} |[ e.f |] \sigma &= \mathcal{A}|[e|] \sigma f\\
  \mathcal{A} |[ e_1{f \mapsto e_2} |] \sigma f &= \mathcal{A}|[ e_1 |] \sigma [f \mapsto \mathcal{A}|[ e_2 |] \sigma ]\\
  \mathcal{A} |[ \{f_1 = e_1 ; \dots ; f_n = e_n\} |] \sigma f_i &= \mathcal{A}|[ e_i |] \sigma \\
\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.

\subsection{Structural Operational Semantic for commands}

We define $->$ the structural operational semantics for commands as:

\[ ->\ \subseteq (Statement \times State) \times ((Statement \times State) \cup State) \]

\subsubsection{Regular execution}
For all $\sigma \neq \bot$:
\[
  \inference{}{(\<skip>, \sigma) -> \sigma}
\]
\[
  \inference{}{(x := a, \sigma) -> \sigma[x \mapsto \mathcal{A}|[a|] \sigma]}{\text{if }\mathcal{A}|[a|] \sigma \neq \bot}
\]
\[
  \inference{(S_1, \sigma) -> (S_1', \sigma')}{(S_1 ; S_2, \sigma) -> (S_1' ; S_2, \sigma')}
\]
\[
  \inference{(S_1, \sigma) -> \sigma'}{(S_1 ; S_2, \sigma) -> (S_2, \sigma')}
\]
\[
  \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> (S ; \<while>\ b\ \<do>\ S, \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{tt}}
\]
\[
  \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{ff}}
\]
\[
  \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> (S_1, \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{tt}}
\]
\[
  \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> (S_2, \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{ff}}
\]

\subsubsection{Error handling}
An error can occurs when one tries to add (or compare) records.
In that case, according to our definition of arithmetic expressions, $\mathcal{A}|[e|] \sigma$ (or $\mathcal{B}|[b|]$) will returns $\bot$.
From this point, the execution of the program makes no sense, and we will return the error state.

\[
  \inference{}{(x := a, \sigma) -> \bot}{\text{if }\mathcal{A}|[a|] \sigma = \bot}
\]
\[
  \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> \bot}{\text{if } \mathcal{B}|[b|] \sigma = \bot}
\]
\[
  \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> \bot}{\text{if } \mathcal{B}|[b|] \sigma = \bot}
\]

To ensure that the error can make it through the end, we also add the error propagation rule:

\[
  \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:
\[
  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:

\[
  \inference{}{\Gamma \vdash n : int}
\]
\[
  \inference{(x : T) \in \Gamma}{\Gamma \vdash x : T}
\]
\[
  \inference{\Gamma \vdash a_1 : int & \Gamma \vdash a_2 : int}{\Gamma \vdash a_1\ o\ a_2 : int}{o \in \{+, -, \times\}}
\]

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\}}
\]

Field assignment

\[
  \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[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\}}
\]
% 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$.
We also introduce a new subsumption typing rule:

\[
  \inference{\Gamma \vdash e : S & S <: T}{\Gamma \vdash e : T}
\]

Assignment
\[
  \inference{\Gamma \vdash x : T & \Gamma \vdash a : T}{\Gamma \vdash x := a}
\]

Sequence
\[
  \inference{\Gamma \vdash S_1 & \Gamma \vdash S_2}{\Gamma \vdash (S_1 ; S_2)}
\]

While loop
\[
  \inference{\Gamma \vdash b & \Gamma \vdash S}{\Gamma \vdash \<while>\ b\ \<do>\ S}
\]

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:
\[
  \inference{}{\Gamma \vdash \<true>}
\]
\[
  \inference{}{\Gamma \vdash \<false>}
\]
\[
  \inference{\Gamma \vdash b}{\Gamma \vdash \<not>\ b}
\]
\[
  \inference{\Gamma \vdash b_1 & \Gamma \vdash b_2}{\Gamma \vdash b_1\ o\ b_2}{o \in \{\<and>, \<or>\}}
\]
\[
  \inference{\Gamma \vdash a_1 : int & \Gamma \vdash a_2 : int}{\Gamma \vdash a_1 \le a_2}
\]
\[
  \inference{\Gamma \vdash a_1 : T & \Gamma \vdash a_2 : T}{\Gamma \vdash a_1 = a_2}
\]
Note: for the equality test, the rule works for \<int> as well as for records.

% Domains
\[
  n \in Num
\]
\[
  x \in Var
\]
\[
  e,e_1,e_2,a,a_1,a_2 \in AExpr
\]
\[
  b,b_1,b_2 \in BExpr
\]
\[
  f,f_1,\dots,f_n,f_i,g_1,\dots,g_k, \in Field % Field n'est pas défini…
\]
\[
  S,S_1,S_2 \in Statement
\]

\subsection{Correctness}

\begin{definition}[Well typed value]
A value $v \in Value$ is well typed regarding to a type $T$ (noted $v |- T$) when :
\begin{align*}
v |- int &=> v \in \mathbb{N} \\
v |- \{f_1 : T_1, \dots, f_n : T_n\} &=> v \in Field \rightharpoonup Value\text{ and }\forall f_i, f_i \in dom(v) \land v(t_i) |- T_i
\end{align*}
\end{definition}

\begin{definition}[Well typed state]
A state $\sigma \in State$, $\sigma \neq \bot$ is well typed with regards to a type system $\Gamma$ (noted $\sigma |- \Gamma$) when
\[\forall x \in Var,\ \Gamma |- x : T => x |- T\]
\end{definition}

\begin{lemma}[Well typed expressions cannot go wrong]
$\forall e \in AExpr, \sigma \in State, \Gamma$ such as $\sigma |- \Gamma$ :
\[\Gamma |- e : T => \mathcal{A}|[e|] \sigma |- T\]
In particular, $\mathcal{A}|[e|] \neq \bot$.
\end{lemma}

\begin{proof}
We demonstrate this property by induction on the structure of the expression $e$.
First let assume that $\Gamma |- e : T$.
We can eliminates all trivial cases in contradiction with this assumption (for example when $e = 1 + 1$ and $T = \{\}$).
Here are the other base cases:
\begin{itemize}
\item $e = n, T = int$.

$\mathcal{A}|[e|] = \mathcal{N}|[n|]$.

$\mathcal{N}|[n|] \in \mathbb{N}$ so we have $\mathcal{A}|[e|] \in \mathbb{N}$ which means that $\mathcal{A}|[e|] \sigma |- T$.

\item $e = n, T = int$.
\item $e = x$.
\item $e = e_1 o e_2, T = int$.
\item $e = e_1.f$.
\item $e = e_1[f \mapsto e_2]$.
\item $e = \{f_1 = e_1; \dots; f_n = e_n\}$.

\end{itemize}
\end{proof}

\begin{lemma}[Well typed programs cannot go wrong]
\[\forall \Gamma P,\quad \Gamma \vdash P \; => \;\forall \sigma,\; (P, \sigma) \not\reduce \bot\]
\end{lemma}

\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}

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 Fields}).
\[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*}

\subsection{Definition}

% TODO : définir l'opérateur \vdash

\[
  \inference{RF(l) \subseteq RF (init(S)) & RF \vdash (S, l) & RF(l) \subseteq RF(l')}{RF \vdash (\<while>\ [b]^l\ \<do>\ S, l')}
\]
\[
  \inference{RF(l) \subseteq RF(init(S_1)) & RF \vdash (S_1, l') \\ RF(l) \subseteq RF(init(S_2)) & RF \vdash (S_2, l')}{RF \vdash (\<if>\ [b]^l\ \<then>\ S_1\ \<else>\ S_2, l')}
\]
\[
  \inference{RF(l) \subseteq RF(l')}{RF \vdash ([skip]^l, l')}
\]
\[
  \inference{RF \vdash (S_1, init(S_2)) & RF \vdash (S_2, l')}{RF \vdash (S_1 ; S_2, l')}
\]
\[
  \inference{RF(l)[x \mapsto \{f_1, \dots, f_n\}] \subseteq RF(l')}{RF \vdash ([x := \{f_1 = e_1 ; \dots ; f_n = e_n\}]^l, l')}
\]
\[
  % TODO : il faudrait évaluer statiquement e_1 pour être moins pessimiste
  \inference{RF(l)[x \mapsto \{f\}] \subseteq RF(l')}{RF \vdash ([x := e_1[f \mapsto e_2]]^l, l')}
\]
% autres affectations
\[
  \inference{RF(l)[x \mapsto \emptyset] \subseteq RF(l')}{RF \vdash ([x := n]^l, l')}
\]
\[
  \inference{RF(l)[x \mapsto RF(l)(y)] \subseteq RF(l')}{RF \vdash ([x := y]^l, l')}
\]
\[
  \inference{RF(l)[x \mapsto \emptyset] \subseteq RF(l')}{RF \vdash ([x := e_1\ o\ e_2]^l, l')}
\]
\[
  \inference{RF(l)[x \mapsto \emptyset] \subseteq RF(l')}{RF \vdash ([x := e.f]^l, l')}
\]

\begin{landscape}
  \subsection{Example}
  Let $S_1 = [x := \{f_1 = 0; f_2 = 42\}]^1$,
  $S_3 = [y := \{f_1 = x.f_1 + 1\}]^3$,
  $S_4 = [x := y]^4$,
  and $S = \<while>\ ([x.f_1 \le 100]^2)\ \<do>\ (S_3 ; S_4)$.

  We perform the static analysis for the program $S_1 ; S$:
  {
    \footnotesize\[
      \inference
      {
        \inference
        {
          RF(1)[x \mapsto \{f_1, f_2\}] \subseteq RF(2)
        }
        {
          RF \vdash (S_1, 2)
        } &
        \inference
        {
          RF(2) \subseteq RF(3) &
          \inference
          {
            \inference
            {
              RF(3)[y \mapsto \{f_1\}] \subseteq RF(4)
            }
            {
              RF \vdash (S_3, 4)
            } &
            \inference
            {
              RF(4)[x \mapsto RF(4)(y)] \subseteq RF(2)
            }
            {
              RF \vdash (S_4, 2)
            }
          }
          {
            RF \vdash (S_3 ; S_4, 2)
          } &
          RF(2) \subseteq RF(l')
        }
        {
          RF \vdash (S, l')
        }
      }
      {
        RF \vdash (S_1; S, l')
      }
    \]
  }

  So the equation system is:
  \begin{align*}
    RF(1)[x \mapsto \{f_1, f_2\}] &\subseteq RF(2) \\
    RF(2) &\subseteq RF(3) \\
    RF(3)[y \mapsto \{f_1\}] &\subseteq RF(4) \\
    RF(4)[x \mapsto RF(4)(y)] &\subseteq RF(2) \\
    RF(2) &\subseteq RF(l')
  \end{align*}
\end{landscape}

\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}