A bunch more writing. Write write write.

1 files changed, 43 insertions, 38 deletions

diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex
index 1e0ef90..109864e 100644
--- a/tex/thesis/litreview/litreview.tex
+++ b/tex/thesis/litreview/litreview.tex
@@ -10,19 +10,19 @@
 
 \chapter{Preliminaries} \label{chap:litreview}
 
-In this chapter we will review the relevant portion of literature
-pertaining to static analysis. We will briefly cover the semantics of
-programs generally before looking more closely at the framework of
-abstract interpretation for program analysis. The chapter will
-conclude with an explanation of one particular method of abstract
-interpretation over zones.
+In this chapter we review the relevant literature pertaining to static
+analysis. We briefly cover the semantics of programs generally before
+looking more closely at the framework of abstract interpretation for
+program analysis. The chapter concludes with an explanation of the
+particular method of abstract interpretation over intervals and zones
+which is implemented in this thesis.
 
 \section{Program Semantics}
 
 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. The semantics of a program can be captured in several ways,
-but for our purposes we will consider \emph{denotational}, or
+but for our purposes we consider \emph{denotational}, or
 \emph{mathematical}, \emph{semantics}\cite{SCOTT70B}.
 
 Denotational semantics views a program as a (partial) function built
@@ -77,7 +77,7 @@ following example:
 
   One possible abstraction would be to instead consider a variable's
   \emph{sign}. That is, to consider $x$ as satisfying one of the
