1698 presentations leave out any arguments why these Turing machines |
1698 presentations leave out any arguments why these Turing machines |
1699 should be correct. This means the reader is left |
1699 should be correct. This means the reader is left |
1700 with the task of finding appropriate invariants and measures for |
1700 with the task of finding appropriate invariants and measures for |
1701 showing the correctness and termination of these Turing machines. |
1701 showing the correctness and termination of these Turing machines. |
1702 Whenever we can use Hoare-style reasoning, the invariants are |
1702 Whenever we can use Hoare-style reasoning, the invariants are |
1703 relatively straightforward and much smaller than for example the |
1703 relatively straightforward and as a point of comparison much smaller than for example the |
1704 invariants used by Myreen in a correctness proof of a garbage collector |
1704 invariants used by Myreen in a correctness proof of a garbage collector |
1705 written in machine code \cite[Page 76]{Myreen09}. However, the invariant |
1705 written in machine code \cite[Page 76]{Myreen09}. However, the invariant |
1706 needed for the abacus proof, where Hoare-style reasoning does not work, is |
1706 needed for the abacus proof, where Hoare-style reasoning does not work, is |
1707 similar in size as the one by Myreen and finding a sufficiently |
1707 similar in size as the one by Myreen and finding a sufficiently |
1708 strong one took us, like Myreen, something on the magnitude of |
1708 strong one took us, like Myreen, something on the magnitude of |
1709 weeks. |
1709 weeks. |
1710 |
1710 |
1711 Our reasoning about the invariants is not much supported by the |
1711 Our reasoning about the invariants is not much supported by the |
1712 automation beyond the standard automation tools available in Isabelle/HOL. |
1712 automation beyond the standard automation tools available in Isabelle/HOL. |
1713 There is however a tantalising connection |
1713 There is however a tantalising connection |
1714 between our work and very recent work \cite{Jensen13} on verifying |
1714 between our work and very recent work by Jensen et al \cite{Jensen13} on verifying |
1715 X86 assembly code that might change that. They observed a similar phenomenon with assembly |
1715 X86 assembly code that might change that. They observed a similar phenomenon with assembly |
1716 programs where Hoare-style reasoning is sometimes possible, but |
1716 programs where Hoare-style reasoning is sometimes possible, but |
1717 sometimes it is not. In order to ease their reasoning, they |
1717 sometimes it is not. In order to ease their reasoning, they |
1718 introduced a more primitive specification logic, on which |
1718 introduced a more primitive specification logic, on which |
1719 Hoare-rules can be provided for special cases. It remains to be |
1719 Hoare-rules can be provided for special cases. It remains to be |