diff -r 06db15939b7c -r cdef5b1072fe Paper/Paper.thy --- a/Paper/Paper.thy Wed Jan 30 09:33:06 2013 +0000 +++ b/Paper/Paper.thy Wed Jan 30 23:00:09 2013 +0000 @@ -723,7 +723,7 @@ ``doing what they are supposed to be doing''. Such correctness proofs are usually left out in the informal literature, for example \cite{Boolos87}. The first program we need to prove correct is the @{term dither} program shown in \eqref{dither} - and the other program is @{term "tcopy"} defined as + and the second program is @{term "tcopy"} defined as \begin{equation} \mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @@ -732,18 +732,18 @@ \end{equation} \noindent - whose three components are given in Figure~\ref{copy}. We introduce - the notion of total correctness defined in terms of - \emph{Hoare-triples}, written @{term "{P} p {Q}"} (this notion is - very similar to \emph{realisability} in \cite{AspertiRicciotti12}). - The Hoare-triples implement the idea that a program @{term p} - started in state @{term "1::nat"} with a tape satisfying @{term P} - will after some @{text n} steps halt (have transitioned into the - halting state) with a tape satisfying @{term Q}. We also have - \emph{Hoare-pairs} of the form @{term "{P} p \"} implementing the - case that a program @{term p} started with a tape satisfying @{term - P} will loop (never transition into the halting state). Both notion - are formally defined as + whose three components are given in Figure~\ref{copy}. For our + correctness proofs, we introduce the notion of total correctness + defined in terms of \emph{Hoare-triples}, written @{term "{P} p + {Q}"}. They implement the idea that a program @{term + p} started in state @{term "1::nat"} with a tape satisfying @{term + P} will after some @{text n} steps halt (have transitioned into the + halting state) with a tape satisfying @{term Q}. This idea is very + similar to \emph{realisability} in \cite{AspertiRicciotti12}. We + also have \emph{Hoare-pairs} of the form @{term "{P} p \"} + implementing the case that a program @{term p} started with a tape + satisfying @{term P} will loop (never transition into the halting + state). Both notion are formally defined as \begin{center} \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} @@ -765,7 +765,7 @@ \end{center} \noindent - For our Hoare-triples we can easily prove the following consequence rule + For our Hoare-triples we can easily prove the following Hoare-consequence rule \begin{equation} @{thm[mode=Rule] Hoare_consequence} @@ -784,10 +784,10 @@ example, completely separately from @{term "tcopy_loop"} and @{term "tcopy_end"}. - It is realatively straightforward to prove that the small Turing program + It is realatively straightforward to prove that the Turing program @{term "dither"} shown in \eqref{dither} is correct. This program should be the ``identity'' when started with a standard tape representing - @{text "1"} but loop when started with @{text 0} instead, as pictured + @{text "1"} but loops when started with @{text 0} instead, as pictured below. @@ -851,7 +851,7 @@ \end{center} \noindent - The first is by a simple calculation. The second is by induction on the + The first is by a simple calculation. The second is by an induction on the number of steps we can perform starting from the input tape. The program @{term tcopy} defined in \eqref{tcopy} has 15 states; @@ -878,18 +878,20 @@ \noindent The first corresponds to the usual Hoare-rule for composition of two - terminating programs. The second rule is for cases where the first program - terminates generating a tape for which the second program loops. - The side-condition about @{thm (prem 3) HR2} is needed in both rules - in order to ensure that the redirection of the halting and initial - state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly. + terminating programs. The second rule gives the conditions for when + the first program terminates generating a tape for which the second + program loops. The side-conditions about @{thm (prem 3) HR2} are + needed in order to ensure that the redirection of the halting and + initial state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly. - The Hoare-rules above allow us to prove the correctness of @{term tcopy} - by considering the correctness of the components @{term "tcopy_begin"}, @{term "tcopy_loop"} - and @{term "tcopy_end"} in isolation. We will show the details for - the program @{term "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots, @{term "inv_begin4"} - shown in Figure~\ref{invbegin}, - we define the following invariant for @{term "tcopy_begin"}. + The Hoare-rules allow us to prove the correctness of @{term + tcopy} by considering the correctness of the components @{term + "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"} in + isolation. We will show the details for the program @{term + "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots, + @{term "inv_begin4"} shown in Figure~\ref{invbegin} corresponding to + each state of @{term tcopy_begin}, we define the + following invariant for the whole program: \begin{figure} \begin{center} @@ -922,10 +924,10 @@ \end{center} \noindent - This definition depends on @{term n}, which represents the number - of @{term Oc}s on the tape. It is not hard (26 lines of automated proof script) - to show that for @{term "n > (0::nat)"} this invariant is preserved under @{term step} and @{term steps}. - + This invariant depends on @{term n} representing the number of + @{term Oc}s on the tape. It is not hard (26 lines of automated proof + script) to show that for @{term "n > (0::nat)"} this invariant is + preserved under computation rules @{term step} and @{term steps}. measure for the copying TM, which we however omit.