summaryrefslogtreecommitdiff
path: root/tex/thesis/litreview/litreview.tex
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis/litreview/litreview.tex')
-rw-r--r--tex/thesis/litreview/litreview.tex67
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*}