Don Knuth, "Structured Programming with go to Statements":
"Just recently, however, Hoare has shown that there is, in fact, a rather simple way to give an axiomatic definition of go to statements; indeed, he wishes quite frankly that it hadn't been quite so simple....
"Informally, α(L) represents the desired state of affairs at label L; this definition says essentially that a program is correct if α(L) holds at L and before all "go to L" statements, and that control never "falls through" a go to statement to the following text. Stating the assertions α(L) is analogous to formulating loop invariants. Thus, it is not difficult to deal formally with tortuous program structure if it turns out to be necessary; all we need to know is the "meaning" of each label."