--- a/handouts/ho09.tex	Fri Dec 05 01:17:31 2014 +0000
+++ b/handouts/ho09.tex	Mon Dec 08 07:14:28 2014 +0000
@@ -1,6 +1,9 @@
 \documentclass{article}
 \usepackage{../style}
 \usepackage{../langs}
+\usepackage{../graphics}
+\usepackage{../grammar}
+\usepackage{multicol}
 
 \begin{document}
 
@@ -8,32 +11,111 @@
 
 If we want to improve the safety and security of our programs,
 we need a more principled approach to programming. Testing is
-good, but as Dijkstra famously said: ``Testing can only show
-the presence of bugs, not their absence''. While such a more
-principled approach has been the subject of intense study for
-a long time, only in the past few years some impressive
-results have been achieved. One is the complete formalisation
-and (mathematical) verification of a microkernel operating
-system called seL4.
+good, but as Dijkstra famously said: 
+
+\begin{quote}\it 
+``Program testing can be a very effective way to show the
+\underline{\smash{presence}} of bugs, but it is hopelessly
+inadequate for showing their \underline{\smash{absence}}.''
+\end{quote}
+
+\noindent While such a more principled approach has been the
+subject of intense study for a long, long time, only in the
+past few years some impressive results have been achieved. One
+is the complete formalisation and (mathematical) verification
+of a microkernel operating system called seL4.
 
 \begin{center}
 \url{http://sel4.systems}
 \end{center}
 
-\noindent In 2011, this work was included in the MIT
-Technology Review in the annual list of the world’s ten most
-important emerging
+\noindent This work was in 2011 included in the MIT Technology
+Review in the annual list of the world’s ten most important
+emerging
 technologies.\footnote{\url{http://www2.technologyreview.com/tr10/?year=2011}}
 While this work is impressive, its technical details are too
-enormous for explanation here. Therefore let us look at
+enormous for an explanation here. Therefore let us look at
 something much simpler, namely finding out properties about
 programs using \emph{static analysis}.
 
-Static analysis is one technique that checks properties
-of a program without actually running the program. This
-should raise alarm bells---the reason that almost all 
-interesting properties about programs are equivalent to
-the halting problem, which we know is undecidable. 
+Static analysis is one technique that checks properties of a
+program without actually running the program. This should
+raise alarm bells with you---because almost all interesting
+properties about programs are equivalent to the halting
+problem, which we know is undecidable. For example estimating
+the memory consumption of programs is in general undecidable,
+just like the halting problem. Static analysis circumvents
+this undecidability-problem by essentially allowing answers
+\emph{yes} and \emph{no}, but also \emph{don't know}. With
+this ``trick'' even the halting problem becomes
+decidable\ldots{}for example we could always say \emph{don't
+know}. Of course this would be silly. The point is that we
+should be striving for a method that answers as often as
+possible \emph{yes} or \emph{no}---just in cases when it is
+too difficult we fall back on the \emph{don't-know}-answer.
+This might sound all like abstract nonsense. Therefore let us
+look at a concrete example.
+
+
+\subsubsection*{A Simple, Idealised Programming Language}
+
+Our starting point is a small, idealised programming language.
+This language contains variables holding integers. We want to
+find out what the sign of these integers will be when the
+program runs. This seems like a very simple problem, but it
+will turn out even such a simple analysis is in general
+undecidable, just like Turing's halting problem. Is it an
+interesting problem? Well, yes---if a compiler can find out
+that for example a variable will never be negative and this
+variable is used as an index for an array, then the compiler
+does not need to generate code for an underflow-test. Remember
+some languages are immune to buffer-overflow attacks because
+they add bound checks everywhere. This could potentially
+drastically speed up the generated code.
+
+Since we want to 
+
+\begin{multicols}{2}
+\begin{plstx}[rhs style=,one per line,left margin=9mm]
: \meta{Exp} ::= \meta{Exp} \texttt{+} \meta{Exp}
+               | \meta{Exp} \texttt{*} \meta{Exp}
+               | \meta{Exp} \texttt{=} \meta{Exp} 
+               | \meta{num}
+               | \meta{var}\\
+\end{plstx}
+\columnbreak
+\begin{plstx}[rhs style=,one per line]
+: \meta{Stmt} ::= \meta{label} \texttt{:}
+                | \meta{var} \texttt{:=} \meta{Exp}
+                | \texttt{jmp?} \meta{Exp} \meta{label}
+                | \texttt{goto} \meta{label}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
+\end{plstx}
+\end{multicols}
+
+\begin{lstlisting}[numbers=none,
+                   language={},xleftmargin=10mm]
+      a := 1
+      n := 5 
+top:  jmp? n = 0 done 
+      a := a * n 
+      n := n + -1 
+      goto top 
+done:
+\end{lstlisting}
+
+\begin{lstlisting}[numbers=none,
+                   language={},xleftmargin=10mm]
+      n := 6
+      m1 := 0
+      m2 := 1
+loop: jmp? n = 0 done
+      tmp := m2
+      m2 := m1 + m2
+      m1 := tmp
+      n := n + -1
+      goto top
+done:
+\end{lstlisting}
 
 \bigskip