Graph algorithms · why a restructuring tool is even possible

The structured program theorem

Any flowchart, however tangled its jumps, can be rewritten using nothing but sequence, selection and iteration. That guarantee is why a GOTO-elimination tool is allowed to exist at all — and the guarantee is weaker than it sounds.

Where this shows up in reverse engineering

This theorem is the reason any migration or decompilation tool is allowed to promise "we can always produce structured output" in the first place — and the fine print behind that promise is why real tools do not actually reach for the universal construction.

The problem

Arbitrary GOTOs make a program's control flow depend on where a jump happens to land, not on any block structure visible in the text. Eliminating GOTOs gives three surgical rewrites for the common shapes — forward past some statements, backward to a label, into or out of a nested scope — but surgical rules only cover the shapes someone thought to write a rule for. The question those rules quietly assume an answer to: is there always some way to rewrite any flowchart using only sequence, selection and iteration, no matter how its jumps are arranged? Yes. That is the theorem this page is about.

The theorem

Böhm and Jacopini, 1966:[1] any deterministic flowchart program is equivalent to one built from only three ways of combining statements —

Sequence — run one statement, then another.
Selection — run one of two statements, chosen by a boolean test (IF).
Iteration — run a statement repeatedly while a boolean test holds (WHILE).

Nothing else — no jump, no label — is needed to express any control flow a flowchart could have, including the irreducible two-entry cycle from reducibility and loop detection that none of eliminating GOTOs' three rules handle directly. The original proof's construction, however, buys this generality at a cost it does not advertise in the one-sentence version: it may need to invent a new variable to do it.

The construction: one flag, one loop

The idea behind Böhm and Jacopini's construction, stripped to its essentials: give every statement a name, wrap the whole program in one WHILE loop, and replace every jump with an assignment to a variable that says which statement comes next. The loop's own body becomes a cascade of IFs dispatching on that variable's current value. Nothing jumps anywhere; the loop simply runs again with a different value.

Run on the two-entry cycle — a shape with no single header, so none of eliminating GOTOs' rules apply to it directly:

flowchart TD
    Entry{"start_at_b?"} -->|true| B
    Entry -->|false| A
    A["A: doA()"] --> B["B: doB()"]
    B --> Cond{"c?"}
    Cond -->|true| A
    Cond -->|false| ExitNode(["Exit"])

Becomes, with one auxiliary variable loc standing in for "which statement is next":

flowchart TD
    Start(["loc := Entry"]) --> LoopTest{"loc = Exit?"}
    LoopTest -->|yes| Done(["done"])
    LoopTest -->|no| CheckEntry
    subgraph Body["loop body — one dispatch pass"]
        CheckEntry{"loc = Entry?"} -->|yes| SetFromEntry["loc := start_at_b ? B : A"]
        CheckEntry -->|no| CheckA{"loc = A?"}
        CheckA -->|yes| DoA["doA(); loc := B"]
        CheckA -->|no| DoB["doB(); loc := c ? A : Exit"]
    end
    SetFromEntry -.->|back to top of while| LoopTest
    DoA -.->|back to top of while| LoopTest
    DoB -.->|back to top of while| LoopTest

One WHILE, holding a cascade of nested IFs, nothing else — exactly the three structures the theorem allows. Walking it with start_at_b = false and c true then false, dispatch pass by dispatch pass:

