A wp Characterization of Jump Statements

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.