-  following (the symbols in parentheses will be used to refer to these
+  following (the symbols in parentheses are used to refer to these
   values from now):
   \begin{align*}
     x &\in \Z & (\pm) \\
@@ -180,14 +180,14 @@ to perform abstract interpretation over zones.
 
 \subsection{Partial-ordering Formulation}
 
-To begin our construction of the equation systems we first need to
-formalise one of a CFG. For our purposes we will consider a CFG to be
-a tuple $G = (N, E, s, st)$. A finite set of \emph{control-points}
-$N$, a finite set $E \subseteq N \times N$ of \emph{edges} between
-these control points (ie. if $(u,v) \in E$ then an edge exists in the
-CFG from $u$ to $v$). A mapping $s: N \times N \to \Stmt$ taking each
-edge in the CFG to a \emph{statement} $\in \Stmt$. $st \in N$ denotes
-the special \emph{start control-point}.
+To begin our construction of the equation systems we need to formalise
+one of a CFG. We consider a CFG to be a tuple $G = (N, E, s, st)$. A
+finite set of \emph{control-points} $N$, a finite set $E \subseteq N
+\times N$ of \emph{edges} between these control points (ie. if $(u,v)
+\in E$ then an edge exists in the CFG from $u$ to $v$). A mapping $s:
+N \times N \to \Stmt$ taking each edge in the CFG to a
+\emph{statement} $\in \Stmt$. $st \in N$ denotes the special
+\emph{start control-point}.
 
 We can now begin our construction of our abstract semantics $V^\#[v],
 \forall v \in N$.
@@ -280,15 +280,15 @@ least as big as the complete set of abstract states (as in
     \label{fig:partial-ordered-construction}
   \end{figure}
 
-  We will now attempt to derive a system of inequalities from this for
-  the \emph{least upper bound}
+  We now attempt to derive a system of inequalities from this for the
+  \emph{least upper bound}
   \begin{align*}
     ub: {} & ~\Vars \to \CZ \\
     ub(x) &= \min\{v \in \CZ ~|~ x \le v\}.
   \end{align*}
   We wish to find a value for $ub(x)$ at each program point in our
-  original program. We will denote these values by $ub_A(x)$,
-  $ub_B(x)$ and $ub_C(x)$.
+  original program. We denote these values by $ub_A(x)$, $ub_B(x)$ and
+  $ub_C(x)$.
 
   For $A$ the value of $x$ is entirely unknown, so no useful bound can
   be given. The possible values of $x$ are bounded only by the top
@@ -307,10 +307,10 @@ least as big as the complete set of abstract states (as in
 
   The edge from $B$ to itself is somewhat more complex. To begin with
   it changes the value of $x$ depending on the previous value of
-  $x$. It also is executed conditionally (when $x \le 99$), which will
-  affect the bound on $x$. Because the condition limits the growth of
-  $x$ the corresponding equation for this edge is $ub(x_B) \ge
-  \min(x, 99) + 1$.
+  $x$. It also is executed conditionally (when $x \le 99$), which
+  affects the bound on $x$. Because the condition limits the growth of
+  $x$ the corresponding equation for this edge is $ub(x_B) \ge \min(x,
+  99) + 1$.
 
   This leaves us with two simultaneous constraints on the value of
   $ub(x_B)$.
@@ -348,7 +348,7 @@ least as big as the complete set of abstract states (as in
 The partial-ordering formulation considered above is a helpful
 presentation of the problem in terms of constraints, but an equivalent
 system can be constructed to aid us in locating the \emph{least}
-solution to the system.
+solution to the constraint system.
 
 For every partial-ordering on a set there exists an equivalent
 lattice, defined in terms of a meet operator ($\vee$) and a join
@@ -358,10 +358,11 @@ operator ($\land$), which are defined by the following relationships:
   x \le y ~&\iff~ x \land y = x
 \end{align*}
 
-In the case that we are considering, with $x, y \in \CZ$, the meet and
-join operators correspond with $\max$ and $\min$, respectively. This
-allows us to simplify the system of inequalities in Example
-\ref{example:partial-ordered-construction} to the following:
+In the case of Example \ref{example:partial-ordered-construction},
+with $x, y \in \CZ$, the meet and join operators correspond with
+$\max$ and $\min$, respectively. This allows us to simplify the system
+of inequalities in Example \ref{example:partial-ordered-construction}
+to the following:
 \begin{align*}
   ub(x_A) &= \infty \\
   ub(x_B) &= \max(1, \min(ub(x_B), 99) + 1) \\
@@ -370,7 +371,11 @@ allows us to simplify the system of inequalities in Example
 
 The two constraints on the upper bound of $x_B$ can be combined into
 one constraint by taking the maximum of them. This is because $x \ge
-\max(a, b) ~\implies~ x \ge a \text{ and } x \ge b$
+\max(a, b) ~\implies~ x \ge a \text{ and } x \ge b$. The
+Knaster-Tarski Fixpoint 
+%We change from using $\ge$ in our constraints to using $=$ in our
+%equation system as a consequence of the Knaster-Tarski Fixpoint
+%Theorem\cite{Knaster-Tarski}.
 
 
 
@@ -378,19 +383,19 @@ one constraint by taking the maximum of them. This is because $x \ge
   \label{example:both-bounds}
 
   In order to determine a lower bound for $x$ at each program point it
-  is sufficient to determine an \emph{upper} bound for $-x$. We will
-  again consider the program fragment in Figure
+  is sufficient to determine an \emph{upper} bound for $-x$. We again
+  consider the program fragment in Figure
   \ref{fig:partial-ordered-construction}.
 
-  We will now try to derive an equation system for the \emph{upper}
-  and \emph{lower} bounds of $x$.
+  We now try to derive an equation system for the \emph{upper} and
+  \emph{lower} bounds of $x$.
 
   In order to capture the state of the variables at each program point
-  we will consider the abstract state as the two-dimensional vector
+  we consider the abstract state as the two-dimensional vector
   $(ub(x), -lb(x))$, that is the upper bound of $x$, $ub(x)$, and the
   \emph{negated} lower bound of $x$, $-lb(x)$. The least fixpoint of
-  our system of equations over $\CZ^2$ will then give us our bounds
-  for $ub(x)$ and $lb(x)$.
+  our system of equations over $\CZ^2$ then gives us bounds for
+  $ub(x)$ and $lb(x)$.
 
   To begin with, let us once again consider the node $A$. At the point
   of $A$ there is no information as to the bounds of $x$, so our
@@ -580,7 +585,7 @@ one constraint by taking the maximum of them. This is because $x \ge
 \label{sec-1-3-5}
 
 
-Reconsidering our earlier equation system, we will now attempt to find
+Reconsidering our earlier equation system, we now attempt to find
 the minimal fixpoint by means of \emph{policy iteration} and
 \emph{fixpoint iteration}.