The structured program theorem

Read first: Reducibility and loop detection, Eliminating GOTOs

A GOTO lands wherever its label happens to be, so a cycle can be entered at two different points — and a cycle with two ways in has no single top to hang a WHILE on. Rewrite rules that fix one jump shape at a time only cover the shapes someone wrote a rule for, which leaves open whether every flowchart has a structured equivalent at all.

Below, a cycle entered at either A or B is rewritten twice: once by the generic one-loop dispatch, which invents a variable loc to remember where it is, and once by copying doA() to the entry, which needs no new variable. Both run doA(), doB(), doA(), doB() on the same inputs as the original.

Reducible, irreducible and natural loop are defined in reducibility and loop detection.

The example: a cycle with two ways in

This is the two-entry cycle. The test at the top sends control into the cycle A → B → c? at A or at B; c? either goes round again or leaves:

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"])

The answer is two structured programs, each using only sequence, IF and WHILE, and each matching the graph above step for step. They differ in what they had to add:

The first row is the generic machine. It replaces each arrow in the graph with an assignment to loc, then dispatches on loc inside one loop:

loc := Entry
while (loc != Exit) {
  if (loc = Entry)  loc := start_at_b ? B : A
  else if (loc = A) { doA(); loc := B }
  else              { doB(); loc := c ? A : Exit }
}

The second row works because this cycle has only one way out, the c? test. A copy of doA() before the loop absorbs the false arrow from start_at_b?, and what is left has a single top:

if (!start_at_b) doA();
doB();
while (c) { doA(); doB(); }

Drawn as a graph, the copied doA() sits outside the loop, and the only way into the cycle is through while c?:

flowchart TD
    S{"start_at_b?"} -->|false| A1["doA()"]
    S -->|true| B1["doB()"]
    A1 --> B1
    B1 --> W{"while c?"}
    W -->|true| A2["doA()"]
    A2 --> B2["doB()"]
    B2 -.->|back to while test| W
    W -->|false| X(["Exit"])

With start_at_b true, the top IF skips the first doA(), just as the original graph enters at B.

Step by step: one variable, one loop

The walk below runs the one-loop dispatch from the first fragment, drawn as a flowchart. Each step is one pass of the WHILE; the highlighted box is the arm that pass takes (in the last step, the loop test that ends it), and the chips show what it does to loc. Inputs: start_at_b false, c true the first time and false the second.

The table lines the walk up with the original graph and with the no-variable fragment. Each row is one move in the original; the three programs make the same calls in the same order:

The loc after column is the price of the generic version. loc is state the original graph never needed: in the graph, the program's own position is its memory of "where next". The right-hand column shows this program did not need to pay it. Since the cycle has one exit, Kosaraju's criterion (below) says no new variable is required, and copying doA() was enough.

The dispatch in the walk is not quite Böhm and Jacopini's own construction; their proof transforms the flowchart piece by piece. Harel calls the one-loop version the "folk" theorem:^[7] a simpler argument that has come to stand in for the original. Its recipe is what the first fragment shows. Name every statement, wrap the whole program in one WHILE, and replace every jump with an assignment to loc. Nothing jumps; the loop simply runs again with a different value.

The theorem the walk just used

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

Each line of the box was used in the walk. Sequence: step 1's arm doA(); loc := B runs two statements in order. Selection: in steps 1 to 4 the IF cascade picks one arm, and in step 2 the c ? A : Exit test picks A. Iteration: each of those steps is one more pass of the single WHILE, and its test loc = Exit? ends the loop in step 5. The walk's flowchart contains nothing else: no jump and no label.

Why the local rewrites stop here

Eliminating GOTOs gives three surgical rewrites: a forward jump becomes an IF, a backward jump becomes a loop, and a jump into or out of a nested scope is moved one level at a time. Each one needs a single place to put its block. The example's cycle does not have one. Listing every arrow into each of its three nodes:

Two rows have an arrow from outside, so the cycle has two entries and no single header. None of the three rules applies to it directly. The question the rules quietly assume an answer to is whether some structured rewrite always exists, however the jumps are arranged. The two fragments in the example show one does here; the theorem says one always does.

When you don't need the generic machine

The one-loop dispatch works on anything, reducible or not, which is also why it is overkill almost everywhere. It flattens the entire program into one dispatch loop, as the walk's flowchart does, throwing away whatever block structure the original already had. How many ways in and how many ways out a region has decides what it will actually cost:

