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{Introduction}

% TODO

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

\input{sections/correctness.tex}

\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$.

\subsection{Definition}

Here is the definition of the static analysis.
We suppose that we dispose of the control flow graph $flow(P)$ of the program.

\[RF(l) = \bigcap_{(l', l) \in flow(P)} RF_{out}(l')\]

Where $RF_{out}$ is defined by:

\begin{align*}
RF_{out}([\<skip>]^l) &= RF(l) \\
RF_{out}([b]^l) &= RF(l)\quad(b \in BExp)\\
RF_{out}([x := n]^l) &= RF(l)[x \mapsto \{\}]\quad(n \in \mathbb{N})\\
RF_{out}([x := y]^l) &= RF(l)[x \mapsto (RF(l) y)]\quad(y \in Var)\\
RF_{out}([x := \{f_1 = e_1; \dots; f_n = e_n\}]^l) &= RF(l)[x \mapsto \{f_1, \dots, f_n\}]\\
RF_{out}([x := e_1[f \mapsto e_2]]^l) &= RF(l)[x \mapsto \{f\}] \\
RF_{out}([x := e.f]^l) &= RF(l)[x \mapsto \{\}]
\end{align*}

\begin{align*}
\mathcal{A}
\end{align*}

\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]^5$:
Let's begin with the initial state:

\begin{align*}
RF(1) &= \{\}
RF(2) &= RF(1) \cap RF(4)
RF(3) &= RF(2)[y \mapsto \{f_1\}]
RF(4) &= 
\end{align*}

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

\section{Discussion of the type system and static analysis}

% The static analysis and the type system are complementary to prove
% is pessimistic by nature, so it will reject some programs which are legals.

The static analysis of the program $x := \{f = 1\} ; y := 3 + x$ works because there is no undefined field reading.
The variable $x$ contains one field $f$, and no other fields are read.
However, the type system rejects this program.
Indeed, the expression $3 + x$ is not well typed as the type of $x$ is $\{f:int\}$, not $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$.
Thus, the last statement, $y := x.f$, tries to reach the undefined (according to the analysis) field $f$.

\subsection{Extension of the static analysis}

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}