equal
deleted
inserted
replaced
1168 example the second instruction the jump @{term "Goto 0"} in @{term clear} means |
1168 example the second instruction the jump @{term "Goto 0"} in @{term clear} means |
1169 we jump back to the first instruction closing the loop. Like with our |
1169 we jump back to the first instruction closing the loop. Like with our |
1170 Turing machines, we fetch instructions from an abacus program such |
1170 Turing machines, we fetch instructions from an abacus program such |
1171 that a jump out of ``range'' behaves like a @{term "Nop"}-action. In |
1171 that a jump out of ``range'' behaves like a @{term "Nop"}-action. In |
1172 this way it is easy to define a function @{term steps} that |
1172 this way it is easy to define a function @{term steps} that |
1173 executes @{term n} instructions of an abacus program. By convention |
1173 executes @{term n} instructions of an abacus program. A \emph{configuration} |
|
1174 of an abacus machine is the program counter together with a snapshot of |
|
1175 all registers. |
|
1176 By convention |
1174 the value calculated by an abacus program is stored in the |
1177 the value calculated by an abacus program is stored in the |
1175 last register (the register with the highest index). |
1178 last register (the register with the highest index). |
1176 |
1179 |
1177 The main point of abacus programs is to be able to translate them to |
1180 The main point of abacus programs is to be able to translate them to |
1178 Turing machine programs. Registers and their content are represented by |
1181 Turing machine programs. Registers and their content are represented by |
1242 contains @{text Goto}s all over the place. The unfortunate result is |
1245 contains @{text Goto}s all over the place. The unfortunate result is |
1243 are needed to translate each abacus instructionthat we cannot |
1246 are needed to translate each abacus instructionthat we cannot |
1244 use our Hoare-rules for reasoning about sequentially composed |
1247 use our Hoare-rules for reasoning about sequentially composed |
1245 programs. Instead we have to treat the Turing machine as one ``block'' |
1248 programs. Instead we have to treat the Turing machine as one ``block'' |
1246 and show as invariant that it performs the same operations |
1249 and show as invariant that it performs the same operations |
1247 as the abacus program. |
1250 as the abacus program. For this we have to show that for each |
|
1251 configuration of an abacus machine the @{term step}-function |
|
1252 is simulated by zero or more steps in our constructed Turing |
|
1253 machine. |
1248 |
1254 |
1249 |
1255 |
1250 *} |
1256 *} |
1251 |
1257 |
1252 |
1258 |