1 (*<*)

     2 theory Slides3

     3 imports "../thys/UTM" "../thys/Abacus_Defs"

     4 begin

     5 declare [[show_question_marks = false]]

     6 

     7 hide_const (open) s 

     8 

     9 abbreviation

    10   "update2 p a \<equiv> update a p"

    11 

    12 notation (Rule output)

    13   "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")

    14 

    15 syntax (Rule output)

    16   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

    17   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")

    18 

    19   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 

    20   ("\<^raw:\mbox{>_\<^raw:}\\>/ _")

    21 

    22   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

    23 

    24 notation (Axiom output)

    25   "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")

    26 

    27 notation (IfThen output)

    28   "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

    29 syntax (IfThen output)

    30   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

    31   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

    32   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

    33   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

    34 

    35 notation (IfThenNoBox output)

    36   "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

    37 syntax (IfThenNoBox output)

    38   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

    39   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

    40   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

    41   "_asm" :: "prop \<Rightarrow> asms" ("_")

    42 

    43 context uncomputable

    44 begin

    45 

    46 notation (latex output)

    47   Cons ("_::_" [48,47] 68) and

    48   append ("_@_" [65, 64] 65) and

    49   Oc ("1") and

    50   Bk ("0") and

    51   exponent ("_\<^bsup>_\<^esup>" [107] 109) and

    52   inv_begin0 ("I\<^sub>0") and

    53   inv_begin1 ("I\<^sub>1") and

    54   inv_begin2 ("I\<^sub>2") and

    55   inv_begin3 ("I\<^sub>3") and

    56   inv_begin4 ("I\<^sub>4") and 

    57   inv_begin ("I\<^bsub>cbegin\<^esub>") and

    58   inv_loop1 ("J\<^sub>1") and

    59   inv_loop0 ("J\<^sub>0") and

    60   inv_end1 ("K\<^sub>1") and

    61   inv_end0 ("K\<^sub>0") and

    62   recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^sup>_\<^raw:}>\<^sub>_") and

    63   Pr ("Pr\<^sup>_") and

    64   Cn ("Cn\<^sup>_") and

    65   Mn ("Mn\<^sup>_") and

    66   tcopy ("copy") and 

    67   tcontra ("contra") and

    68   tape_of ("\<langle>_\<rangle>") and 

    69   code_tcontra ("code contra") and

    70   tm_comp ("_ ; _") 

    71 

    72  

    73 lemma inv_begin_print:

    74   shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and

    75         "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and 

    76         "s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and 

    77         "s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and 

    78         "s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and

    79         "s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"

    80 apply(case_tac [!] tp)

    81 by (auto)

    82 

    83 

    84 lemma inv1: 

    85   shows "0 < (n::nat) \<Longrightarrow> Turing_Hoare.assert_imp (inv_begin0 n) (inv_loop1 n)"

    86 unfolding Turing_Hoare.assert_imp_def

    87 unfolding inv_loop1.simps inv_begin0.simps

    88 apply(auto)

    89 apply(rule_tac x="1" in exI)

    90 apply(auto simp add: replicate.simps)

    91 done

    92 

    93 lemma inv2: 

    94   shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"

    95 apply(rule ext)

    96 apply(case_tac x)

    97 apply(simp add: inv_end1.simps)

    98 done

    99 

   100 

   101 lemma measure_begin_print:

   102   shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and

   103         "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and

   104         "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and 

   105         "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"

   106 by (simp_all)

   107 

   108 lemma inv_begin01:

   109   assumes "n > 1"

   110   shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"

   111 using assms by auto                          

   112 

   113 lemma inv_begin02:

   114   assumes "n = 1"

   115   shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"

   116 using assms by auto

   117 

   118 (*>*)

   119 

   120 

   121 

   122 text_raw {*

   123   \renewcommand{\slidecaption}{ITP, 24 July 2013}

   124   \newcommand{\bl}[1]{#1}                        

   125   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   126   \mode<presentation>{

   127   \begin{frame}

   128   \frametitle{%

   129   \begin{tabular}{@ {}c@ {}}

   130   \\[-3mm]

   131   {\fontsize{20}{20}\selectfont{}Mechanising Turing Machines and}\\[-2mm] 

   132   {\fontsize{20}{20}\selectfont{}Computability Theory in Isabelle}\\[-3mm] 

   133   \end{tabular}}

   134   

   135   \bigskip\medskip\medskip

   136  

   137   \begin{center}

   138   \begin{tabular}{c@ {\hspace{1cm}}c}

   139   \includegraphics[scale=0.29]{jian.jpg}  &

   140   \includegraphics[scale=0.034]{xingyuan.jpg} \\

   141   Jian Xu & Xingyuan Zhang\\[-3mm]

   142   \end{tabular}\\[3mm]

   143   \small PLA University of Science and Technology

   144   \end{center}

   145 

   146   \begin{center}

   147   Christian Urban\\[0mm]

   148   \small King's College London

   149   \end{center}

   150   \end{frame}}

   151   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   152 *}

   153 

   154 

   155 text_raw {*

   156   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   157   \mode<presentation>{

   158   \begin{frame}[c]

   159   \frametitle{Why Turing Machines?}%

   160 

   161   \begin{itemize}

   162   \item At the beginning, it was just a student project

   163   about computability.\smallskip

   164 

   165   \begin{center}

   166   \begin{tabular}{c}

   167   \includegraphics[scale=0.3]{boolos.jpg}\\[-2mm]

   168   \footnotesize Computability and Logic (5th.~ed)\\[-2mm]

   169   \footnotesize Boolos, Burgess and Jeffrey\\[2mm]

   170   \end{tabular}

   171   \end{center}

   172 

   173   \item found an inconsistency in the definition of halting computations

   174   (Chap.~3 vs Chap.~8)

   175   \end{itemize}

   176 

   177   \end{frame}}

   178   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   179 *}

   180 

   181 text_raw {*

   182   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   183   \mode<presentation>{

   184   \begin{frame}[c]

   185   \frametitle{Some Previous Works}%

   186 

   187   \begin{itemize}

   188   \item Norrish formalised computability theory in HOL starting

   189   from the lambda-calculus\smallskip 

   190   \begin{itemize}

   191   \item \textcolor{gray}{for technical reasons we could not follow his work}

   192   \item \textcolor{gray}{some proofs use TMs (Wang tilings)}

   193   \end{itemize}

   194   \bigskip

   195 

   196   \item Asperti and Ricciotti formalised TMs in Matita\smallskip

   197   \begin{itemize}

   198   \item \textcolor{gray}{no undecidability result $\Rightarrow$ interest in complexity}

   199   \item \textcolor{gray}{their UTM operates on a different alphabet than the TMs it simulates}

   200   \begin{quote}

   201   \textcolor{gray}{"In particular, the fact that the universal machine operates with a different 

   202   alphabet with respect to the machines it simulates is annoying." [Asperti and Ricciotti]}

   203   \end{quote}

   204   \end{itemize}

   205   \end{itemize}

   206 

   207   \end{frame}}

   208   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   209 *}

   210 

   211 text_raw {*

   212   \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]

   213   \tikzstyle{node1}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 

   214                      draw=black!50, top color=white, bottom color=black!20]

   215   \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 

   216                      draw=red!70, top color=white, bottom color=red!50!black!20]

   217   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   218   \mode<presentation>{

   219   \begin{frame}[c]

   220   \frametitle{The Big Picture}%

   221 

   222   \begin{center}

   223   \begin{tikzpicture}

   224   \matrix[ampersand replacement=\&,column sep=13mm, row sep=5mm]

   225   { \node (def1)   [node1] {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; \&

   226     \node (proof1) [node1] {\begin{tabular}{c}Register\\Machines\end{tabular}}; \&

   227     \node (alg1)   [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\    

   228   };

   229 

   230   \draw[->,black!50,line width=2mm] (proof1) -- (def1);

   231   \draw[<-,black!50,line width=2mm] (proof1) -- (alg1);

   232   

   233   \end{tikzpicture}

   234   \end{center}

   235 

   236   \only<2->{

   237   \begin{textblock}{3}(8.3,4.0)

   238   \begin{tikzpicture}

   239   \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};

   240   \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};

   241   \end{tikzpicture}

   242   \end{textblock}

   243 

   244   \begin{textblock}{3}(3.1,4.0)

   245   \begin{tikzpicture}

   246   \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};

   247   \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};

   248   \end{tikzpicture}

   249   \end{textblock}}

   250 

   251   \only<3->{

   252   \begin{textblock}{4}(10.9,9.4)

   253   \begin{tikzpicture}

   254   \draw (0,0) node {\begin{tabular}{l}UF\end{tabular}};

   255   \end{tikzpicture}

   256   \end{textblock}

   257 

   258   \begin{textblock}{3}(1,10.0)

   259   \begin{tikzpicture}

   260   \draw (0,0) node {\small\begin{tabular}{l}undecidability\\of the halting\\ problem\end{tabular}};

   261   \end{tikzpicture}

   262   \end{textblock}}

   263 

   264   \only<4->{

   265   \begin{textblock}{4}(4.2,12.4)

   266   \begin{tikzpicture}

   267   \draw (0,0) node {\begin{tabular}{l}a correct UTM by translation\end{tabular}};

   268   \end{tikzpicture}

   269   \end{textblock}}

   270 

   271   \end{frame}}

   272   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   273 *}

   274 

   275 text_raw {*

   276   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   277   \mode<presentation>{

   278   \begin{frame}[c]

   279   \frametitle{Turing Machines}%

   280 

   281   \begin{itemize}

   282   \item tapes are lists and contain @{text 0}s or @{text 1}s only

   283 

   284   \begin{center}

   285 \begin{tikzpicture}[scale=1]

   286   \draw[very thick] (-3.0,0)   -- ( 3.0,0);

   287   \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);

   288   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

   289   \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

   290   \draw[very thick] (-0.75,0)   -- (-0.75,0.5);

   291   \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

   292   \draw[very thick] (-1.25,0)   -- (-1.25,0.5);

   293   \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

   294   \draw[very thick] (-1.75,0)   -- (-1.75,0.5);

   295   \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);

   296   \draw[very thick] ( 3.0,0)   -- ( 3.0,0.5);

   297   \draw[very thick] (-3.0,0)   -- (-3.0,0.5);

   298   \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);

   299   \draw[fill]     (1.35,0.1) rectangle (1.65,0.4);

   300   \draw[fill]     (0.85,0.1) rectangle (1.15,0.4);

   301   \draw[fill]     (-0.35,0.1) rectangle (-0.65,0.4);

   302   \draw[fill]     (-1.65,0.1) rectangle (-1.35,0.4);

   303   \draw (-0.25,0.8) -- (-0.25,-0.8);

   304   \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);

   305   \node [anchor=base] at (-0.85,-0.5) {\small left list\;\;\;\;\mbox{}};

   306   \node [anchor=base] at (0.40,-0.5) {\small \mbox{}\;\;\;\;right list};

   307   \node [anchor=base] at (0.1,0.7) {\small \;\;head};

   308   \node [anchor=base] at (-2.2,0.2) {\ldots};

   309   \node [anchor=base] at ( 2.3,0.2) {\ldots};

   310   \end{tikzpicture}

   311   \end{center}\pause

   312 

   313   \item @{text steps} function:

   314 

   315   \begin{quote}\rm

   316   What does the TM calculate after it has executed @{text n} steps?

   317   \end{quote}\pause

   318 

   319   \item designate the @{text 0}-state as "halting state" and remain there 

   320   forever, i.e.~have a @{text Nop}-action

   321   \end{itemize}

   322 

   323   \end{frame}}

   324   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   325 *}

   326 

   327 text_raw {*

   328   

   329 

   330   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   331   \mode<presentation>{

   332   \begin{frame}[c]

   333   \frametitle{Register Machines}%

   334 

   335   \begin{itemize}

   336   \item programs are lists of instructions

   337 

   338   \begin{center}

   339   \begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}

   340   @{text "I"} & $::=$  & @{term "Goto L\<iota>"}

   341   & \textcolor{black!60}{jump to instruction @{text L}}\\[1mm]

   342   & $\mid$ & @{term "Inc R\<iota>"} & \textcolor{black!60}{increment register @{text "R"} by one}\\[1mm]

   343   & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & \textcolor{black!60}{if the content of @{text R} is non-zero,}\\

   344   & & & \textcolor{black!60}{then decrement it by one}\\

   345   & & & \textcolor{black!60}{otherwise jump to instruction @{text L}}

   346   \end{tabular}

   347   \end{center}

   348   \end{itemize}

   349 

   350   \only<2->{

   351   \begin{textblock}{4}(0.3,11.8)

   352   \begin{tikzpicture}

   353   \node[ellipse callout, fill=red, callout absolute pointer={(-0.2,1)}] 

   354    at (0, 0){\large\fontspec{Chalkduster}\textcolor{yellow}{Spaghetti Code!}};

   355   \end{tikzpicture}

   356   \end{textblock}}

   357 

   358   \end{frame}}

   359   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   360 *}

   361 

   362 text_raw {*

   363   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   364   \mode<presentation>{

   365   \begin{frame}[c]

   366   \frametitle{Recursive Functions}%

   367 

   368   \begin{itemize}

   369   \item[] 

   370   \begin{center}

   371   \begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}

   372   @{text "rec"} & $::=$  & @{term "Z"} & \textcolor{black!60}{zero-function}\\[1mm]

   373   & $\mid$ & @{term "S"} & \textcolor{black!60}{successor-function}\\[1mm]

   374   & $\mid$ & @{term "id n m"} & \textcolor{black!60}{projection}\\[1mm]

   375   & $\mid$ & @{term "Cn n f gs"} & \textcolor{black!60}{composition}\\[1mm]

   376   & $\mid$ & @{term "Pr n f g"} & \textcolor{black!60}{primitive recursion}\\[1mm]

   377   & $\mid$ & @{term "Mn n f"} & \textcolor{black!60}{minimisation}

   378   \end{tabular}

   379   \end{center}\bigskip

   380 

   381   \item @{text "eval :: rec \<Rightarrow> nat list \<Rightarrow> nat"}\\ 

   382   can be defined by simple recursion\\ (HOL has @{term "Least"})

   383   

   384   \item \small you define

   385   \begin{itemize}

   386   \item addition, multiplication, logical operations, quantifiers\ldots

   387   \item coding of numbers (Cantor encoding), UF

   388   \end{itemize}

   389 

   390   \end{itemize}

   391   

   392 

   393   \end{frame}}

   394   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   395 *}

   396 

   397 text_raw {*

   398   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   399   \mode<presentation>{

   400   \begin{frame}[c]

   401   \frametitle{Copy Turing Machine}%

   402 

   403   \begin{itemize}

   404   \item TM that copies a number on the input tape

   405   \begin{center}

   406   @{text "copy \<equiv> cbegin ; cloop ; cend"}

   407   \end{center}\smallskip

   408 

   409 

   410   \begin{center}

   411   \begin{tikzpicture}[scale=0.7]

   412   \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};

   413   \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};

   414   \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};

   415   \node [anchor=base] at (2.2,-0.8) {\small$\overbrace{@{text cbegin}}^{}$};

   416   \node [anchor=base] at (5.6,-0.8) {\small$\overbrace{@{text cloop}}^{}$};

   417   \node [anchor=base] at (10.5,-0.8) {\small$\overbrace{@{text cend}}^{}$};

   418 

   419 

   420   \begin{scope}[shift={(0.5,0)}]

   421   \draw[very thick] (-0.25,0)   -- ( 1.25,0);

   422   \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5);

   423   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

   424   \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

   425   \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

   426   \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

   427   \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);

   428   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

   429   \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);

   430   \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);

   431   \end{scope}

   432 

   433   \begin{scope}[shift={(2.9,0)}]

   434   \draw[very thick] (-0.25,0)   -- ( 2.25,0);

   435   \draw[very thick] (-0.25,0.5) -- ( 2.25,0.5);

   436   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

   437   \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

   438   \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

   439   \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

   440   \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);

   441   \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);

   442   \draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6);

   443   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

   444   \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);

   445   \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);

   446   \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);

   447   \end{scope}

   448 

   449   \begin{scope}[shift={(6.8,0)}]

   450   \draw[very thick] (-0.75,0)   -- ( 3.25,0);

   451   \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);

   452   \draw[very thick] (-0.75,0)   -- (-0.75,0.5);

   453   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

   454   \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

   455   \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

   456   \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

   457   \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);

   458   \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);

   459   \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);

   460   \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5);

   461   \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);

   462   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

   463   \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);

   464   \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);

   465   \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);

   466   \end{scope}

   467 

   468   \begin{scope}[shift={(11.7,0)}]

   469   \draw[very thick] (-0.75,0)   -- ( 3.25,0);

   470   \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);

   471   \draw[very thick] (-0.75,0)   -- (-0.75,0.5);

   472   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

   473   \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

   474   \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

   475   \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

   476   \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);

   477   \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);

   478   \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);

   479   \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5);

   480   \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);

   481   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

   482   \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);

   483   \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);

   484   \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);

   485   \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);

   486   \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);

   487   \end{scope}

   488   \end{tikzpicture}

   489   \end{center}\bigskip

   490 

   491   \footnotesize

   492   \begin{center}

   493   \begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c}

   494   \begin{tabular}[t]{@ {}l@ {}}

   495   @{text cbegin} @{text "\<equiv>"}\\

   496   \hspace{2mm}@{text "["}@{text "(W\<^bsub>0\<^esub>, 0), (R, 2), (R, 3),"}\\

   497   \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>1\<^esub>, 3), (L, 4),"}\\

   498   \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} 

   499   \end{tabular}

   500   &

   501   \begin{tabular}[t]{@ {}l@ {}}

   502   @{text cloop} @{text "\<equiv>"}\\

   503   \hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\

   504   \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>0\<^esub>, 2), (R, 3), (R, 4),"}\\

   505   \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>1\<^esub>, 5), (R, 4), (L, 6),"}\\

   506   \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} 

   507   \end{tabular}

   508   &

   509   \begin{tabular}[t]{@ {}l@ {}}

   510   @{text cend} @{text "\<equiv>"}\\

   511   \hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>1\<^esub>, 3),"}\\

   512   \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\

   513   \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>0\<^esub>, 4), (R, 0),"}\\

   514   \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"} 

   515   \end{tabular}

   516   \end{tabular}

   517   \end{center}

   518 

   519   \end{itemize}

   520 

   521 

   522   \end{frame}}

   523   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   524 *}

   525 

   526 text_raw {*

   527   \definecolor{mygrey}{rgb}{.80,.80,.80}

   528   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   529   \mode<presentation>{

   530   \begin{frame}[c]

   531   \frametitle{Hoare Logic for TMs}%

   532 

   533   \begin{itemize}

   534   \item Hoare-triples\onslide<2>{ and Hoare-pairs:}

   535 

   536   \small

   537   \begin{center}

   538   \begin{tabular}{@ {\hspace{-6mm}}c@ {\hspace{-3mm}}c@ {}}

   539   \begin{tabular}[t]{@ {}l@ {}}

   540   \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]

   541   \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\

   542   \hspace{7mm}if @{term "P tp"} holds then\\

   543   \hspace{7mm}@{text "\<exists>"}@{term n}. such that\\

   544   \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\

   545   \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"}

   546   \end{tabular} &

   547 

   548   \onslide<2>{

   549   \begin{tabular}[t]{@ {}l@ {}}

   550   \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]

   551   \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ 

   552   \hspace{7mm}if @{term "P tp"} holds then\\

   553   \hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"}

   554   \end{tabular}}

   555   \end{tabular}

   556   \end{center}

   557 

   558   \end{itemize}

   559 

   560   \end{frame}}

   561   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   562 *}

   563 

   564 (*<*)

   565 lemmas HR1 = 

   566   Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^sub>1" and B="p\<^sub>2"]

   567 

   568 lemmas HR2 =

   569   Hoare_plus_unhalt[where ?A="p\<^sub>1" and B="p\<^sub>2"]

   570 (*>*)

   571 

   572 text_raw {*

   573   \definecolor{mygrey}{rgb}{.80,.80,.80}

   574   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   575   \mode<presentation>{

   576   \begin{frame}[c]

   577   \frametitle{Some Derived Rules}%

   578   \large

   579   

   580   \begin{center}

   581   @{thm[mode=Rule] Hoare_consequence}\bigskip\bigskip\\

   582   

   583   \begin{tabular}{@ {\hspace{-5mm}}c@ {\hspace{4mm}}c@ {}}

   584   $\inferrule*

   585   {@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}}

   586   {@{thm (concl) HR1}}

   587   $ &

   588   $

   589   \inferrule*

   590   {@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}

   591   {@{thm (concl) HR2}}

   592   $

   593   \end{tabular}

   594   \end{center}

   595 

   596   \end{frame}}

   597   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   598 *}

   599 

   600 text_raw {*

   601   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   602   \mode<presentation>{

   603   \begin{frame}[b]

   604   \frametitle{Undecidability}%

   605 

   606   \begin{textblock}{7}(4,2.4)

   607   @{thm tcontra_def}

   608   \end{textblock}

   609   

   610   \only<2>{

   611   \begin{itemize}

   612   \item Suppose @{text H} decides @{text contra} called with the code 

   613   of @{text contra} halts, then\smallskip

   614 

   615   \begin{center}\small

   616   \begin{tabular}{@ {}l@ {}}

   617   \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}}

   618   @{term "P\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\

   619   @{term "P\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\

   620   @{term "P\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}

   621   \end{tabular}\bigskip\bigskip

   622   \\

   623   \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}

   624   $\inferrule*{

   625     \inferrule*{@{term "{P\<^sub>1} tcopy {P\<^sub>2}"} \\ @{term "{P\<^sub>2} H {P\<^sub>3}"}}

   626     {@{term "{P\<^sub>1} (tcopy |+| H) {P\<^sub>3}"}}

   627     \\ @{term "{P\<^sub>3} dither \<up>"}

   628    }

   629    {@{term "{P\<^sub>1} tcontra \<up>"}}

   630   $

   631   \end{tabular}

   632   \end{tabular}

   633   \end{center}

   634   \end{itemize}}

   635   \only<3>{

   636   \begin{itemize}

   637   \item Suppose @{text H} decides @{text contra} called with the code 

   638   of @{text contra} does \emph{not} halt, then\\[-8mm]\mbox{}

   639 

   640   \begin{center}\small

   641   \begin{tabular}{@ {}l@ {}}

   642   \begin{tabular}[t]{@ {\hspace{-1mm}}l@ {}}

   643   @{term "Q\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\

   644   @{term "Q\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\

   645   @{term "Q\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}

   646   \end{tabular}\bigskip\bigskip

   647   \\

   648   \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}

   649   $\inferrule*{

   650     \inferrule*{@{term "{Q\<^sub>1} tcopy {Q\<^sub>2}"} \\ @{term "{Q\<^sub>2} H {Q\<^sub>3}"}}

   651     {@{term "{Q\<^sub>1} (tcopy |+| H) {Q\<^sub>3}"}}

   652     \\ @{term "{Q\<^sub>3} dither {Q\<^sub>3}"}

   653    }

   654    {@{term "{Q\<^sub>1} tcontra {Q\<^sub>3}"}}

   655   $

   656   \end{tabular}

   657   \end{tabular}

   658   \end{center}

   659   \end{itemize}}

   660 

   661   \end{frame}}

   662   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   663 *}

   664 

   665 

   666 text_raw {*

   667   \definecolor{mygrey}{rgb}{.80,.80,.80}

   668   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   669   \mode<presentation>{

   670   \begin{frame}[c]

   671   \frametitle{Hoare Reasoning}%

   672 

   673   \begin{itemize}

   674   \item reasoning is quite demanding, e.g.~the invariants 

   675   of the copy-machine:\\[-5mm]\mbox{}

   676 

   677   \footnotesize

   678   \begin{center}

   679   \begin{tabular}{@ {\hspace{-5mm}}c@ {}}

   680   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {\hspace{-0.9cm}}l@ {}}

   681   \hline

   682   @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\

   683   @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\

   684   @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\

   685   @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\

   686   @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\

   687                                 &             & @{thm (rhs) inv_begin02}\smallskip \\

   688    \hline

   689   @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\

   690                                &             & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\

   691   @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\

   692    \hline

   693   @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\

   694   @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\

   695   \hline

   696   \end{tabular}

   697   \end{tabular}

   698   \end{center}

   699 

   700   \end{itemize}

   701 

   702   \end{frame}}

   703   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   704 *}

   705 

   706 

   707 

   708 text_raw {*

   709   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   710   \mode<presentation>{

   711   \begin{frame}[c]

   712   \frametitle{Midway Conclusion}%

   713 

   714   \begin{itemize}

   715   \item feels awfully like reasoning about machine code

   716   \item compositional constructions / reasoning is not at all frictionless

   717   \item sizes

   718 

   719   \begin{center}

   720   \begin{tabular}{ll}

   721   & sizes:\smallskip\\

   722   UF       & @{text 140843} constructors\\

   723   URM      & @{text 2} Mio instructions\\

   724   UTM      & @{text 38} Mio states\\

   725   \end{tabular}

   726   \end{center}\smallskip\pause

   727 

   728   \item an observation: our treatment of recursive functions is a mini-version

   729   of the work by\\ Myreen \& Owens about deeply embedding HOL

   730   \end{itemize}

   731  

   732   \only<1>{

   733   \begin{textblock}{4}(2,13.9)

   734   \begin{tikzpicture}

   735   \draw (0,0) node {\small\begin{tabular}{l}$^\star$old version: 

   736   URM (@{text 12} Mio) UTM (@{text 112} Mio)\end{tabular}};

   737   \end{tikzpicture}

   738   \end{textblock}}

   739 

   740   \end{frame}}

   741   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   742 *}

   743 

   744 text_raw {*

   745   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   746   \mode<presentation>{

   747   \begin{frame}[c]

   748   \frametitle{\begin{tabular}{@ {}c@ {}}\Large Inspiration from other Works\end{tabular}}%

   749 

   750   \onslide<3->{

   751   \begin{itemize}

   752   \item Jensen, Benton, Kennedy ({\bf 2013}),

   753   {\it High-Level Separation Logic for Low-Level Code}\medskip\\

   754   

   755   \item Myreen ({\bf 2008}), {\it Formal Verification of Machine-Code Programs},

   756   PhD thesis\medskip

   757 

   758   \item Klein, Kolanski, Boyton ({\bf 2012}), {\it Mechanised Separation Algebra}

   759 

   760   \end{itemize}}

   761 

   762   \only<2->{

   763   \begin{textblock}{4}(1.4,0.9)

   764   \begin{tikzpicture}

   765   \draw (0,0) node {\fontspec{Chalkduster}\textcolor{red!80}{\LARGE Stealing}};

   766   \end{tikzpicture}

   767   \end{textblock}}

   768   \end{frame}}

   769   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   770 *}

   771 

   772 text_raw {*

   773   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   774   \mode<presentation>{

   775   \begin{frame}[c]

   776   \frametitle{Better Composability}%

   777 

   778   \begin{itemize}

   779   \item an idea from Jensen, Benton \& Kennedy who looked at X86 

   780   assembly programs and macros\bigskip

   781   

   782   \item assembly for TMs:\medskip

   783   \begin{center}

   784   \begin{tabular}{l}

   785   @{text "move_one_left"} @{text "\<equiv>"}\\ 

   786   \hspace{13mm} @{text "\<Lambda> exit."}\\

   787   \hspace{16mm} @{text "Inst (L, exit) (L, exit)"} @{text ";"}\\

   788   \hspace{16mm} @{text "Label exit"}\\

   789   \end{tabular}

   790   \end{center}\bigskip\bigskip

   791 

   792   \begin{tabular}{l}

   793   $\Rightarrow$ represent "state" labels as functions\\

   794   \phantom{$\Rightarrow$} (with bound variables $\Rightarrow$ locality) 

   795   \end{tabular}

   796   \end{itemize}

   797   \end{frame}}

   798   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   799 *}

   800 

   801 text_raw {*

   802   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   803   \mode<presentation>{

   804   \begin{frame}[c]

   805   \frametitle{Better Composability}%

   806 

   807   \begin{center}

   808   \begin{tabular}{@ {\hspace{-10mm}}l}

   809   @{text "move_left_until_zero"} @{text "\<equiv>"} \\

   810   \hspace{31mm} @{text "\<Lambda> start exit."}\\

   811   \hspace{36mm} @{text "Label start"} @{text ";"}\\

   812   \hspace{36mm} @{text "if_zero exit"} @{text ";"}\\

   813   \hspace{36mm} @{text "move_left"} @{text ";"}\\

   814   \hspace{36mm} @{text "jmp start"} @{text ";"}\\

   815   \hspace{36mm} @{text "Label exit"}\\

   816   \end{tabular}

   817   \end{center}

   818 

   819   \small

   820   \begin{tabular}{l}

   821   @{text "if_zero e \<equiv> \<Lambda> exit. Inst (W\<^sub>0, e), (W\<^sub>1, exit); Label exit"}\\

   822   \hspace{5mm}@{text "jmp e \<equiv> Inst (W\<^sub>0, e), (W\<^sub>1, e)"}

   823   \end{tabular}

   824 

   825   \end{frame}}

   826   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   827 *}

   828 

   829 text_raw {*

   830   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   831   \mode<presentation>{

   832   \begin{frame}[c]

   833   \frametitle{{\large The Trouble With Hoare-Triples}}%

   834 

   835   \begin{itemize}

   836   \item Whenever we wanted to prove 

   837 

   838   \begin{center}

   839   \large @{text "{P} p {Q}"}

   840   \end{center}\bigskip\medskip

   841  

   842   \item[@{text "(1)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy)}

   843 

   844   

   845   

   846   \item[@{text "(2)"}] we had to find a termination order proving that @{text p} terminates

   847   \textcolor{gray}{(not easy either)}

   848   \end{itemize}\pause

   849   

   850   \begin{center}

   851   \alert{very little opportunity for automation}

   852   \end{center}

   853 

   854   \end{frame}}

   855   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   856 *}

   857 

   858 text_raw {*

   859   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   860   \mode<presentation>{

   861   \begin{frame}[c]

   862   \frametitle{Separation Algebra}%

   863 

   864   \begin{itemize}

   865   \item use some infrastructure introduced by Klein et al in Isabelle/HOL

   866   \item and an idea by Myreen\bigskip\bigskip

   867 

   868   \begin{center}

   869   \large @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"}\bigskip\bigskip

   870   \end{center}

   871   

   872   \item[] @{text "p, c, q"} will be assertions in a separation logic\pause

   873 

   874   \begin{center}

   875   e.g.~~@{text "\<lbrace>st i \<star> hd n \<star> ones u v \<star> zero (v + 1)\<rbrace>"}

   876   \end{center}

   877   \end{itemize}

   878   \end{frame}}

   879   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   880 *}

   881 

   882 text_raw {*

   883   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   884   \mode<presentation>{

   885   \begin{frame}[c]

   886   \frametitle{Separation Triples}%

   887 

   888   \Large

   889   \begin{center}

   890   \begin{tabular}{l@ {\hspace{-10mm}}l}

   891   @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"} @{text "\<equiv>"}\smallskip\\

   892   & @{text "\<forall> cf r."}\\

   893   & \hspace{3mm} @{text "(p \<star> c \<star> r) cf"} implies\\

   894   & \hspace{3mm} @{text "\<exists> k. "} @{text "(q \<star> c \<star> r) (steps k cf)"} 

   895   \end{tabular}

   896   \end{center}\bigskip\bigskip

   897 

   898   \normalsize

   899   @{text "c"} can be\;\;\; @{text "i:[move_left_until_zero]:j"}

   900   

   901 

   902   \end{frame}}

   903   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   904 *}

   905 

   906 text_raw {*

   907   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   908   \mode<presentation>{

   909   \begin{frame}[c]

   910   \frametitle{Automation}%

   911 

   912   \begin{itemize}

   913   \item we introduced some tactics for handling sequential programs\bigskip

   914 

   915   \begin{center}

   916   @{text "\<lbrace>p\<rbrace> i:[c\<^sub>1 ; ... ; c\<^sub>n]:j \<lbrace>q\<rbrace>"}

   917   \end{center}\bigskip\bigskip

   918 

   919   \item for loops we often only have to do inductions on the length 

   920   of the input (e.g.~how many @{text "1"}s are on the tape)\pause

   921   

   922   \item these macros allow us to completely get rid of register machines

   923   \end{itemize}

   924   

   925 

   926   \end{frame}}

   927   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   928 *}

   929 

   930 text_raw {*

   931   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   932   \mode<presentation>{

   933   \begin{frame}[c]

   934   \frametitle{Conclusion}%

   935 

   936   \begin{itemize}

   937   \item What started out as a student project, turned out to be much more

   938   fun than first thought.\bigskip

   939 

   940   \item Where can you claim that you proved the correctness of

   941   a @{text "38"} Mio instruction program?

   942   (ca.~@{text 7000} is the soa \raisebox{-1mm}{\includegraphics[scale=0.077]{smiley.jpg}})

   943   \bigskip

   944   

   945   \item We learned a lot about current verification technology for low-level code

   946   (we had no infrastructure: CPU model).\bigskip

   947 

   948   \item The existing literature on TMs \& RMs leave out quite a bit of the story

   949   (not to mention contains bugs).

   950   \end{itemize}

   951   

   952 

   953   \end{frame}}

   954   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   955 *}

   956 

   957 (*<*)

   958 end

   959 end

   960 (*>*)