# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1374650525 -7200
# Node ID 98b3b769ec9aba010f65f0d516135925063e3113
# Parent  acc752cef1e74b3f59449c328363eed02a0fb707
slides

diff -r acc752cef1e7 -r 98b3b769ec9a Slides/Slides2.thy
--- a/Slides/Slides2.thy	Wed Jul 24 00:38:48 2013 +0200
+++ b/Slides/Slides2.thy	Wed Jul 24 09:22:05 2013 +0200
@@ -188,7 +188,7 @@
   \item Norrish formalised computability theory in HOL starting
   from the lambda-calculus\smallskip 
   \begin{itemize}
-  \item \textcolor{gray}{for technical reasons we could not follow him}
+  \item \textcolor{gray}{for technical reasons we could not follow his work}
   \item \textcolor{gray}{some proofs use TMs (Wang tilings)}
   \end{itemize}
   \bigskip
@@ -264,7 +264,7 @@
   \only<4->{
   \begin{textblock}{4}(4.2,12.4)
   \begin{tikzpicture}
-  \draw (0,0) node {\begin{tabular}{l}correct UTM by translation\end{tabular}};
+  \draw (0,0) node {\begin{tabular}{l}a correct UTM by translation\end{tabular}};
   \end{tikzpicture}
   \end{textblock}}
 
@@ -340,7 +340,7 @@
   @{text "I"} & $::=$  & @{term "Goto L\<iota>"}
   & \textcolor{black!60}{jump to instruction @{text L}}\\[1mm]
   & $\mid$ & @{term "Inc R\<iota>"} & \textcolor{black!60}{increment register @{text "R"} by one}\\[1mm]
-  & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & \textcolor{black!60}{if content of @{text R} is non-zero,}\\
+  & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & \textcolor{black!60}{if the content of @{text R} is non-zero,}\\
   & & & \textcolor{black!60}{then decrement it by one}\\
   & & & \textcolor{black!60}{otherwise jump to instruction @{text L}}
   \end{tabular}
@@ -384,7 +384,7 @@
   \item \small you define
   \begin{itemize}
   \item addition, multiplication, logical operations, quantifiers\ldots
-  \item coding of numbers (Cantor encoding), UTM
+  \item coding of numbers (Cantor encoding), UF
   \end{itemize}
 
   \end{itemize}
@@ -401,7 +401,10 @@
   \frametitle{Copy Turing Machine}%
 
   \begin{itemize}
-  \item TM that copies a number on the input tape\smallskip
+  \item TM that copies a number on the input tape
+  \begin{center}
+  @{text "copy \<equiv> cbegin ; cloop ; cend"}
+  \end{center}\smallskip
 
 
   \begin{center}
@@ -488,7 +491,6 @@
   \footnotesize
   \begin{center}
   \begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c}
-  \multicolumn{3}{@ {\hspace{-8mm}}l}{\small@{text "copy \<equiv> cbegin ; cloop ; cend"}}\\[4mm]
   \begin{tabular}[t]{@ {}l@ {}}
   @{text cbegin} @{text "\<equiv>"}\\
   \hspace{2mm}@{text "["}@{text "(W\<^bsub>0\<^esub>, 0), (R, 2), (R, 3),"}\\
@@ -669,8 +671,8 @@
   \frametitle{Hoare Reasoning}%
 
   \begin{itemize}
-  \item reasoning is still quite demanding;\\
-  the invariants of the copy-machine:\\[-5mm]\mbox{}
+  \item reasoning is quite demanding, e.g.~the invariants 
+  of the copy-machine:\\[-5mm]\mbox{}
 
   \footnotesize
   \begin{center}
@@ -711,7 +713,7 @@
 
   \begin{itemize}
   \item feels awfully like reasoning about machine code
-  \item compositional constructions / reasoning not at all frictionless
+  \item compositional constructions / reasoning is not at all frictionless
   \item sizes
 
   \begin{center}
@@ -774,7 +776,7 @@
   \frametitle{Better Composability}%
 
   \begin{itemize}
-  \item an idea from Jensen, Benton, Kennedy who looked at X86 
+  \item an idea from Jensen, Benton \& Kennedy who looked at X86 
   assembly programs and macros\bigskip
   
   \item assembly for TMs:\medskip
@@ -837,10 +839,12 @@
   \large @{text "{P} p {Q}"}
   \end{center}\bigskip\medskip
  
-  \item[@{text "(1)"}] we had to find a termination order proving that @{text p} terminates
-  \textcolor{gray}{(not easy)}
+  \item[@{text "(1)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy)}
+
   
-  \item[@{text "(2)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy either)}
+  
+  \item[@{text "(2)"}] we had to find a termination order proving that @{text p} terminates
+  \textcolor{gray}{(not easy either)}
   \end{itemize}\pause
   
   \begin{center}
@@ -934,12 +938,15 @@
   fun than first thought.\bigskip
 
   \item Where can you claim that you proved the correctness of
-  a @{text "38"} Mio instruction program. 
+  a @{text "38"} Mio instruction program?
   (ca.~@{text 7000} is the soa \raisebox{-1mm}{\includegraphics[scale=0.077]{smiley.jpg}})
   \bigskip
   
   \item We learned a lot about current verification technology for low-level code
-  (we had no infrastructure: CPU model).
+  (we had no infrastructure: CPU model).\bigskip
+
+  \item The existing literature on TMs \& RMs leave out quite a bit of the story
+  (not to mention contains bugs).
   \end{itemize}
   
 
diff -r acc752cef1e7 -r 98b3b769ec9a slides2.pdf
Binary file slides2.pdf has changed