# HG changeset patch # User Christian Urban # Date 1364390681 0 # Node ID b66578c084906a8822881d5f8ef521b14c098a4a # Parent 49dcc0b9b0b3fa5e3bc255620b2084d5f4707361 tunded diff -r 49dcc0b9b0b3 -r b66578c08490 Paper/Paper.thy --- a/Paper/Paper.thy Wed Mar 27 13:16:37 2013 +0000 +++ b/Paper/Paper.thy Wed Mar 27 13:24:41 2013 +0000 @@ -1672,7 +1672,8 @@ \cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to some slick mechanised proofs, our experience is that Turing machines are not too daunting if one is only concerned with formalising the - undecidability of the halting problem for Turing machines. This + undecidability of the halting problem for Turing machines. As a point of + comparison, the halting problem took us around 1500 loc of Isar-proofs, which is just one-and-a-half times of a mechanised proof pearl about the Myhill-Nerode theorem. So our conclusion is that this part is not as daunting @@ -1705,7 +1706,7 @@ with the task of finding appropriate invariants and measures for showing the correctness and termination of these Turing machines. Whenever we can use Hoare-style reasoning, the invariants are - relatively straightforward and as a point of comparison much smaller than for example the + relatively straightforward and again as a point of comparison much smaller than for example the invariants used by Myreen in a correctness proof of a garbage collector written in machine code \cite[Page 76]{Myreen09}. However, the invariant needed for the abacus proof, where Hoare-style reasoning does not work, is diff -r 49dcc0b9b0b3 -r b66578c08490 paper.pdf Binary file paper.pdf has changed