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