Running the structured version, dispatch pass by dispatch pass (6 steps)
  1. loc = Entry. start_at_b is false, so the entry dispatch sets loc := A.

    flowchart TD
        Start(["loc := Entry"]) --> LoopTest{"loc = Exit?"}
        LoopTest -->|yes| Done(["done"])
        LoopTest -->|no| CheckEntry
        subgraph Body["loop body — one dispatch pass"]
            CheckEntry{"loc = Entry?"} -->|yes| SetFromEntry["loc := start_at_b ? B : A"]
            CheckEntry -->|no| CheckA{"loc = A?"}
            CheckA -->|yes| DoA["doA(); loc := B"]
            CheckA -->|no| DoB["doB(); loc := c ? A : Exit"]
        end
        SetFromEntry -.->|back to top of while| LoopTest
        DoA -.->|back to top of while| LoopTest
        DoB -.->|back to top of while| LoopTest
        class SetFromEntry changed
        classDef changed fill:#f5b041,stroke:#f5b041,color:#000
    

    loc

    Entry → A
  2. loc = A: doA() runs, loc := B.

    flowchart TD
        Start(["loc := Entry"]) --> LoopTest{"loc = Exit?"}
        LoopTest -->|yes| Done(["done"])
        LoopTest -->|no| CheckEntry
        subgraph Body["loop body — one dispatch pass"]
            CheckEntry{"loc = Entry?"} -->|yes| SetFromEntry["loc := start_at_b ? B : A"]
            CheckEntry -->|no| CheckA{"loc = A?"}
            CheckA -->|yes| DoA["doA(); loc := B"]
            CheckA -->|no| DoB["doB(); loc := c ? A : Exit"]
        end
        SetFromEntry -.->|back to top of while| LoopTest
        DoA -.->|back to top of while| LoopTest
        DoB -.->|back to top of while| LoopTest
        class DoA changed
        classDef changed fill:#f5b041,stroke:#f5b041,color:#000
    

    loc

    doA()A → B
  3. loc = B: doB() runs. c is true this time, so loc := A.

    flowchart TD
        Start(["loc := Entry"]) --> LoopTest{"loc = Exit?"}
        LoopTest -->|yes| Done(["done"])
        LoopTest -->|no| CheckEntry
        subgraph Body["loop body — one dispatch pass"]
            CheckEntry{"loc = Entry?"} -->|yes| SetFromEntry["loc := start_at_b ? B : A"]
            CheckEntry -->|no| CheckA{"loc = A?"}
            CheckA -->|yes| DoA["doA(); loc := B"]
            CheckA -->|no| DoB["doB(); loc := c ? A : Exit"]
        end
        SetFromEntry -.->|back to top of while| LoopTest
        DoA -.->|back to top of while| LoopTest
        DoB -.->|back to top of while| LoopTest
        class DoB changed
        classDef changed fill:#f5b041,stroke:#f5b041,color:#000
    

    loc

    doB()B → A (c held)
  4. loc = A again: doA() runs a second time, loc := B.

    flowchart TD
        Start(["loc := Entry"]) --> LoopTest{"loc = Exit?"}
        LoopTest -->|yes| Done(["done"])
        LoopTest -->|no| CheckEntry
        subgraph Body["loop body — one dispatch pass"]
            CheckEntry{"loc = Entry?"} -->|yes| SetFromEntry["loc := start_at_b ? B : A"]
            CheckEntry -->|no| CheckA{"loc = A?"}
            CheckA -->|yes| DoA["doA(); loc := B"]
            CheckA -->|no| DoB["doB(); loc := c ? A : Exit"]
        end
        SetFromEntry -.->|back to top of while| LoopTest
        DoA -.->|back to top of while| LoopTest
        DoB -.->|back to top of while| LoopTest
        class DoA changed
        classDef changed fill:#f5b041,stroke:#f5b041,color:#000
    

    loc

    doA()A → B
  5. loc = B again: doB() runs a second time. c is false this time, so loc := Exit.

    flowchart TD
        Start(["loc := Entry"]) --> LoopTest{"loc = Exit?"}
        LoopTest -->|yes| Done(["done"])
        LoopTest -->|no| CheckEntry
        subgraph Body["loop body — one dispatch pass"]
            CheckEntry{"loc = Entry?"} -->|yes| SetFromEntry["loc := start_at_b ? B : A"]
            CheckEntry -->|no| CheckA{"loc = A?"}
            CheckA -->|yes| DoA["doA(); loc := B"]
            CheckA -->|no| DoB["doB(); loc := c ? A : Exit"]
        end
        SetFromEntry -.->|back to top of while| LoopTest
        DoA -.->|back to top of while| LoopTest
        DoB -.->|back to top of while| LoopTest
        class DoB changed
        classDef changed fill:#f5b041,stroke:#f5b041,color:#000
    

    loc

    doB()B → Exit (c failed)
  6. loc = Exit: the loop's own test now fails. Done.

    flowchart TD
        Start(["loc := Entry"]) --> LoopTest{"loc = Exit?"}
        LoopTest -->|yes| Done(["done"])
        LoopTest -->|no| CheckEntry
        subgraph Body["loop body — one dispatch pass"]
            CheckEntry{"loc = Entry?"} -->|yes| SetFromEntry["loc := start_at_b ? B : A"]
            CheckEntry -->|no| CheckA{"loc = A?"}
            CheckA -->|yes| DoA["doA(); loc := B"]
            CheckA -->|no| DoB["doB(); loc := c ? A : Exit"]
        end
        SetFromEntry -.->|back to top of while| LoopTest
        DoA -.->|back to top of while| LoopTest
        DoB -.->|back to top of while| LoopTest
        class LoopTest,Done changed
        classDef changed fill:#f5b041,stroke:#f5b041,color:#000
    

