Merge branch 'master' of ssh://bitbucket.org/czan/honours

Conflicts:
	impl/IdSet.hpp
	impl/main.cpp
	impl/systems/long-fixpoint

2 files changed, 83 insertions, 17 deletions

diff --git a/tex/lit-review/main.tex b/tex/lit-review/main.tex
index 8f5c5ce..28a9495 100644
--- a/tex/lit-review/main.tex
+++ b/tex/lit-review/main.tex
@@ -48,7 +48,8 @@ abstraction we can still define some semantics which reflect the program itself
 a negative number is a negative number). Each abstract domain must also contain
 a "top" $(\top)$ and a "bottom" $(\bot)$ element. The existence of these two
 elements turn our abstract domain into a complete lattice, which ensures some
-helpful properties of our abstract domain.
+helpful properties of our abstract domain, including the existence of solutions
+to fixpoint-equations (\cite{tarski}).
 
 By constructing appropriate abstract domains we can infer properties of the
 program's concrete semantics which are relevant to our application. The above
@@ -71,7 +72,7 @@ positive/negative/zero.
 The abstract domain of "zones", are handled in \cite{mine:padoII}. These zones
 provide a way to perform analysis on the bounds of variable differences (ie. to
 place bounds as $a - b \leq c$) and are also referred to as Difference Bound
-Matrices (which are used in other model-checking applications
+Matrices (which are used in other model-checking applications, such as
 \cite{Yovine98modelchecking}).
 
 The domain of zones is then extended by the same author into the "Octagon
@@ -88,6 +89,14 @@ one can define a polyhedra $1 \times x_1 + (-1) \times x_2 + c \ge 0$ which is
 equivalent. The octagon domain is $(\pm 1) \times x_1 + (\pm 1) \times x_2 + c
 \ge 0$.
 
+Non-integral abstract domains have also been investigated in papers such as
+\cite{springerlink}, which considers the abstract domain
+of strings with abstract values being regular expressions, but it seems the
+majority of the literature is concerned with providing bounds for integral, or
+at the very least numerical, expressions. The reasons for this are fairly
+obvious when one considers the ubiquity of integers and the relative simplicity
+of the numerical domain compared to many others.
+
 \section{Fixpoints}
 
 When performing static analysis there is a great need to perform some sort of
@@ -96,9 +105,10 @@ When looping, for instance, it is necessary to "iterate" (in some sense) to find
 what values each variable may take during a loop iteration.
 
 The most basic method for doing so is simply to perform a complete iteration in
-the abstract domain, but doing so has no guarantee of termination and would not
-be expected to be performant. In \cite{CousotCousot77-1} an approach of
-"widening" and "narrowing" is introduced.
+the abstract domain, but doing so within the integers has no guarantee of
+termination (due to the integers being an unbounded set) and would not be
+expected to be performant. In \cite{CousotCousot77-1} an approach of "widening"
+and "narrowing" is introduced.
 
 This widening/narrowing method performs some fixed number of iteration steps.
 If, after this fixed number, the iteration has not stabilised then it assumes
@@ -108,20 +118,42 @@ wherein variables are brought back into the finite domain by some terminating
 condition on the loop.
 
 This approach is quite general, and so is applicable to many instances of real
-programs, but is a crude approximation of the reality of the program. In
-specific instances it is possible to perform a better approximation. In
-particular the case of monotonic, expansive operators is considered in \cite{}.  % something from thomas here
-With this approach code points are converted into fixpoint equations with
-$minimum$ and $maximum$ expressions. These fixpoint equations can then be solved
-in order to give information about the program's abstract semantics. These
-equations are solved using the technique of strategy iteration \cite{}  % something about strategy iteration here
-combined with a fast fixpoint-iteration algorithm (such as the one presented in
-\cite{DBLP:tr/trier/MI96-11}).
-
-%Other test citation: \cite{DBLP:tr/trier/MI96-11}
+programs, but is a crude approximation of the reality of the program (albeit,
+with surprisingly good results). In specific instances it is possible to perform
+a better approximation. In particular the case of addition, multiplication (by
+positive constants), minimum and maximum is considered in
+\cite{Gawlitza:2007:PFC:1762174.1762203}.  With this approach code points are
+converted into fixpoint equations with $minimum$ and $maximum$ expressions.
+These fixpoint equations can then be solved in order to give information about
+the program's abstract semantics. These equations are solved using a form of
+policy iteration (referred to as strategy iteration) over the $maximum$
+expressions present in each term.  A second step consisting of ordinary
+fixpoint-iteration over the resulting $minimum$-expressions is then performed.
+
+When fixpoint-iteration is known to terminate then it is possible to get
+significant speed gains by processing each expression according to their
+dependencies. The approach presented in \cite{DBLP:tr/trier/MI96-11}, in
+particular, improves the real-world performance of their fixpoint-equation
+solver. It should be noted, however, that such evaluation strategies can do
+nothing to affect the worst-case complexity as it is always possible to
+construct a system in which evaluation of each variable is necessary at every
+stage until the system stabilises.
 
 \section{Conclusion}
 
+Static analysis is of great practical importance to real world developers. It
+gives us the ability to create tools which automatically identify common errors
+in programs due to developer errors and so allows us to provide greater
+guarantees about the behaviour of our software.
+
+Unfortunately complete static analysis of a program is an undecidable problem,
+and so we must perform abstract interpretation of a program's semantics in order
+to provide useful results of analysis. Many different abstract domains exist in
+which to consider programs, with varying precision and computational complexity.
+In particular the abstract domain of polyhedra (and the related domains of
+zones and ranges) are of great use when performing analysis of a program's
+integral semantics.
+
 \bibliographystyle{abbrv}
 \bibliography{references.bib}
 \end{document}
diff --git a/tex/lit-review/references.bib b/tex/lit-review/references.bib
index d6db721..d746821 100644
--- a/tex/lit-review/references.bib
+++ b/tex/lit-review/references.bib
@@ -80,4 +80,38 @@
   pages = {114--152},
   publisher = {Springer-Verlag}
 }
-
+@inproceedings{Gawlitza:2007:PFC:1762174.1762203,
+  author = {Gawlitza, Thomas and Seidl, Helmut},
+  title = {Precise fixpoint computation through strategy iteration},
+  booktitle = {Proceedings of the 16th European conference on Programming},
+  series = {ESOP'07},
+  year = {2007},
+  isbn = {978-3-540-71314-2},
+  location = {Braga, Portugal},
+  pages = {300--315},
+  numpages = {16},
+  url = {http://dl.acm.org/citation.cfm?id=1762174.1762203},
+  acmid = {1762203},
+  publisher = {Springer-Verlag},
+  address = {Berlin, Heidelberg},
+} 
+@article{tarski,
+  author = {Tarski, Alfred},
+  title = {A lattice-theoretical fixpoint theorem and its
+           applications.},
+  year = {1955}
+}
+@incollection {springerlink,
+  author = {Christensen, Aske and Mø, Anders and Schwartzbach, Michael},
+  affiliation = {BRICS Denmark},
+  title = {Precise Analysis of String Expressions},
+  booktitle = {Static Analysis},
+  series = {Lecture Notes in Computer Science},
+  editor = {Cousot, Radhia},
+  publisher = {Springer Berlin / Heidelberg},
+  isbn = {978-3-540-40325-8},
+  keyword = {Computer Science},
+  pages = {1076-1076},
+  volume = {2694},
+  year = {2003}
+}