3 ms·
No goto? Funny, but there is actually a Hoare rule for goto (by Hoare himself), and a rather straightforward one: { pre(L) } S; { P } -------------
by Joker_vD 6y ago
No goto? Funny, but there is actually a Hoare rule for goto (by Hoare himself), and a rather straightforward one:
{ pre(L) } S; { P }
------------------------
{ pre(L) } L: S; { P }
{ pre(L) } goto L; { false }
You just have to use the same precondition pre(L) for every mention of the label L.