Both programs, run on the same inputs, visit Entry, A, B, A, B, Exit and call doA(), doB(), doA(), doB() in that order — identical traces, confirmed by running both side by side rather than asserted. The structured version earns that only by inventing loc: a piece of state the original flowchart never needed, because the original used the program's own location as its memory of "where next."

When you don't need the generic machine

The construction above works unconditionally — reducible or not, nested or not — which is also why it is overkill almost everywhere. It flattens the entire program into one dispatch loop, throwing away whatever block structure the original already had. A program built entirely out of reducible, properly nested natural loops never needs it: eliminating GOTOs' three local rewrites — forward jump to IF, backward jump to loop, cross-scope jump climbed one level at a time — reconstruct the same sequence/selection/iteration shape statement by statement, keeping every block that was already well-formed untouched. DJ graphs and natural loop bodies is what tells you, before you start, whether the local rewrites alone will finish the job or whether some region needs this page's generic fallback instead.

What goes wrong

Where this is used

This theorem is the reason Dijkstra's 1968 argument against GOTO[2] was an argument about style, not capability — nothing expressible with jumps becomes inexpressible without them. IBM applied a structuring algorithm built on it directly to COBOL in the 1980s, as the COBOL Structuring Facility.[6] In this repository, the generic one-flag-one-loop construction on this page is the fallback eliminating GOTOs never has to reach for in practice, because real COBOL sections are almost always already reducible — but it is the guarantee that makes attempting the local, structure-preserving rewrites safe in the first place: whatever those rules cannot finish, this page's construction always can.

References

  1. C. Böhm and G. Jacopini. "Flow Diagrams, Turing Machines and Languages with Only Two Formation Rules." Communications of the ACM, 9(5), May 1966, pp. 366–371. The theorem itself.
  2. E. W. Dijkstra. "Go To Statement Considered Harmful." Communications of the ACM, 11(3), March 1968, pp. 147–148.
  3. E. Ashcroft and Z. Manna. "The Translation of GOTO Programs into WHILE Programs." Proceedings of IFIP Congress 71, Volume 1, 1972, pp. 250–255. First proof that an auxiliary variable can be unavoidable.
  4. S. R. Kosaraju. "Analysis of Structured Programs." Proceedings of the 5th ACM Symposium on Theory of Computing (STOC '73), 1973, pp. 240–252. The no-two-distinct-exits characterization and the multi-level-break hierarchy.
  5. D. Kozen and W.-L. D. Tseng. "The Böhm–Jacopini Theorem Is False, Propositionally." Mathematics of Program Construction (MPC 2008), LNCS 5133, 2008, pp. 177–192. The three-state counterexample this page's limitation cites.
  6. R. C. Linger and H. D. Mills. "A Case Study in Cleanroom Software Engineering: The IBM COBOL Structuring Facility." Proceedings of the 12th International Computer Software and Applications Conference (COMPSAC '88), 1988, pp. 10–17.