# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1417416625 0
# Node ID f1491e0d7be0acf55887182a086e9af878fd774a
# Parent  92a718b88e14ecc5771abf6b15b86877f5a30b79
updated

diff -r 92a718b88e14 -r f1491e0d7be0 handouts/ho09.tex
--- a/handouts/ho09.tex	Fri Nov 28 12:22:50 2014 +0000
+++ b/handouts/ho09.tex	Mon Dec 01 06:50:25 2014 +0000
@@ -8,10 +8,10 @@
 
 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
+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 recent years some impressive
+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.
@@ -20,16 +20,22 @@
 \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 In 2011, this work was 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, it technical details are too
-numerous that they can be explained here. So let us look at
+While this work is impressive, its technical details are too
+enormous for explanation here. Therefore let us look at
 something much simpler, namely finding out properties about
-programs in a very simple programming language using
-\emph{static analysis}.
+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. 
+
+\bigskip
 
 \noindent What would be missing in comparison with real
 (low-level machine) code? Well, the numbers we assume to be