The first row is any program built from reducible, properly nested natural loops. Eliminating GOTOs' three rewrites rebuild sequence, selection and iteration statement by statement there, and leave every block that was already well-formed untouched. The second row's irreducibility, which DJ graphs and natural loop bodies detects, means the cycle cannot be kept as written. The third row needs a flag even when the loop is perfectly reducible; eliminating GOTOs' outward climb already adds exactly such flags.

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, 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 like the walk's loc is allowed. Kozen and Tseng^[5] give a three-state automaton small enough to state directly: from any one state, each of the other two is reachable by a single labelled transition. A sketch of that sentence only, not the paper's figure (transition labels and tests left out):

  flowchart LR
      S1((1)) --> S2((2))
      S2 --> S1
      S2 --> S3((3))
      S3 --> S2
      S1 --> S3
      S3 --> S1
  

  Every pair of states forms its own cycle, 1⇄2, 2⇄3 and 1⇄3, and no state lies on all three. There is no repeated structure that a nested IF/WHILE could exploit. The only escape, other than an extra variable, is a WHILE with multi-level break, breaking out of several nested loops at once. Kosaraju showed this is exactly as powerful as a flag variable, with its own strict hierarchy: for every depth n, 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 and iteration with no new variable, copying code where needed as the example did, if and only if it contains no loop with two distinct exits. This loop has two: an early special? test at the top, and the ordinary cond? test at the bottom.

  flowchart TD
      LoopTop{"special?"} -->|yes| AfterLoop(["AfterLoop"])
      LoopTop -->|no| DoWork["doWork()"]
      DoWork --> CondCheck{"cond?"}
      CondCheck -->|yes| LoopTop
      CondCheck -->|no| AfterLoop
  

  Without break, the fix is a flag that merges the two exits into one before the loop's own test 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| WhileTest
  

  The two graphs agree on three cases, traced through each by hand:

  case	special? answers	cond? answers	doWork() calls, original	with flag
  early exit on the first pass	yes	—	0	0
  two ordinary passes, then early exit	no, no, yes	yes, yes	2	2
  two ordinary passes, then normal exit	no, no	yes, no	2	2

  The same shape, and the same fix, is eliminating GOTOs' fresh-flag mechanism for a jump into an outer scope. Two separate things are true there. The theorem: some flag like exited_early is necessary, so its appearance is not an implementation accident. The implementation bug: that page's "What goes wrong" notes the invented flag's name is a fixed constant, reused by every climb of every jump. That is a defect in how the flag is named, not in the need for one.
• The flag is forced by atomic tests, not by every language. The no-variable characterization assumes, as Kosaraju's model does, that each test is atomic: one predicate, evaluated once at its own node, like the diamonds in the two graphs above. Allow compound conditions and the two-exit loop needs no flag:

  if (!special) {
    doWork();
    while (cond && !special) doWork();
  }

  This evaluates special, doWork(), cond, special, … in exactly the original graph's order; when cond is false, && stops before testing special, just as the original leaves at cond?. The flag is what the atomic-test model forces.

Where this shows up in reverse engineering

• Why eliminating GOTOs' local rewrites are safe to try first: the one-loop dispatch in the walk is the theoretical guarantee underneath them. Whatever shape those targeted rules cannot finish, a structured equivalent is known to exist. It is a guarantee, not a fallback the pipeline runs: nothing in eliminating GOTOs implements this construction, and its inward and sideways moves are not implemented either.
• 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 the example's flowchart than to an AST. That has historically been answered with targeted algorithms for multi-level break/continue, not the textbook construction directly, for the blowup reasons in what goes wrong.

This page produced three kinds of fine print, and each can turn up in a restructuring tool's output:

None of the three is a bug report against the tool. Each is this theorem's own fine print showing up in the generated code, and recognizing it as such is cheaper than debugging it as a surprise.

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 cobol-rekt, the generic one-loop construction from the walk is not implemented at all. Eliminating GOTOs gets by without it because COBOL paragraph labels sit at the top level of their section, so a source jump only ever has to move outward. The construction is a theoretical guarantee, not a pipeline fallback: it is what makes attempting the local, structure-preserving rewrites reasonable, since whatever they cannot finish is known to have some structured equivalent.

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.
7. D. Harel. "On Folk Theorems." Communications of the ACM, 23(7), July 1980, pp. 379–389. Traces the single-loop program-counter construction, and how it came to be credited to Böhm and Jacopini.