(*<*)
theory Slides3
imports "../thys/UTM" "../thys/Abacus_Defs"
begin
declare [[show_question_marks = false]]
hide_const (open) s
abbreviation
"update2 p a \<equiv> update a p"
notation (Rule output)
"==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
syntax (Rule output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
("\<^raw:\mbox{>_\<^raw:}\\>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
notation (Axiom output)
"Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
notation (IfThen output)
"==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThen output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
notation (IfThenNoBox output)
"==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThenNoBox output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("_")
context uncomputable
begin
notation (latex output)
Cons ("_::_" [48,47] 68) and
append ("_@_" [65, 64] 65) and
Oc ("1") and
Bk ("0") and
exponent ("_\<^bsup>_\<^esup>" [107] 109) and
inv_begin0 ("I\<^sub>0") and
inv_begin1 ("I\<^sub>1") and
inv_begin2 ("I\<^sub>2") and
inv_begin3 ("I\<^sub>3") and
inv_begin4 ("I\<^sub>4") and
inv_begin ("I\<^bsub>cbegin\<^esub>") and
inv_loop1 ("J\<^sub>1") and
inv_loop0 ("J\<^sub>0") and
inv_end1 ("K\<^sub>1") and
inv_end0 ("K\<^sub>0") and
recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^sup>_\<^raw:}>\<^sub>_") and
Pr ("Pr\<^sup>_") and
Cn ("Cn\<^sup>_") and
Mn ("Mn\<^sup>_") and
tcopy ("copy") and
tcontra ("contra") and
tape_of ("\<langle>_\<rangle>") and
code_tcontra ("code contra") and
tm_comp ("_ ; _")
lemma inv_begin_print:
shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and
"s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and
"s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and
"s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and
"s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and
"s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"
apply(case_tac [!] tp)
by (auto)
lemma inv1:
shows "0 < (n::nat) \<Longrightarrow> Turing_Hoare.assert_imp (inv_begin0 n) (inv_loop1 n)"
unfolding Turing_Hoare.assert_imp_def
unfolding inv_loop1.simps inv_begin0.simps
apply(auto)
apply(rule_tac x="1" in exI)
apply(auto simp add: replicate.simps)
done
lemma inv2:
shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"
apply(rule ext)
apply(case_tac x)
apply(simp add: inv_end1.simps)
done
lemma measure_begin_print:
shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and
"s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and
"s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and
"s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"
by (simp_all)
lemma inv_begin01:
assumes "n > 1"
shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"
using assms by auto
lemma inv_begin02:
assumes "n = 1"
shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"
using assms by auto
(*>*)
text_raw {*
\renewcommand{\slidecaption}{Imperial College, 24 November 2013}
\newcommand{\bl}[1]{#1}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{%
\begin{tabular}{@ {}c@ {}}
\\[-3mm]
{\fontsize{30}{30}\selectfont{}Turing Machines and}\\[-1mm]
{\fontsize{30}{30}\selectfont{}Separation Logic}\\[0mm]
{\fontsize{22}{22}\selectfont{}(Work in Progress)}\\[-3mm]
\end{tabular}}
\bigskip\medskip\medskip
\begin{center}
\begin{tabular}{c@ {\hspace{1cm}}c}
\includegraphics[scale=0.29]{jian.jpg} &
\includegraphics[scale=0.034]{xingyuan.jpg} \\
Jian Xu & Xingyuan Zhang\\[-3mm]
\end{tabular}\\[3mm]
\small PLA University of Science and Technology
\end{center}
\begin{center}
Christian Urban\\[0mm]
\small King's College London
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Why Turing Machines?}%
\begin{itemize}
\item we wanted to formalise computability theory
\item at the beginning, it was just a student project\smallskip
\begin{center}
\begin{tabular}{c}
\includegraphics[scale=0.3]{boolos.jpg}\\[-2mm]
\footnotesize Computability and Logic (5th.~ed)\\[-2mm]
\footnotesize Boolos, Burgess and Jeffrey\\[2mm]
\end{tabular}
\end{center}
\item found an inconsistency in the definition of halting computations
(Chap.~3 vs Chap.~8)
\end{itemize}
\only<2->{
\begin{textblock}{1}(0.7,4)
\begin{tikzpicture}
\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
{\normalsize
\begin{minipage}{11cm}
\begin{quote}\rm
\begin{itemize}
\item TMs are a fantastic model of low-level code
\item completely unstructured\makebox[0mm][10mm]{\mbox{}}\;\;
\only<2>{\textcolor{cream}{\fontspec{Chalkduster}Spaghetti Code}}%
\only<3->{\textcolor{red}{\fontspec{Chalkduster}Spaghetti Code}}
\bigskip
\item good testbed for verification techniques
\item Can we verify a program with 38 Mio instructions?
\item we can delay implementing a concrete machine model (for OS/low-level code verification)
\end{itemize}
\end{quote}
\end{minipage}};
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{
\begin{tabular}{c}Some Previous Works\\[-5mm]
\hspace{3.5cm}\small (but not interested in low-level code)
\end{tabular}}%
\begin{itemize}
\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 his work}
\item \textcolor{gray}{some proofs use TMs (Wang tilings)}
\end{itemize}
\bigskip
\item Asperti and Ricciotti formalised TMs in Matita\smallskip
\begin{itemize}
\item \textcolor{gray}{no undecidability result $\Rightarrow$ interest in complexity}
\item \textcolor{gray}{their UTM operates on a different alphabet than the TMs it simulates}
\begin{quote}
\textcolor{gray}{"In particular, the fact that the universal machine operates with a different
alphabet with respect to the machines it simulates is annoying." (Asperti and Ricciotti)}
\end{quote}
\end{itemize}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
\tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
\tikzstyle{node1}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
draw=black!50, top color=white, bottom color=black!20]
\tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
draw=red!70, top color=white, bottom color=red!50!black!20]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{The Big Picture}%
\mbox{}\\[19mm]
\begin{center}
\begin{tikzpicture}
\matrix[ampersand replacement=\&,column sep=13mm, row sep=5mm]
{ \node (tm) [node1] {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; \&
\node (reg) [node1] {\begin{tabular}{c}Register\\Machines\end{tabular}}; \&
\node (rf) [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\
};
\only<2->{\draw[->,black!50,line width=2mm] (reg) -- (tm);}
\only<2->{\draw[<-,black!50,line width=2mm] (reg) -- (rf);}
\only<4->{
\draw [<-, black!50,line width=2mm, rounded corners]
% start right of digit.east, that is, at the point that is the
% linear combination of digit.east and the vector (2mm,0pt). We
% use the ($ ... $) notation for computing linear combinations
($ (rf.south) + (0mm,0) $)
% Now go down
-- ++(0,-2.5)
% And back to the left of digit.west
-| ($ (tm.south) - (0mm,0) $);}
\end{tikzpicture}
\end{center}
\only<1->{
\begin{textblock}{3}(1,4.9)
\begin{tikzpicture}
\draw (0,0) node {\small\begin{tabular}{l}undecidability\\of the halting\\ problem\end{tabular}};
\end{tikzpicture}
\end{textblock}}
\only<2->{
\begin{textblock}{3}(8.3,8.4)
\begin{tikzpicture}
\node at (0,0) [single arrow, shape border rotate=90, fill=black!50,text=white]{};
\draw (0,-1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};
\end{tikzpicture}
\end{textblock}
\begin{textblock}{3}(3.1,8.4)
\begin{tikzpicture}
\node at (0,0) [single arrow, shape border rotate=90, fill=black!50,text=white]{};
\draw (0,-1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};
\end{tikzpicture}
\end{textblock}}
\only<3->{
\begin{textblock}{4}(12.5,5.8)
\begin{tikzpicture}
\draw (0,0) node {\begin{tabular}{l}UF\end{tabular}};
\end{tikzpicture}
\end{textblock}}
\only<4->{
\begin{textblock}{4}(3.3,13.3)
\begin{tikzpicture}
\draw (0,0) node {\begin{tabular}{l}a correct UTM by translation\end{tabular}};
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Turing Machines}%
\begin{itemize}
\item tapes are lists and contain @{text 0}s or @{text 1}s only
\begin{center}
\begin{tikzpicture}[scale=1]
\draw[very thick] (-3.0,0) -- ( 3.0,0);
\draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
\draw[very thick] (-1.75,0) -- (-1.75,0.5);
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
\draw[very thick] ( 3.0,0) -- ( 3.0,0.5);
\draw[very thick] (-3.0,0) -- (-3.0,0.5);
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
\draw[fill] (1.35,0.1) rectangle (1.65,0.4);
\draw[fill] (0.85,0.1) rectangle (1.15,0.4);
\draw[fill] (-0.35,0.1) rectangle (-0.65,0.4);
\draw[fill] (-1.65,0.1) rectangle (-1.35,0.4);
\draw (-0.25,0.8) -- (-0.25,-0.8);
\draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
\node [anchor=base] at (-0.85,-0.5) {\small left list\;\;\;\;\mbox{}};
\node [anchor=base] at (0.40,-0.5) {\small \mbox{}\;\;\;\;right list};
\node [anchor=base] at (0.1,0.7) {\small \;\;head};
\node [anchor=base] at (-2.2,0.2) {\ldots};
\node [anchor=base] at ( 2.3,0.2) {\ldots};
\end{tikzpicture}
\end{center}\pause
\item @{text steps} function:
\begin{quote}\rm
What does the TM calculate after it has executed @{text n} steps?
\end{quote}\pause
\item designate the @{text 0}-state as "halting state" and remain there
forever, i.e.~have a @{text Nop}-action
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Register Machines}%
\begin{itemize}
\item programs are lists of instructions
\begin{center}
\begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}
@{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 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}
\end{center}
\end{itemize}
\only<2->{
\begin{textblock}{4}(0.3,11.8)
\begin{tikzpicture}
\node[ellipse callout, fill=red, callout absolute pointer={(-0.2,1)}]
at (0, 0){\large\fontspec{Chalkduster}\textcolor{yellow}{Spaghetti Code!}};
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Recursive Functions}%
\begin{itemize}
\item[]
\begin{center}
\begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}
@{text "rec"} & $::=$ & @{term "Z"} & \textcolor{black!60}{zero-function}\\[1mm]
& $\mid$ & @{term "S"} & \textcolor{black!60}{successor-function}\\[1mm]
& $\mid$ & @{term "id n m"} & \textcolor{black!60}{projection}\\[1mm]
& $\mid$ & @{term "Cn n f gs"} & \textcolor{black!60}{composition}\\[1mm]
& $\mid$ & @{term "Pr n f g"} & \textcolor{black!60}{primitive recursion}\\[1mm]
& $\mid$ & @{term "Mn n f"} & \textcolor{black!60}{minimisation}
\end{tabular}
\end{center}\bigskip
\item @{text "eval :: rec \<Rightarrow> nat list \<Rightarrow> nat"}\\
\hspace{3mm}can be defined by recursion (HOL has @{term "Least"})
\item \small you define
\begin{itemize}
\item addition, multiplication, logical operations, quantifiers\ldots
\item coding of numbers (Cantor encoding), UF
\end{itemize}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Copy Turing Machine}%
\begin{itemize}
\item TM that copies a number on the input tape
\begin{center}
@{text "copy \<equiv> cbegin ; cloop ; cend"}
\end{center}\smallskip
\begin{center}
\begin{tikzpicture}[scale=0.7]
\node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
\node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
\node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
\node [anchor=base] at (2.2,-0.8) {\small$\overbrace{@{text cbegin}}^{}$};
\node [anchor=base] at (5.6,-0.8) {\small$\overbrace{@{text cloop}}^{}$};
\node [anchor=base] at (10.5,-0.8) {\small$\overbrace{@{text cend}}^{}$};
\begin{scope}[shift={(0.5,0)}]
\draw[very thick] (-0.25,0) -- ( 1.25,0);
\draw[very thick] (-0.25,0.5) -- ( 1.25,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
\end{scope}
\begin{scope}[shift={(2.9,0)}]
\draw[very thick] (-0.25,0) -- ( 2.25,0);
\draw[very thick] (-0.25,0.5) -- ( 2.25,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
\draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
\end{scope}
\begin{scope}[shift={(6.8,0)}]
\draw[very thick] (-0.75,0) -- ( 3.25,0);
\draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
\draw[fill] ( 2.85,0.1) rectangle (3.15,0.4);
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
\end{scope}
\begin{scope}[shift={(11.7,0)}]
\draw[very thick] (-0.75,0) -- ( 3.25,0);
\draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
\draw[fill] ( 2.85,0.1) rectangle (3.15,0.4);
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
\end{scope}
\end{tikzpicture}
\end{center}\bigskip
\footnotesize
\begin{center}
\begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c}
\begin{tabular}[t]{@ {}l@ {}}
@{text cbegin} @{text "\<equiv>"}\\
\hspace{2mm}@{text "["}@{text "(W\<^bsub>0\<^esub>, 0), (R, 2), (R, 3),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>1\<^esub>, 3), (L, 4),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"}
\end{tabular}
&
\begin{tabular}[t]{@ {}l@ {}}
@{text cloop} @{text "\<equiv>"}\\
\hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>0\<^esub>, 2), (R, 3), (R, 4),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>1\<^esub>, 5), (R, 4), (L, 6),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"}
\end{tabular}
&
\begin{tabular}[t]{@ {}l@ {}}
@{text cend} @{text "\<equiv>"}\\
\hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>1\<^esub>, 3),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>0\<^esub>, 4), (R, 0),"}\\
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"}
\end{tabular}
\end{tabular}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Dither Machine}%
\begin{itemize}
\item TM that is the identity with @{text "1"} and loops with @{text "0"}
\smallskip
\begin{center}
\begin{tabular}{l@ {\hspace{3mm}}lcl}
& \multicolumn{1}{c}{start tape}\\[1mm]
\raisebox{2mm}{halting case:} &
\begin{tikzpicture}[scale=0.8]
\draw[very thick] (-2,0) -- ( 0.75,0);
\draw[very thick] (-2,0.5) -- ( 0.75,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
\node [anchor=base] at (-1.7,0.2) {\ldots};
\end{tikzpicture}
& \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
\begin{tikzpicture}[scale=0.8]
\draw[very thick] (-2,0) -- ( 0.75,0);
\draw[very thick] (-2,0.5) -- ( 0.75,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
\node [anchor=base] at (-1.7,0.2) {\ldots};
\end{tikzpicture}\\
\raisebox{2mm}{non-halting case:} &
\begin{tikzpicture}[scale=0.8]
\draw[very thick] (-2,0) -- ( 0.25,0);
\draw[very thick] (-2,0.5) -- ( 0.25,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\node [anchor=base] at (-1.7,0.2) {\ldots};
\end{tikzpicture}
& \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
\raisebox{2mm}{loops}
\end{tabular}
\end{center}\bigskip
\small
\begin{center}
\begin{tabular}[t]{@ {}l@ {}}
@{text dither} @{text "\<equiv>"} @{text "["}@{text "(W\<^bsub>0\<^esub>, 1), (R, 2), (L, 1), (L, 0)"}@{text "]"}
\end{tabular}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
\definecolor{mygrey}{rgb}{.80,.80,.80}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Hoare Logic for TMs}%
\begin{itemize}
\item Hoare-triples\onslide<2>{ and Hoare-pairs:}
\small
\begin{center}
\begin{tabular}{@ {\hspace{-6mm}}c@ {\hspace{-3mm}}c@ {}}
\begin{tabular}[t]{@ {}l@ {}}
\colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
\hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\
\hspace{7mm}if @{term "P tp"} holds then\\
\hspace{7mm}@{text "\<exists>"}@{term n}. such that\\
\hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\
\hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"}
\end{tabular} &
\onslide<2>{
\begin{tabular}[t]{@ {}l@ {}}
\colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
\hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\
\hspace{7mm}if @{term "P tp"} holds then\\
\hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"}
\end{tabular}}
\end{tabular}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
(*<*)
lemmas HR1 =
Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^sub>1" and B="p\<^sub>2"]
lemmas HR2 =
Hoare_plus_unhalt[where ?A="p\<^sub>1" and B="p\<^sub>2"]
(*>*)
text_raw {*
\definecolor{mygrey}{rgb}{.80,.80,.80}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Some Derived Rules}%
\large
\begin{center}
@{thm[mode=Rule] Hoare_consequence}\bigskip\bigskip\\
\begin{tabular}{@ {\hspace{-5mm}}c@ {\hspace{4mm}}c@ {}}
$\inferrule*
{@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}}
{@{thm (concl) HR1}}
$ &
$
\inferrule*
{@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}
{@{thm (concl) HR2}}
$
\end{tabular}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[b]
\frametitle{Undecidability}%
\begin{textblock}{7}(4,2.4)
@{thm tcontra_def}
\end{textblock}
\only<2>{
\begin{itemize}
\item Suppose @{text H} decides whether @{text contra} called with the code
of @{text contra} halts, then\smallskip
\begin{center}\small
\begin{tabular}{@ {}l@ {}}
\begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}}
@{term "P\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
@{term "P\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
@{term "P\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
\end{tabular}\bigskip\bigskip
\\
\begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}
$\inferrule*{
\inferrule*{@{term "{P\<^sub>1} tcopy {P\<^sub>2}"} \\ @{term "{P\<^sub>2} H {P\<^sub>3}"}}
{@{term "{P\<^sub>1} (tcopy |+| H) {P\<^sub>3}"}}
\\ @{term "{P\<^sub>3} dither \<up>"}
}
{@{term "{P\<^sub>1} tcontra \<up>"}}
$
\end{tabular}
\end{tabular}
\end{center}
\end{itemize}}
\only<3>{
\begin{itemize}
\item Suppose @{text H} decides wether @{text contra} called with the code
of @{text contra} does \alert{not} halt, then\\[-8mm]\mbox{}
\begin{center}\small
\begin{tabular}{@ {}l@ {}}
\begin{tabular}[t]{@ {\hspace{-1mm}}l@ {}}
@{term "Q\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
@{term "Q\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
@{term "Q\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
\end{tabular}\bigskip\bigskip
\\
\begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}
$\inferrule*{
\inferrule*{@{term "{Q\<^sub>1} tcopy {Q\<^sub>2}"} \\ @{term "{Q\<^sub>2} H {Q\<^sub>3}"}}
{@{term "{Q\<^sub>1} (tcopy |+| H) {Q\<^sub>3}"}}
\\ @{term "{Q\<^sub>3} dither {Q\<^sub>3}"}
}
{@{term "{Q\<^sub>1} tcontra {Q\<^sub>3}"}}
$
\end{tabular}
\end{tabular}
\end{center}
\end{itemize}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
\definecolor{mygrey}{rgb}{.80,.80,.80}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Hoare Reasoning}%
\begin{itemize}
\item reasoning is quite demanding, e.g.~the invariants
of the copy-machine:\\[-5mm]\mbox{}
\footnotesize
\begin{center}
\begin{tabular}{@ {\hspace{-5mm}}c@ {}}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {\hspace{-0.9cm}}l@ {}}
\hline
@{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
@{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
@{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
@{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
@{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
& & @{thm (rhs) inv_begin02}\smallskip \\
\hline
@{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
& & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
@{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\
\hline
@{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\
@{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\
\hline
\end{tabular}
\end{tabular}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Midway Conclusion}%
\begin{itemize}
\item feels awfully like reasoning about machine code
\item compositional constructions / reasoning is not at all frictionless
\item sizes
\begin{center}
\begin{tabular}{ll}
& sizes:\smallskip\\
UF & @{text 140843} constructors\\
URM & @{text 2} Mio instructions\\
UTM & @{text 38} Mio states\\
\end{tabular}
\end{center}\smallskip
\end{itemize}
\only<1>{
\begin{textblock}{4}(2,13.9)
\begin{tikzpicture}
\draw (0,0) node {\small\begin{tabular}{l}$^\star$old version:
URM (@{text 12} Mio) UTM (@{text 112} Mio)\end{tabular}};
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{{\fontsize{20}{20}\selectfont{}The Trouble With Hoare-Triples}}%
\begin{itemize}
\item Whenever we wanted to prove
\begin{center}
\large @{text "{P} p {Q}"}
\end{center}\bigskip\medskip
\item[@{text "(1)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy)}
\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}
\alert{very little opportunity for automation}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\begin{tabular}{@ {}c@ {}}\Large Inspiration from other Works\end{tabular}}%
\onslide<3->{
\begin{itemize}
\item Jensen, Benton, Kennedy ({\bf 2013}),
{\it High-Level Separation Logic for Low-Level Code}\medskip\\
\item Myreen ({\bf 2008}), {\it Formal Verification of Machine-Code Programs},
PhD thesis\medskip
\item Klein, Kolanski, Boyton ({\bf 2012}), {\it Mechanised Separation Algebra}
\end{itemize}}
\only<2->{
\begin{textblock}{4}(1.4,0.9)
\begin{tikzpicture}
\draw (0,0) node {\fontspec{Chalkduster}\textcolor{red!80}{\LARGE Stealing}};
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Better Composability}%
\begin{itemize}
\item an idea from Jensen, Benton \& Kennedy who looked at X86
assembler programs and macros\bigskip
\item assembler for TMs:\medskip
\begin{center}
\begin{tabular}{l}
@{text "move_one_left"} @{text "\<equiv>"}\\
\hspace{13mm} @{text "\<Lambda> exit."}\\
\hspace{16mm} @{text "Inst (L, exit) (L, exit)"} @{text ";"}\\
\hspace{16mm} @{text "Label exit"}\\
\end{tabular}
\end{center}\bigskip\bigskip
\begin{tabular}{l}
$\Rightarrow$ represent "state" labels as functions\\
\phantom{$\Rightarrow$} (with bound variables $\Rightarrow$ locality)
\end{tabular}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Better Composability}%
\begin{center}
\begin{tabular}{@ {\hspace{-10mm}}l}
@{text "move_left_until_zero"} @{text "\<equiv>"} \\
\hspace{31mm} @{text "\<Lambda> start exit."}\\
\hspace{36mm} @{text "Label start"} @{text ";"}\\
\hspace{36mm} @{text "if_zero exit"} @{text ";"}\\
\hspace{36mm} @{text "move_left"} @{text ";"}\\
\hspace{36mm} @{text "jmp start"} @{text ";"}\\
\hspace{36mm} @{text "Label exit"}\\
\end{tabular}
\end{center}
\small
\begin{tabular}{l}
@{text "if_zero e \<equiv> \<Lambda> exit. Inst (W\<^sub>0, e), (W\<^sub>1, exit); Label exit"}\\
\hspace{5mm}@{text "jmp e \<equiv> Inst (W\<^sub>0, e), (W\<^sub>1, e)"}
\end{tabular}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{An RM-API with TMs}%
\begin{center}
\begin{tikzpicture}
\matrix[ampersand replacement=\&,column sep=13mm, row sep=5mm]
{ \node (tm) [node1, minimum size=44mm] {\mbox{}}; \&
\node (rf) [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\
};
\draw[->,black!50,line width=2mm] (rf) -- (tm);
\node [above, rotate=90] at (tm.east) {\textcolor{gray}{Reg.Mach. API}};
\node [below right] at (tm.north west) {\textcolor{gray}{Macros}};
\node [node1] at (tm) {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}};
\end{tikzpicture}
\end{center}
\begin{itemize}
\item Suppose the first four registers of an RM contain 1,2,0 and 3, then the encoding is
\begin{center}
\begin{tikzpicture}[scale=1]
\draw[very thick] (-0.25,0) -- ( 8.25,0);
\draw[very thick] (-0.25,0.5) -- ( 8.25,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
\draw[very thick] ( 3.75,0) -- ( 3.75,0.5);
\draw[very thick] ( 4.25,0) -- ( 4.25,0.5);
\draw[very thick] ( 4.75,0) -- ( 4.75,0.5);
\draw[very thick] ( 5.25,0) -- ( 5.25,0.5);
\draw[very thick] ( 5.75,0) -- ( 5.75,0.5);
\draw[very thick] ( 6.25,0) -- ( 6.25,0.5);
\draw[very thick] ( 6.75,0) -- ( 6.75,0.5);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
\draw[fill] ( 1.35,0.1) rectangle (1.65,0.4);
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
\draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
\draw[fill] ( 3.35,0.1) rectangle (3.65,0.4);
\draw[fill] ( 4.35,0.1) rectangle (4.65,0.4);
\draw[fill] ( 4.85,0.1) rectangle (5.15,0.4);
\draw[fill] ( 5.35,0.1) rectangle (5.65,0.4);
\draw[fill] ( 5.85,0.1) rectangle (6.15,0.4);
\end{tikzpicture}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Inc a}%
\begin{center}
\begin{tabular}{@ {\hspace{-10mm}}l}
@{text "Inc a"} @{text "\<equiv>"} \\
\hspace{16mm} @{text "locate a"} @{text ";"}\\
\hspace{16mm} @{text "right_until_zero"} @{text ";"}\\
\hspace{16mm} @{text "move_right"} @{text ";"}\\
\hspace{16mm} @{text "shift_right"} @{text ";"}\\
\hspace{16mm} @{text "move_left"} @{text ";"}\\
\hspace{16mm} @{text "left_until_double_zero"} @{text ";"}\\
\hspace{16mm} @{text "write_one"} @{text ";"}\\
\hspace{16mm} @{text "left_until_double_zero"} @{text ";"}\\
\hspace{16mm} @{text "move_right"} @{text ";"}\\
\hspace{16mm} @{text "move_right"}\\
\end{tabular}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Separation Algebra}%
\begin{itemize}
\item use some infrastructure introduced by Klein et al in Isabelle/HOL
\item and an idea by Myreen\bigskip\bigskip
\begin{center}
\large @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"}\bigskip\bigskip
\end{center}
\item[] @{text "p, c, q"} will be assertions in a separation logic\pause
\begin{center}
e.g.~~@{text "\<lbrace>st i \<star> hd n \<star> ones u v \<star> zero (v + 1)\<rbrace>"}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Separation Triples}%
\Large
\begin{center}
\begin{tabular}{l@ {\hspace{-10mm}}l}
@{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"} @{text "\<equiv>"}\smallskip\\
& @{text "\<forall> cf r."}\\
& \hspace{3mm} @{text "(p \<star> c \<star> r) cf"} implies\\
& \hspace{3mm} @{text "\<exists> k. "} @{text "(q \<star> c \<star> r) (steps k cf)"}
\end{tabular}
\end{center}\bigskip\bigskip
\normalsize
\begin{center}
@{text "\<lbrace> st i \<star> hd v \<star> zero u \<star> ones (u + 1) v \<rbrace>"}\\
@{text "i:[left_until_zero]:j"}\\
@{text "\<lbrace> st j \<star> hd u \<star> zero u \<star> ones (u + 1) v \<rbrace>"}\\
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Inductions over \textit{ones}}%
\begin{itemize}
\item What most simplifies the work is that we can do inductions over
the ''input'' (inductively defined assertions)\pause\medskip
\item Suppose @{text "right_until_zero"}:\bigskip
\begin{center}
\begin{tikzpicture}[scale=1]
\draw[very thick] (-0.25,0) -- ( 8.25,0);
\draw[very thick] (-0.25,0.5) -- ( 8.25,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
\draw[very thick] ( 3.75,0) -- ( 3.75,0.5);
\draw[very thick] ( 4.25,0) -- ( 4.25,0.5);
\draw[very thick] ( 4.75,0) -- ( 4.75,0.5);
\draw[very thick] ( 5.25,0) -- ( 5.25,0.5);
\draw[very thick] ( 5.75,0) -- ( 5.75,0.5);
\draw[very thick] ( 6.25,0) -- ( 6.25,0.5);
\draw[very thick] ( 6.75,0) -- ( 6.75,0.5);
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
\draw[fill] ( 1.35,0.1) rectangle (1.65,0.4);
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
\draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
\draw[fill] ( 3.35,0.1) rectangle (3.65,0.4);
\draw[fill] ( 3.85,0.1) rectangle (4.15,0.4);
\draw[fill] ( 4.35,0.1) rectangle (4.65,0.4);
\draw[fill] ( 4.85,0.1) rectangle (5.15,0.4);
\draw[fill] ( 5.35,0.1) rectangle (5.65,0.4);
\draw[fill] ( 5.85,0.1) rectangle (6.15,0.4);
\path (2.75,0) edge [decorate,decoration={brace,amplitude=14pt}, thick] node[below=8pt]
{\small\textcolor{gray}{@{text "ones u v"}}} (-0.25,0);
\end{tikzpicture}
\end{center}
\begin{center}
@{text "\<lbrace> st i \<star> hd u \<star> zero (v + 1) \<star> ones u v \<rbrace>"}\\
@{text "i:[right_until_zero]:j"}\\
@{text "\<lbrace> st j \<star> hd (v + 1) \<star> zero (v + 1) \<star> ones u v \<rbrace>"}\\
\end{center}
\end{itemize}
\begin{textblock}{3}(11,10)
\begin{tikzpicture}
\only<2>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};}
\end{tikzpicture}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Automation}%
\begin{itemize}
\item we introduced some tactics for handling sequential programs\bigskip
\begin{center}
@{text "\<lbrace>p\<rbrace> i:[c\<^sub>1 ; ... ; c\<^sub>n]:j \<lbrace>q\<rbrace>"}
\end{center}\bigskip\bigskip
\item for loops we often only have to do inductions on the length
of the input (e.g.~how many @{text "0"}s/@{text "1"}s are on the tape)
\item no termination measures are needed
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Register Machines}%
\begin{itemize}
\item We could also use Jensen's et al work to give
a more appropriate \alert{view} on register machines
\begin{center}
@{text "\<lbrace>p\<rbrace> i:[rm_c]:j \<lbrace>q\<rbrace>"}
\end{center}\bigskip
\end{itemize}
\small
\begin{itemize}
\item Rule for @{text "Inc"}
\begin{tabular}{rl}
@{text "RM."} & @{text "\<lbrace> pc i \<star> m a v \<rbrace>"} \\
& @{text "i:[ Inc a ]:j"} \\
& @{text "\<lbrace> pc j \<star> m a (Suc v)\<rbrace>"}
\end{tabular}
\item Rules for @{text "Dec"}
\begin{tabular}{c c}
\begin{tabular}{r l}
@{text "RM."} & @{text "\<lbrace>(pc i \<star> m a (Suc v))\<rbrace>"} \\
& @{text "i :[ Dec a e ]: j"} \\
& @{text "\<lbrace>pc j \<star> m a v\<rbrace>"}
\end{tabular} &
\begin{tabular}{r l}
@{text "RM."} & @{text "\<lbrace> pc i \<star> m a 0 \<rbrace>"} \\
& @{text "i:[ Dec a e ]:j"} \\
& @{text "\<lbrace> pc e \<star> m a 0 \<rbrace>"}
\end{tabular}
\end{tabular}
%\item Rule for @{text "Goto"}
%
% \begin{tabular}{r l}
% @{text "RM."} & @{text "\<lbrace> pc i \<rbrace>"} \\
% &@{text "i:[ (Goto e) ]:j"} \\
% &@{text "\<lbrace> pc e \<rbrace>"}
% \end{tabular}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Conclusion}%
\begin{itemize}
\item What started out as a student project, turned out to be much more
fun than first thought.\bigskip
\item Where can you claim that you proved the correctness of
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).\bigskip
\item The existing literature on TMs \& RMs leave out quite a bit of the story
(not to mention contains bugs).
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
(*<*)
end
end
(*>*)