Thesis stuff. Contribution & lit review.

1 files changed, 63 insertions, 4 deletions

diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex
index 4b9f3da..bde7160 100644
--- a/tex/thesis/litreview/litreview.tex
+++ b/tex/thesis/litreview/litreview.tex
@@ -1,6 +1,7 @@
 \newcommand{\Env}{\mathsf{Env}}
 \newcommand{\PP}{\mathsf{PP}}
 \newcommand{\States}{\mathsf{States}}
+\newcommand{\state}{\mathsf{state}}
 
 \chapter{Literature Review} \label{chap:litreview}
 
@@ -8,7 +9,65 @@
 
 In order to perform any static analysis of a program it is necessary
 to have some notion of the \emph{semantics}, or meaning, of a
-program.
+program. The semantics of a program can be captured in several ways,
+but for our purposes we will consider Denotational
+Semantics\cite{SCOTT70B}.
+
+Denotational semantics takes a view of a program as a (partial)
+function built up by the composition of many smaller functions. By
+expressing our expressions, assignments, conditionals and loops as
+smaller functions we can then compose them to determine the semantics
+of our whole program. For imperative languages we consider each
+assignment, conditional or loop as having the denotation $\llb s \rrb:
+\state \to \state$. We define their composition as $\llb s_1 ; s_2
+\rrb = \llb s_2 \rrb \circ \llb s_1 \rrb$.
+
+As an example, we'll define some denotational semantics for a simple
+language. Here our $\state$ will be a partial function $\state: I \to N$
+\newcommand\halfpage[1]{\begin{minipage}{0.45\textwidth}#1\end{minipage}}
+\newcommand\halfpages[2]{\halfpage{#1}\hfill\halfpage{#2}}
+\begin{figure}[here]
+  \halfpages{Syntax:}{Semantics:}
+
+  \halfpages{
+    $P :: S$
+  }{
+    $P: \state \to \state$ \\
+    $P\llb S \rrb = S\llb S \rrb \{\}$
+  }
+  \halfpages{
+    $S ::= S_1;S_2 \mid if ~B~ then ~S_1~ else ~S_2~ \mid I := E$
+  }{
+    $S: \state \to \state$ \\
+    $S\llb S_1;S_2 \rrb = \lambda v . (S\llb S_2 \rrb (S\llb S_1 \rrb(s)))$ \\
+    $S\llb if ~B~ then ~S_1~ else ~S_2~ \rrb = \lambda v . (S \llb S_b \rrb(v))$ \\
+    where $b = B\llb B \rrb (v) + 1$ \\
+    $S\llb I := E \rrb = \lambda v: (v \oplus \{ I \mapsto E \})$
+  }
+  \halfpages{
+    $E ::= E_1 + E_2 \mid I \mid N$
+  }{
+    $E: \state \to \N$ \\
+    $E\llb E_1 + E_2 \rrb = \lambda v . (E\llb E_1 \rrb(v) + E\llb E_2 \rrb(v))$ \\
+    $E\llb I \rrb = \lambda v . v(I)$ \\
+    $E\llb N \rrb = \lambda v . N$
+  }
+  \halfpages{
+    $B ::= E_1 = E_2 \mid \lnot B$
+  }{
+    $B: \state \to \{0,1\}$ \\
+    $B\llb E_1 = E_2 \rrb = \lambda v . (if ~\llb E_1 \rrb(v) = \llb E_2 \rrb(v) ~then~ 1 ~else~ 0)$
+  }
+  \halfpages{
+    $I ::= $ variable identifier
+  }{~}
+  \halfpages{
+    $N ::= \N$
+  }{~}
+  \label{fig:denotational-semantics-example}
+\end{figure}
+
+
 
 A program's semantics can be realised by considering the possible
 values for each variable at each point in the program, which we will
@@ -22,9 +81,9 @@ particular point
 As a formalisation of these notions we can consider these to be
 defined as follows:
 \begin{align*}
-  \Env: {} & X \to \Z \\
-  \PP: {} & \{ \text{program points} \} \\
-  \States: {} & \PP \times \Env
+  \Env:& X \to \Z \\
+  \PP:& \{ \text{program points} \} \\
+  \States:& \PP \times \Env
 \end{align*}