717 Like Asperti and Ricciotti with their notion of realisability, we |
717 Like Asperti and Ricciotti with their notion of realisability, we |
718 have set up our Hoare-rules so that we can deal explicitly |
718 have set up our Hoare-rules so that we can deal explicitly |
719 with total correctness and non-terminantion, rather than have |
719 with total correctness and non-terminantion, rather than have |
720 notions for partial correctness and termination. Although the latter |
720 notions for partial correctness and termination. Although the latter |
721 would allow us to reason more uniformly (only using Hoare-triples), |
721 would allow us to reason more uniformly (only using Hoare-triples), |
722 we prefer our definitions because we can derive simple |
722 we prefer our definitions because we can derive below some simple |
723 Hoare-rules for sequentially composed Turing programs. In this way |
723 Hoare-rules for sequentially composed Turing programs. In this way |
724 we can reason about the correctness of @{term "tcopy_begin"}, for |
724 we can reason about the correctness of @{term "tcopy_begin"}, for |
725 example, completely separately from @{term "tcopy_loop"} and @{term |
725 example, completely separately from @{term "tcopy_loop"} and @{term |
726 "tcopy_end"}. |
726 "tcopy_end"}. |
727 |
727 |
728 It is realatively straightforward to prove that the Turing program |
728 It is realatively straightforward to prove that the small Turing program |
729 @{term "dither"} shown in \eqref{dither} is correct. This program |
729 @{term "dither"} shown in \eqref{dither} is correct. This program |
730 should be the ``identity'' when started with a standard tape representing |
730 should be the ``identity'' when started with a standard tape representing |
731 @{text "1"} but loop when started with @{text 0} instead, as pictured |
731 @{text "1"} but loop when started with @{text 0} instead, as pictured |
732 below. |
732 below. |
733 |
733 |
793 |
793 |
794 \noindent |
794 \noindent |
795 The first is by a simple calculation. The second is by induction on the |
795 The first is by a simple calculation. The second is by induction on the |
796 number of steps we can perform starting from the input tape. |
796 number of steps we can perform starting from the input tape. |
797 |
797 |
798 The purpose of the @{term tcopy} program defined in \eqref{tcopy} is |
798 The program @{term tcopy} defined in \eqref{tcopy} has 15 states; |
799 to produce the standard tape @{term "(DUMMY, <[n, n::nat]>)"} when |
799 its purpose is to produce the standard tape @{term "(DUMMY, <[n, |
800 started with @{term "(DUMMY, <[n::nat]>)"}, that is making a copy of |
800 n::nat]>)"} when started with @{term "(DUMMY, <[n::nat]>)"}, that is |
801 a value on the tape. Reasoning about this program is substantially |
801 making a copy of a value on the tape. Reasoning about this program |
802 harder than about @{term dither}. To ease the burden, we prove |
802 is substantially harder than about @{term dither}. To ease the |
803 the following two Hoare-rules for sequentially composed programs. |
803 burden, we prove the following two Hoare-rules for sequentially |
|
804 composed programs. |
804 |
805 |
805 \begin{center} |
806 \begin{center} |
806 \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}} |
807 \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}} |
807 $\inferrule*[Right=@{thm (prem 3) HR1}] |
808 $\inferrule*[Right=@{thm (prem 3) HR1}] |
808 {@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}} |
809 {@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}} |
825 state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly. |
826 state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly. |
826 |
827 |
827 |
828 |
828 The Hoare-rules above allow us to prove the correctness of @{term tcopy} |
829 The Hoare-rules above allow us to prove the correctness of @{term tcopy} |
829 by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"} |
830 by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"} |
830 and @{term "tcopy_end"} in isolation. We will show the details for the |
831 and @{term "tcopy_end"} in isolation. We will show the details for |
831 the program @{term "tcopy_begin"}. |
832 the program @{term "tcopy_begin"}. We found the following invariants for each |
|
833 state: |
|
834 |
|
835 \begin{center} |
|
836 @{thm inv_begin0.simps}\\ |
|
837 @{thm inv_begin1.simps}\\ |
|
838 @{thm inv_begin2.simps}\\ |
|
839 @{thm inv_begin3.simps}\\ |
|
840 @{thm inv_begin4.simps} |
|
841 \end{center} |
832 |
842 |
833 |
843 |
834 measure for the copying TM, which we however omit. |
844 measure for the copying TM, which we however omit. |
835 |
845 |
836 \begin{center} |
846 \begin{center} |