Slides/Slides2.thy
changeset 277 c6aa1be1033a
parent 276 6f71b016cbe7
child 278 acc752cef1e7
equal deleted inserted replaced
276:6f71b016cbe7 277:c6aa1be1033a
   255   \end{tikzpicture}
   255   \end{tikzpicture}
   256   \end{textblock}
   256   \end{textblock}
   257 
   257 
   258   \begin{textblock}{3}(1,10.0)
   258   \begin{textblock}{3}(1,10.0)
   259   \begin{tikzpicture}
   259   \begin{tikzpicture}
   260   \draw (0,0) node {\small\begin{tabular}{l}undecidabilty\\of the halting\\ problem\end{tabular}};
   260   \draw (0,0) node {\small\begin{tabular}{l}undecidability\\of the halting\\ problem\end{tabular}};
   261   \end{tikzpicture}
   261   \end{tikzpicture}
   262   \end{textblock}}
   262   \end{textblock}}
   263 
   263 
   264   \only<4->{
   264   \only<4->{
   265   \begin{textblock}{4}(4.2,12.4)
   265   \begin{textblock}{4}(4.2,12.4)
   311   \end{center}\pause
   311   \end{center}\pause
   312 
   312 
   313   \item @{text steps} function:
   313   \item @{text steps} function:
   314 
   314 
   315   \begin{quote}\rm
   315   \begin{quote}\rm
   316   What does the TM claclulate after it has executed @{text n} steps?
   316   What does the TM calculate after it has executed @{text n} steps?
   317   \end{quote}\pause
   317   \end{quote}\pause
   318 
   318 
   319   \item designate the @{text 0}-state as "halting state" and remain there 
   319   \item designate the @{text 0}-state as "halting state" and remain there 
   320   forever, i.e.~have a @{text Nop}-action
   320   forever, i.e.~have a @{text Nop}-action
   321   \end{itemize}
   321   \end{itemize}
   927   \item Where can you claim that you proved the correctness of
   927   \item Where can you claim that you proved the correctness of
   928   a @{text "38"} Mio instruction program. 
   928   a @{text "38"} Mio instruction program. 
   929   (ca.~@{text 7000} is the soa \raisebox{-1mm}{\includegraphics[scale=0.077]{smiley.jpg}})
   929   (ca.~@{text 7000} is the soa \raisebox{-1mm}{\includegraphics[scale=0.077]{smiley.jpg}})
   930   \bigskip
   930   \bigskip
   931   
   931   
   932   \item We learned a lot about current verification technology for low-level code.
   932   \item We learned a lot about current verification technology for low-level code
       
   933   (we had no infrastructure: CPU model).
   933   \end{itemize}
   934   \end{itemize}
   934   
   935   
   935 
   936 
   936   \end{frame}}
   937   \end{frame}}
   937   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   938   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%