In this paper we present a formal characterization of goto statements in terms of Dijkstra’s weakest precondition model. We show that the goto semantics so defined captures the nature of goto statements and even applies when jumping into program constructs like alternation and repetition. With this formal definition of goto, we can characterize break and continue statements in a loop, and prove a new form of the traditional loop invariance theorem, which works with break and continue statements and has a special instance for an invariance theorem about goto statements. We, in turn, take this invariance theorem for goto statements as a basis and generalize it, although not as straightforward as hoped, to treat the multiple sequentially composed labels, which can cover essentially all scenarios.

This paper takes a new look at Clint and Hoare’s proof rule for goto statements, published almost fifty years ago, and discloses several new findings unnoticed before. We start out to propose that the rule take small changes, so it becomes more manageable. As we explore further, we have discovered a simple total correctness rule for goto statements, which uses the variant function to argue about termination just like we do for loops. We further extend the idea and have obtained general proof rules, applicable to multiple labels, for both partial and total correctness of goto statements. Those rules, although complex in appearance, are easy to use in practice. We have successfully applied them to prove programs that current published rules failed to.