1 (*<*)

     2 theory Slides1

     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 

    13 notation (latex output)

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

    15   Oc ("0") and

    16   Bk ("1") and

    17   exponent ("_\<^bsup>_\<^esup>") and

    18   inv_begin0 ("I\<^isub>0") and

    19   inv_begin1 ("I\<^isub>1") and

    20   inv_begin2 ("I\<^isub>2") and

    21   inv_begin3 ("I\<^isub>3") and

    22   inv_begin4 ("I\<^isub>4") and 

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

    24   inv_loop1 ("J\<^isub>1") and

    25   inv_loop0 ("J\<^isub>0") and

    26   inv_end1 ("K\<^isub>1") and

    27   inv_end0 ("K\<^isub>0")

    28 

    29 

    30  

    31 lemma inv_begin_print:

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

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

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

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

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

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

    38 apply(case_tac [!] tp)

    39 by (auto)

    40 

    41 

    42 lemma inv1: 

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

    44 unfolding Turing_Hoare.assert_imp_def

    45 unfolding inv_loop1.simps inv_begin0.simps

    46 apply(auto)

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

    48 apply(auto simp add: replicate.simps)

    49 done

    50 

    51 lemma inv2: 

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

    53 apply(rule ext)

    54 apply(case_tac x)

    55 apply(simp add: inv_end1.simps)

    56 done

    57 

    58 

    59 lemma measure_begin_print:

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

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

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

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

    64 by (simp_all)

    65 

    66 lemma inv_begin01:

    67   assumes "n > 1"

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

    69 using assms by auto                          

    70 

    71 lemma inv_begin02:

    72   assumes "n = 1"

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

    74 using assms by auto

    75 

    76 (*>*)

    77 

    78 

    79 

    80 text_raw {*

    81   \renewcommand{\slidecaption}{SMAL, 16 July 2013}

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

    83   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    84   \mode<presentation>{

    85   \begin{frame}

    86   \frametitle{%

    87   \begin{tabular}{@ {}c@ {}}

    88   \\[-3mm]

    89   \Large Reasoning about Turing Machines\\[-1mm] 

    90   \Large and Low-Level Code\\[-3mm] 

    91   \end{tabular}}

    92   

    93   \begin{center}

    94    Christian Urban\\[1mm]

    95   %%\small King's College London

    96   \end{center}\bigskip

    97  

    98   \begin{center}

    99   in cooperation with Jian Xu and Xingyuan Zhang

   100   \end{center}

   101   \end{frame}}

   102   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   103 *}

   104 

   105 text_raw {*

   106   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   107   \mode<presentation>{

   108   \begin{frame}[c]

   109   \frametitle{A Trend in Verification}%

   110 

   111   \begin{itemize}

   112   \item in the past:\\

   113   \begin{quote}

   114   model a problem mathematically and proof properties about the 

   115   model

   116   \end{quote}\bigskip

   117 

   118   \item needs elegance, is still very hard\bigskip\pause

   119 

   120   \item does not help with ensuring the correctness of running programs

   121   \end{itemize}

   122 

   123   \end{frame}}

   124   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   125 *}

   126 

   127 text_raw {*

   128   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   129   \mode<presentation>{

   130   \begin{frame}[c]

   131   \frametitle{A Trend in Verification}%

   132 

   133   \begin{itemize}

   134   \item make the specification executable (e.g.~Compcert)\bigskip\pause

   135 

   136   you would expect the trend would be to for example model C, implement 

   137   your programs in C and verify the programs written in C (e.g.~seL4) 

   138   \end{itemize}

   139 

   140   \end{frame}}

   141   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   142 *}

   143 

   144 text_raw {*

   145   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   146   \mode<presentation>{

   147   \begin{frame}[c]

   148   \frametitle{A Trend in Verification}%

   149 

   150   \begin{itemize}

   151   \item but actually people start to verify machine code directly

   152   (e.g.~bignum arithmetic implemented in x86-64 -- 700 instructions)

   153 

   154   \item CPU models exists, but the strategy is to use a small subset

   155   which you use in your programs

   156   \end{itemize}

   157 

   158   \end{frame}}

   159   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   160 *}

   161 

   162 text_raw {*

   163   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   164   \mode<presentation>{

   165   \begin{frame}[c]

   166   \frametitle{Why Turing Machines}%

   167 

   168   \begin{itemize}

   169   \item at the beginning it was just a nice student project

   170   about computability

   171 

   172   \begin{center}

   173   \includegraphics[scale=0.3]{boolos.jpg}

   174   \end{center}

   175 

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

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

   178   \pause

   179 

   180   \item \small Norrish formalised computability via lambda-calculus (and nominal);

   181   Asperti and Riccioti formalised TMs but didn't get proper UTM

   182   \end{itemize}

   183 

   184 

   185   \end{frame}}

   186   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   187 *}

   188 

   189 text_raw {*

   190   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   191   \mode<presentation>{

   192   \begin{frame}[c]

   193   \frametitle{Turing Machines}%

   194 

   195   \begin{itemize}

   196   \item tapes contain 0 or 1 only

   197 

   198   \begin{center}

   199 \begin{tikzpicture}[scale=1]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   222   \end{tikzpicture}

   223   \end{center}

   224 

   225   \item steps function

   226 

   227   \begin{quote}

   228   What does the tape look like after the TM has executed n steps?

   229   \end{quote}\pause

   230 

   231   designate the 0-state as halting state and remain there forever

   232   \end{itemize}

   233 

   234   \end{frame}}

   235   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   236 *}

   237 

   238 text_raw {*

   239   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   240   \mode<presentation>{

   241   \begin{frame}[c]

   242   \frametitle{Copy Turing Machines}%

   243 

   244   \begin{itemize}

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

   246 

   247 

   248   \begin{center}

   249 \begin{tikzpicture}[scale=0.7]

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

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

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

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

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

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

   256 

   257 

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

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

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

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

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

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

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

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

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

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

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

   269   \end{scope}

   270 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   285   \end{scope}

   286 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   304   \end{scope}

   305 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   325   \end{scope}

   326   \end{tikzpicture}

   327   \end{center}\bigskip

   328 

   329   \footnotesize

   330   \begin{center}

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

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

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

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

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

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

   337   \end{tabular}

   338   &

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

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

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

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

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

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

   345   \end{tabular}

   346   &

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

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

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

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

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

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

   353   \end{tabular}

   354   \end{tabular}

   355   \end{center}

   356 

   357   \end{itemize}

   358 

   359 

   360   \end{frame}}

   361   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   362 *}

   363 

   364 text_raw {*

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

   366   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   367   \mode<presentation>{

   368   \begin{frame}[c]

   369   \frametitle{Hoare Logic for TMs}%

   370 

   371   \begin{itemize}

   372   \item Hoare-triples and Hoare-pairs:

   373 

   374   \small

   375   \begin{center}

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

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

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

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

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

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

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

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

   384   \end{tabular} &

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

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

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

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

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

   390   \end{tabular}

   391   \end{tabular}

   392   \end{center}

   393 

   394   \end{itemize}

   395 

   396   \end{frame}}

   397   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   398 *}

   399 

   400 text_raw {*

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

   402   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   403   \mode<presentation>{

   404   \begin{frame}[c]

   405   \frametitle{Hoare Reasoning}%

   406 

   407   \begin{itemize}

   408   \item reasoning is still quite difficult---invariants

   409 

   410   \footnotesize

   411   \begin{center}

   412 \begin{tabular}{@ {\hspace{-4mm}}lcl@ {\hspace{-0.9cm}}l@ {}}

   413   \hline

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

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

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

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

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

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

   420    \hline

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

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

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

   424    \hline

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

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

   427   \hline

   428   \end{tabular}

   429   \end{center}

   430 

   431   \end{itemize}

   432 

   433   \end{frame}}

   434   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   435 *}

   436 

   437 text_raw {*

   438   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   439   \mode<presentation>{

   440   \begin{frame}[c]

   441   \frametitle{Register Machines}%

   442 

   443   \begin{itemize}

   444   \item instructions

   445 

   446   \begin{center}

   447   \begin{tabular}{rcl@ {\hspace{10mm}}l}

   448   @{text "I"} & $::=$  & @{term "Inc R\<iota>"} & increment register @{text "R"} by one\\

   449   & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & if content of @{text R} is non-zero,\\

   450   & & & then decrement it by one\\

   451   & & & otherwise jump to instruction @{text L}\\

   452   & $\mid$ & @{term "Goto L\<iota>"} & jump to instruction @{text L}

   453   \end{tabular}

   454   \end{center}

   455 

   456   \end{itemize}

   457 

   458   \end{frame}}

   459   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   460 *}

   461 

   462 text_raw {*

   463   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   464   \mode<presentation>{

   465   \begin{frame}[c]

   466   \frametitle{Recursive Functions}%

   467 

   468   \begin{itemize}

   469   \item addition, multiplication, \ldots

   470   \item logical operations, quantifiers\ldots

   471   \item coding of numbers (Cantor encoding)

   472   \item UF\pause\bigskip

   473 

   474   \item Recursive Functions $\Rightarrow$ Register Machines

   475   \item Register Machines $\Rightarrow$ Turing Machines

   476   \end{itemize}

   477 

   478   \end{frame}}

   479   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   480 *}

   481 

   482 text_raw {*

   483   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   484   \mode<presentation>{

   485   \begin{frame}[c]

   486   \frametitle{Sizes}%

   487 

   488   \begin{itemize}

   489   \item UF (size: 140843)

   490   \item Register Machine (size: 2 Mio instructions)

   491   \item UTM (size: 38 Mio states)

   492   \end{itemize}\bigskip\bigskip

   493 

   494   \small

   495   old version: RM (12 Mio) UTM (112 Mio)

   496   \end{frame}}

   497   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   498 *}

   499 

   500 text_raw {*

   501   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   502   \mode<presentation>{

   503   \begin{frame}[c]

   504   \frametitle{Separation Algebra}%

   505 

   506   \begin{itemize}

   507   \item introduced a separation algebra framework for register machines and TMs 

   508   \item we can semi-automate the reasoning for our small TMs

   509   \item we can assemble bigger programs out of smaller components\bigskip

   510 

   511   \item looks awfully like ``real'' assembly code\pause

   512   \item Conclusion: we have a playing ground for reasoning about low-level 

   513   code; we work on automation

   514   \end{itemize}

   515   \end{frame}}

   516   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   517 *}

   518 

   519 

   520 

   521 

   522 (*<*)

   523 end

   524 (*>*)