219 In this paper we take on this daunting prospect and provide a |
219 In this paper we take on this daunting prospect and provide a |
220 formalisation of Turing machines, as well as abacus machines (a kind |
220 formalisation of Turing machines, as well as abacus machines (a kind |
221 of register machines) and recursive functions. To see the difficulties |
221 of register machines) and recursive functions. To see the difficulties |
222 involved with this work, one has to understand that Turing machine |
222 involved with this work, one has to understand that Turing machine |
223 programs can be completely \emph{unstructured}, behaving similar to |
223 programs can be completely \emph{unstructured}, behaving similar to |
224 Basic programs containing the infamous goto-statement \cite{Dijkstra68}. This |
224 Basic programs containing the infamous goto-statements \cite{Dijkstra68}. This |
225 precludes in the general case a compositional Hoare-style reasoning |
225 precludes in the general case a compositional Hoare-style reasoning |
226 about Turing programs. We provide such Hoare-rules for when it |
226 about Turing programs. We provide such Hoare-rules for when it |
227 \emph{is} possible to reason in a compositional manner (which is |
227 \emph{is} possible to reason in a compositional manner (which is |
228 fortunately quite often), but also tackle the more complicated case |
228 fortunately quite often), but also tackle the more complicated case |
229 when we translate abacus programs into Turing programs. This |
229 when we translate abacus programs into Turing programs. This |
1069 \begin{center} |
1069 \begin{center} |
1070 @{thm tcontra_def} |
1070 @{thm tcontra_def} |
1071 \end{center} |
1071 \end{center} |
1072 |
1072 |
1073 \noindent |
1073 \noindent |
1074 Suppose @{thm (prem 1) "tcontra_halt"}. Given the invariants on the |
1074 Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants on the |
1075 left, we can derive the following Hoare-pair for @{term tcontra} on the right. |
1075 left, we can derive the following Hoare-pair for @{term tcontra} on the right. |
1076 |
1076 |
1077 \begin{center}\small |
1077 \begin{center}\small |
1078 \begin{tabular}{@ {}c@ {\hspace{-10mm}}c@ {}} |
1078 \begin{tabular}{@ {}c@ {\hspace{-10mm}}c@ {}} |
1079 \begin{tabular}[t]{@ {}l@ {}} |
1079 \begin{tabular}[t]{@ {}l@ {}} |
1096 |
1096 |
1097 \noindent |
1097 \noindent |
1098 This Hoare-pair contradicts our assumption that @{term tcontra} started |
1098 This Hoare-pair contradicts our assumption that @{term tcontra} started |
1099 with @{term "<(code tcontra)>"} halts. |
1099 with @{term "<(code tcontra)>"} halts. |
1100 |
1100 |
1101 Suppose @{thm (prem 1) "tcontra_unhalt"}. Again given the invariants on the |
1101 Suppose @{thm (prem 1) "tcontra_unhalt"} holds. Again given the invariants on the |
1102 left, we can derive the Hoare-triple for @{term tcontra} on the right. |
1102 left, we can derive the Hoare-triple for @{term tcontra} on the right. |
1103 |
1103 |
1104 \begin{center}\small |
1104 \begin{center}\small |
1105 \begin{tabular}{@ {}c@ {\hspace{-17mm}}c@ {}} |
1105 \begin{tabular}{@ {}c@ {\hspace{-18mm}}c@ {}} |
1106 \begin{tabular}[t]{@ {}l@ {}} |
1106 \begin{tabular}[t]{@ {}l@ {}} |
1107 @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\ |
1107 @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\ |
1108 @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\ |
1108 @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\ |
1109 @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"} |
1109 @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"} |
1110 \end{tabular} |
1110 \end{tabular} |
1137 Boolos et al \cite{Boolos87} use abacus machines as a stepping stone |
1137 Boolos et al \cite{Boolos87} use abacus machines as a stepping stone |
1138 for making it less laborious to write Turing machine |
1138 for making it less laborious to write Turing machine |
1139 programs. Abacus machines operate over a set of registers $R_0$, |
1139 programs. Abacus machines operate over a set of registers $R_0$, |
1140 $R_1$, \ldots{} each being able to hold an arbitrary large natural |
1140 $R_1$, \ldots{} each being able to hold an arbitrary large natural |
1141 number. We use natural numbers to refer to registers; we also use a natural number |
1141 number. We use natural numbers to refer to registers; we also use a natural number |
1142 to represent a program counter. An abacus |
1142 to represent a program counter and jumping ``addresses''. An abacus |
1143 program is a list of \emph{statements} defined by the datatype: |
1143 program is a list of \emph{statements} defined by the datatype: |
1144 |
1144 |
1145 \begin{center} |
1145 \begin{center} |
1146 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
1146 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
1147 @{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\ |
1147 @{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\ |
1160 @{thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]} |
1160 @{thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]} |
1161 \end{center} |
1161 \end{center} |
1162 |
1162 |
1163 \noindent |
1163 \noindent |
1164 Running such a program means we start with the first instruction |
1164 Running such a program means we start with the first instruction |
1165 then execute statements one after the other, unless there is a jump. For |
1165 then execute one statements after the other, unless there is a jump. For |
1166 example the second statement the jump @{term "Goto 0"} in @{term clear} means |
1166 example the second statement the jump @{term "Goto 0"} in @{term clear} means |
1167 we jump back to the first statement closing the loop. Like with our |
1167 we jump back to the first statement closing the loop. Like with our |
1168 Turing machines, we fetch statements from an abacus program such |
1168 Turing machines, we fetch statements from an abacus program such |
1169 that a jump out of ``range'' behaves like a @{term "Nop"}-action. In |
1169 that a jump out of ``range'' behaves like a @{term "Nop"}-action. In |
1170 this way it is easy to define a function @{term steps} that |
1170 this way it is easy to define a function @{term steps} that |