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.
- Why eliminating GOTOs' local rewrites are safe to try first: this page's generic one-flag-one-loop construction is the guarantee sitting underneath them. Whatever those targeted rules cannot finish for lack of a matching shape, this page's fallback always can — which is what makes attempting the structure-preserving rules first a safe bet rather than a gamble.
- Bytecode decompilers face a sharper version of the same problem: the JVM's branches are offset-based jumps, not nested blocks, so a decompiler is reconstructing structured source from something closer to this page's flowchart than to an AST — historically answered with targeted algorithms for multi-level
break/continue, not the textbook construction directly, for exactly the blowup reasons this page's limitations describe. - A warning worth carrying into any restructuring tool's output: an invented flag variable or a region that had to be duplicated to avoid one is not a bug report against the tool — it is this theorem's own fine print showing up in the generated code, and recognizing it as such is cheaper than debugging it as if it were a surprise.
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 —
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)
loc = Entry.start_at_bis false, so the entry dispatch setsloc := 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:#000loc
Entry → Aloc = 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:#000loc
doA()A → Bloc = B:doB()runs.cis true this time, soloc := 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:#000loc
doB()B → A (c held)loc = Aagain: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:#000loc
doA()A → Bloc = Bagain:doB()runs a second time.cis false this time, soloc := 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:#000loc
doB()B → Exit (c failed)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
- "No extra variable is ever needed" is false. The one-sentence version of this theorem is often repeated without Böhm and Jacopini's own auxiliary-variable caveat attached — and dropping it is not a harmless simplification. Ashcroft and Manna[3] and, independently, Kosaraju[4] proved that some flowcharts have no equivalent
WHILE-program at all unless an auxiliary variable likelocabove is allowed; Kozen and Tseng[5] give a three-state automaton small enough to state directly: three states where, from any one of them, every one of the other two is reachable by a single labelled transition, with no repeated structure anywhere a nestedIF/WHILEcould exploit. The only escape, other than an extra variable, is aWHILEwith multi-levelbreak— breaking out of several nested loops at once — which Kosaraju showed is exactly as powerful as a flag variable, with its own strict hierarchy: for every depthn, some program needs a break that deep and no shallower.[4] - Avoiding the variable is possible exactly when every loop has one exit. Kosaraju's cleaner characterization:[4] a flowchart restructures into sequence/selection/iteration with no new variable if and only if it contains no loop with two distinct exits. A loop with two separate ways out — an early condition checked partway through the body, and the ordinary bottom-of-loop test — is exactly such a case:
flowchart TD LoopTop{"special?"} -->|yes| AfterLoop(["AfterLoop"]) LoopTop -->|no| DoWork["doWork()"] DoWork --> CondCheck{"cond?"} CondCheck -->|yes| LoopTop CondCheck -->|no| AfterLoopWithoutbreakavailable, the fix is the same flag-variable trick, merging the two exits into one before the loop's own test ever sees them:flowchart TD Start(["exited_early := False"]) --> WhileTest{"not exited_early?"} WhileTest -->|no| AfterLoop(["AfterLoop"]) WhileTest -->|yes| CheckSpecial{"special?"} CheckSpecial -->|yes| SetFlag["exited_early := True"] CheckSpecial -->|no| DoWork["doWork()"] DoWork --> CondCheck2{"cond?"} CondCheck2 -->|no| SetFlag2["exited_early := True"] CondCheck2 -.->|"yes, back to top of while"| WhileTest SetFlag -.->|back to top of while| WhileTest SetFlag2 -.->|back to top of while| WhileTestVerified against the original on three cases — an early exit on the first pass, two ordinary passes then an early exit, and two ordinary passes then a normal exit — all giving the identical count ofdoWork()calls. This is the same shape, and the same fix, as eliminating GOTOs' own fresh-flag mechanism for a jump into an outer scope: that page's "What goes wrong" already flags the invented flag name as not guaranteed fresh across two independent climbs — this is that same necessary variable, not an implementation accident.
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
- 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.
- E. W. Dijkstra. "Go To Statement Considered Harmful." Communications of the ACM, 11(3), March 1968, pp. 147–148.
- 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.
- 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.
- 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.
- 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.