To use or not to use the goto statement: Programming styles viewed from Hoare Logic

There has been a vast amount of debate on the goto issue: i.e., the issue whether to use or not to use the goto statement initiated by Dijkstra in his famous Letter to the Editor of CACM and his proposal of ‘Structured Programming’. However, except for the goto-less programming style by Mills based on theoretical results on the expressibility of control flow diagrams, there have hardly been any scientific accounts on this issue from Dijkstra’s own viewpoint of the correctness of programs. In this work, we reconsider this seemingly old-tired issue from the viewpoint of Hoare Logic, the most well-known framework for correctness proof of programs. We show that, in two cases, the with-goto programming styles are more suitable for proving correctness in Hoare Logic than the corresponding without-goto ones; that is, in each of two cases, the without-goto style requires more complicated assertions in the proof-outline than the with-goto one. The first case is on the use of the goto statement for escaping from nested loops and the second case is on the use of the goto statement for expressing state transitions in programming through the finite state machine model. Hence, in both cases, the use of the goto statement can be justified from the viewpoint of the correctness proof in Hoare Logic.