Structured program theorem: Difference between revisions

Revision as of 23:47, 12 April 2020

Latest revision as of 19:58, 19 August 2025

(44 intermediate revisions by 25 users not shown)

Line 1:

{{short description|Control-flow graphs with 3 types of control structures can compute any computable function}}

The '''structured program theorem''', also called the '''Böhm–Jacopini theorem''',<ref name="kozen">{{cite book|url= http://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf |title=The Böhm–Jacopini Theorem Is False, Propositionally|author=[[Dexter Kozen]] and Wei-Lung Dustin Tseng|doi=10.1007/978-3-540-70594-9_11|journal=Mpc 2008|volume=5133|pages=177–192|series=Lecture Notes in Computer Science|year=2008|isbn=978-3-540-70593-2|citeseerx=10.1.1.218.9241}}</ref><ref>{{cite web|url=http://www.cse.buffalo.edu/~rapaport/111F04/greatidea3.html |title=CSE 111, Fall 2004, BOEHM-JACOPINI THEOREM |publisher=Cse.buffalo.edu |date=2004-11-22 |accessdate=2013-08-24}}</ref> is a result in [[programming language theory]]. It states that a class of [[control flow graph]]s (historically called [[flowchart]]s in this context) can compute any [[computable function]] if it combines subprograms in only three specific ways ([[control structure]]s). These are

{{use dmy dates|date=July 2025}}

The '''structured program theorem''', also called the '''Böhm–Jacopini theorem''',{{sfn|Kozen|Tseng|2008}}{{sfn|University at Buffalo|2004}} is a result in [[programming language theory]]. It states that a class of [[control-flow graph]]s (historically called [[flowchart]]s in this context) can compute any [[computable function]] if it combines subprograms in only three specific ways ([[control structure]]s). These are

#Executing one subprogram, and then another subprogram (sequence)

#Executing one of two subprograms according to the value of a [[Boolean data type|boolean]] expression (selection)

#Repeatedly executing a subprogram as long as a boolean expression is true (iteration)

The structured chart subject to these constraints, particularly the loop constraint implying a single exit (as described later in this article), may however use additional variables in the form of [[bit]]s (stored in an extra integer variable in the original proof) in order to keep track of information that the original program represents by the program ___location. The construction was based on Böhm's programming language [[P′′]].

The theorem forms the basis of [[structured programming]], a programming paradigm which eschews [[Goto|goto commands]] and exclusively uses subroutines, sequences, selection and iteration.

The theorem forms the basis of [[structured programming]], a programming paradigm which eschews [[Goto|goto commands]] and exclusively uses subroutines, sequences, selection and iteration.[[File:Structured program patterns.svg|Graphical representation of the three basic patterns of the structured program theorem — sequence, selection, and repetition — using [[Nassi–Shneiderman diagram|NS diagrams]] (blue) and [[flow chart]]s (green).|thumb|center|border|700px]]

== Origin and variants ==

The theorem is typically credited<ref name="Harel"/>{{rpsfn|Harel|1980|p=381}} to a 1966 paper by [[Corrado Böhm]] and [[{{ill|Giuseppe Jacopini]]|it}}.<ref>{{cite journalsfn|last=BohmBöhm|first=Corrado|author2=Giuseppe Jacopini |date=May 1966|title=Flow Diagrams, Turing Machines and Languages with Only Two Formation Rules|journal=[[Communications of the ACM]]|volume=9|issue=5|pages=366–371|doi=10.1145/355592.365646|citeseerx=10.1.1.119.9119}}</ref> [[David Harel|Harel]] wrote in 1980 that the Böhm–Jacopini paper enjoyed "universal popularity",<ref name="Harel"/>{{rpsfn|Harel|1980|p=381}} particularly with proponents of structured programming. Harel also noted that "due to its rather technical style [the 1966 Böhm–Jacopini paper] is apparently more often cited than read in detail"<ref name="Harel"/>{{rpsfn|Harel|1980|p=381}} and, after reviewing a large number of papers published up to 1980, Harel argued that the contents of the Böhm–Jacopini proof were usually misrepresented as a [[Mathematical folklore|folk theorem]] that essentially contains a simpler result, a result which itself can be traced to the inception of modern computing theory in the papers of [[John von Neumann|von Neumann]]{{sfn|Burks|Goldstine|von Neumann|1947}} and [[Stephen Cole Kleene|Kleene]].<ref name="Harel"/>{{rpsfn|Harel|1980|p=383}}

Harel also writes that the more generic name was proposed by [[Harlan Mills|H.D. Mills]] as "The Structure Theorem" in the early 1970s.<ref name="Harel">{{cite journalsfn|last=Harel|first=David|authorlink=David Harel|year=1980|titlep=On Folk Theorems|journal=Communications of the ACM|volume=23|issue=7|pages=379–389|doi=10.1145/358886.358892|url=http://www.wisdom.weizmann.ac.il/~dharel/SCANNED.PAPERS/OnFolkTheorems.pdf}}</ref>{{rp|381}}

=== Single-while-loop, folk version of the theorem ===

This version of the theorem replaces all the original program's control flow with a single global <code>while</code> loop that simulates a [[program counter]] going over all possible labels (flowchart boxes) in the original non-structured program. Harel traced the origin of this folk theorem to two papers marking the beginning of computing. One is the 1946 description of the [[von Neumann architecture]], which explains how a [[program counter]] operates in terms of a while loop. Harel notes that the single loop used by the folk version of the structured programming theorem basically just provides [[operational semantics]] for the execution of a flowchart on a von Neumann computer.<ref name="Harel"/>{{rpsfn|Harel|1980|p=383}} Another, even older source that Harel traced the folk version of the theorem is [[Stephen Kleene]]'s [[Kleene's T predicate|normal form theorem]] from 1936.<ref name="Harel"/>{{rpsfn|Harel|1980|p=383}}

[[Donald Knuth]] criticized this form of the proof, which results in [[pseudocode]] like the one below, by pointing out that the structure of the original program is completely lost in this transformation.<ref>{{citesfn|Knuth|1974|p=274}} journalSimilarly, Bruce Ian Mills wrote about this approach that "The spirit of block structure is a style, not a language. By simulating a von Neumann machine, we can produce the behavior of any spaghetti code within the confines of a block-structured language. This does not prevent it from being spaghetti."{{sfn|Mills|2005|p=279}}

| author = Donald Knuth

| title = Structured Programming with go to Statements

| journal = Computing Surveys

| volume = 6

| issue = 4

| year = 1974

| url =

| pages = 261–301

| doi = 10.1145/356635.356640

| citeseerx = 10.1.1.103.6084

}}</ref>{{rp|274}} Similarly, Bruce Ian Mills wrote about this approach that "The spirit of block structure is a style, not a language. By simulating a Von Neumann machine, we can produce the behavior of any spaghetti code within the confines of a block-structured language. This does not prevent it from being spaghetti."<ref name="Mills2005">{{cite book|author=Bruce Ian Mills|title=Theoretical Introduction to Programming|year=2005|publisher=Springer|isbn=978-1-84628-263-8|page=279}}</ref>

<sourcesyntaxhighlight lang="pascal">

p := 1

while p > 0 do

Line 46 ⟶ 36:

end if

end while

</syntaxhighlight>

</source>

=== Böhm and Jacopini's proof ===

{{expand section|date=July 2014}}

The proof in Böhm and Jacopini's paper proceeds by [[structural induction|induction on the structure]] of the flow chart.<ref name="Harel"/>{{rpsfn|Harel|1980|p=381}} Because it employed [[Subgraph isomorphism problem|pattern matching in graphs]], the proof of Böhm and Jacopini's was not really practical as a [[program transformation]] algorithm, and thus opened the door for additional research in this direction.<ref name="amma92"/>{{sfn|Ammarguellat|1992}}

=== Reversible version ===

The Reversible Structured Program Theorem{{sfn|Yokoyama|Axelsen|Glück|2016}} is an important concept in the field of [[reversible computing]]. It posits that any computation achievable by a reversible program can also be accomplished through a reversible program using only a structured combination of control flow constructs such as sequences, selections, and iterations. Any computation achievable by a traditional, irreversible program can also be accomplished through a reversible program, but with the additional constraint that each step must be reversible and some extra output.{{sfn|Bennett|1973}} Furthermore, any reversible unstructured program can also be accomplished through a structured reversible program with only one iteration without any extra output. This theorem lays the foundational principles for constructing reversible algorithms within a structured programming framework.

For the Structured Program Theorem, both local{{sfn|Böhm|Jacopini|1966}} and global{{sfn|Cooper|1967}} methods of proof are known. However, for its reversible version, while a global method of proof is recognized, a local approach similar to that undertaken by Böhm and Jacopini{{sfn|Böhm|Jacopini|1966}} is not yet known. This distinction is an example that underscores the challenges and nuances in establishing the foundations of reversible computing compared to traditional computing paradigms.

== Implications and refinements ==

The Böhm–Jacopini proof did not settle the question of whether to adopt [[structured programming]] for software development, partly because the construction was more likely to obscure a program than to improve it. On the contrary, it signalled the beginning of the debate. [[Edsger Dijkstra]]'s famous letter, "'''[[Considered Harmful|Go To Statement Considered Harmful]]'''," followed in 1968.<ref>{{cite journalsfn|last=Dijkstra|first=Edsger|authorlink=Edsger W. Dijkstra|year=1968|title=Go To Statement Considered Harmful|journal=Communications of the ACM|volume=11|issue=3|pages=147–148|doi=10.1145/362929.362947|url=http://www.acm.org/classics/oct95/|url-status=dead|archive-url=https://web.archive.org/web/20070703050443/http://www.acm.org/classics/oct95/|archive-date=2007-07-03|df=}}</ref>

Some academics took a purist approach to the Böhm–Jacopini result and argued that even instructions like <code>break</code> and <code>return</code> from the middle of loops are bad practice as they are not needed in the Böhm–Jacopini proof, and thus they advocated that all loops should have a single exit point. This purist approach is embodied in the [[Pascal (programming language)|Pascal programming language]] (designed in 1968–1969), which up to the mid-1990s was the preferred tool for teaching introductory programming classes in academia.<ref name="roberts">{{sfn|Roberts, E. [|1995] "[http://cs.stanford.edu/people/eroberts/papers/SIGCSE-1995/LoopExits.pdf Loop Exits and Structured Programming: Reopening the Debate]," ACM SIGCSE Bulletin, (27)1: 268–272.</ref>}}

[[Edward Yourdon]] notes that in the 1970s there was even philosophical opposition to transforming unstructured programs into structured ones by automated means, based on the argument that one needed to think in structured programming fashion from the get go. The pragmatic counterpoint was that such transformations benefited a large body of existing programs.<ref name="Yourdon1979">{{cite booksfn|author=E. N. Yourdon|title=Classics in Software Engineering|year=1979|publisherpp=Yourdon Press|isbn=978-0-917072-14-7|pages=[https://archive.org/details/classicsinsoftwa00your/page/49 49–50]|url-access=registration|url=https://archive.org/details/classicsinsoftwa00your/page/4950}}</ref> Among the first proposals for an automated transformation was a 1971 paper by Edward Ashcroft and [[Zohar Manna]].<ref>{{cite journalsfn|last=Ashcroft|first=Edward|author2=Zohar Manna |year=1971|title=The translation of go to programs to 'while' programs|journal=[[Proceedings of IFIP Congress]]}} The paper, which is difficult to obtain in the original conference proceedings due to their limited distribution, was republished in Yourdon's 1979 book pp. 51-65</ref>

The direct application of the Böhm–Jacopini theorem may result in additional local variables being introduced in the structured chart, and may also result in some [[code duplication]].<ref name="WattFindlay2004">{{cite booksfn|author1=David Anthony Watt|author2=William Findlay|title=Programming language design concepts|year=2004|publisher=John Wiley & Sons|isbn=978-0-470-85320-7|page=228}}</ref> The latter issue is called the [[loop and a half problem]] in this context.<ref name="LoudenLambert2011">{{cite booksfn|author1=Kenneth C. Louden|author2=Kenneth A. Lambert|title=Programming Languages: Principles and Practices|year=2011|publisher=Cengage Learning|isbn=978-1-111-52941-3|pages=422–423|edition=3}}</ref> Pascal is affected by both of these problems and according to empirical studies cited by [[Eric S. Roberts]], student programmers had difficulty formulating correct solutions in Pascal for several simple problems, including writing a function for searching an element in an array. A 1980 study by Henry Shapiro cited by Roberts found that using only the Pascal-provided control structures, the correct solution was given by only 20% of the subjects, while no subject wrote incorrect code for this problem if allowed to write a return from the middle of a loop.<ref name="roberts"/>{{sfn|Roberts|1995}}

In 1973, [[S. Rao Kosaraju]] proved that it is possible to avoid adding additional variables in structured programming, as long as arbitrary-depth, multi-level breaks from loops are allowed.{{sfn|Kozen|Tseng|2008}}{{refn|{{harvnb|Kosaraju|1973}},{{sfn|Kosaraju|1974}} cited by {{harvnb|Knuth|1974}}.}} Furthermore, Kosaraju proved that a strict hierarchy of programs exists, nowadays called the ''Kosaraju hierarchy'', in that for every integer ''n'', there exists a program containing a multi-level break of depth ''n'' that cannot be rewritten as program with multi-level breaks of depth less than ''n'' (without introducing additional variables).{{sfn|Kozen|Tseng|2008}} Kosaraju cites the multi-level break construct to the [[BLISS]] programming language. The multi-level breaks, in the form a <code>leave ''label''</code> keyword were actually introduced in the BLISS-11 version of that language; the original BLISS only had single-level breaks. The BLISS family of languages didn't provide an unrestricted goto. The [[Java (programming language)|Java programming language]] would later follow this approach as well.{{sfn|Brender|2002|pp=960–965}}

In 1973, [[S. Rao Kosaraju]] proved that it's possible to avoid adding additional variables in structured programming, as long as arbitrary-depth, multi-level breaks from loops are allowed.<ref name="kozen"/><ref>KOSARAJU, S. RAO. "Analysis of structured programs," Proc. Fifth Annual ACM Syrup.

Theory of Computing, (May 1973), 240-252; also in J. Computer and System Sciences, 9,

3 (December 1974), {{doi| 10.1016/S0022-0000(74)80043-7}} cited by {{cite journal

| author = [[Donald Knuth]]

| title = Structured Programming with go to Statements

| journal = Computing Surveys

| volume = 6

| issue = 4

| year = 1974

| url =

| pages = 261–301

| doi = 10.1145/356635.356640

| citeseerx = 10.1.1.103.6084

}}</ref> Furthermore, Kosaraju proved that a strict hierarchy of programs exists, nowadays called the ''Kosaraju hierarchy'', in that for every integer ''n'', there exists a program containing a multi-level break of depth ''n'' that cannot be rewritten as program with multi-level breaks of depth less than ''n'' (without introducing additional variables).<ref name="kozen"/> Kosaraju cites the multi-level break construct to the [[BLISS]] programming language. The multi-level breaks, in the form a <code>leave ''label''</code> keyword were actually introduced in the BLISS-11 version of that language; the original BLISS only had single-level breaks. The BLISS family of languages didn't provide an unrestricted goto. The [[Java (programming language)|Java programming language]] would later follow this approach as well.<ref>{{cite journal | doi = 10.1002/spe.470 | title=The BLISS programming language: a history | journal=Software: Practice and Experience | date=2002 | volume=32 | issue=10 | pages=955–981 | first=Ronald F. | last=Brender | url = https://www.cs.tufts.edu/~nr/cs257/archive/ronald-brender/bliss.pdf}}</ref>{{rp|960–965}}

A simpler result from Kosaraju's paper is that a program is reducible to a structured program (without adding variables) if and only if it does not contain a loop with two distinct exits. Reducibility was defined by Kosaraju, loosely speaking, as computing the same function and using the same "primitive actions" and predicates as the original program, but possibly using different control flow structures. (This is a narrower notion of reducibility than what Böhm–Jacopini used.) Inspired by this result, in section VI of his highly-cited paper that introduced the notion of [[cyclomatic complexity]], Thomas J. McCabe described an analogue of [[Kuratowski's theorem]] for the [[control -flow graph]]s (CFG) of non-structured programs, which is to say, the minimal [[Induced subgraph|subgraphs]] that make the CFG of a program non-structured. These subgraphs have a very good description in natural language. They are:

# branching out of a loop (other than from the loop cycle test)

# branching into a loop

# branching into a decision (i.e. into an if "branch")

# branching out of a decision

McCabe actually found that these four graphs are not independent when appearing as subgraphs, meaning that a necessary and sufficient condition for a program to be non-structured is for its CFG to have as subgraph one of any subset of three of these four graphs. He also found that if a non-structured program contains one of these four sub-graphs, it must contain another distinct one from the set of four. This latter result helps explain how the control flow of non-structured program becomes entangled in what is popularly called "[[spaghetti code]]". McCabe also devised a numerical measure that, given an arbitrary program, quantifies how far off it is from the ideal of being a structured program; McCabe called his measure [[essential complexity (numerical measure of "structuredness")|essential complexity]].<ref name="McCabe">{{refn|The original paper is {{cite journal harvnb|author=Thomas J. McCabe |date=December 1976}}. |journal=IEEEFor Transactionsa onsecondary Softwareexposition Engineeringsee {{harvnb|issue=4 Jorgensen|pages=315–3182002}}.}} |title=AMcCabe's Complexitycharacterization Measure|url=https://books.google.com/books?id=vtNWAAAAMAAJ&pg=PA3of |doi=10.1109/tse.1976.233837}}the For[[forbidden agraph]]s secondaryfor expositionstructured seeprogramming {{citecan book|author=Paulbe C.considered Jorgensen|title=Softwareincomplete, at least Testing:if Athe CraftsmanDijkstra's Approach,D Secondstructures Edition|url=https://booksare considered the building blocks.google.com/books?id=Yph_AwAAQBAJ&pg=PA150{{sfn|year=2002Williams|publisher=CRC Press1983|isbnpp=978-0-8493-0809-3274–275}}{{clarify|pagesdate=150–153|edition=2ndJuly 2014}}</ref>

Up to 1990 there were quite a few proposed methods for eliminating gotos from existing programs, while preserving most of their structure. The various approaches to this problem also proposed several notions of equivalence, which are stricter than simply Turing equivalence, in order to avoid output like the folk theorem discussed above. The strictness of the chosen notion of equivalence dictates the minimal set of control flow structures needed. The 1988 [[JACM]] paper by Lyle Ramshaw surveys the field up to that point, as well proposing its own method.{{sfn|Ramshaw|1988}} Ramshaw's algorithm was used for example in some Java [[decompiler]]s because the [[Java virtual machine]] code has branch instructions with targets expressed as offsets, but the high-level Java language only has multi-level <code>break</code> and <code>continue</code> statements.{{sfn|Nolan|2004}}{{sfn|Proebsting|Watterson|1997}}{{sfn|Maruyama|Ogawa|Matsuoka|1999}} Ammarguellat (1992) proposed a transformation method that goes back to enforcing single-exit.{{sfn|Ammarguellat|1992}}

McCabe's characterization of the [[forbidden graph]]s for structured programming can be considered incomplete, at least if the Dijkstra's D structures are considered the building blocks.<ref>{{cite journal | doi = 10.1093/comjnl/26.3.270 | title=Flowchart Schemata and the Problem of Nomenclature | journal=The Computer Journal | date=1983 | volume=26 | issue=3 | pages=270–276 | first=M. H. | last=Williams| doi-access=free }}</ref>{{rp|274–275}}{{clarify|date=July 2014}}

==Application to COBOL==

Up to 1990 there were quite a few proposed methods for eliminating gotos from existing programs, while preserving most of their structure. The various approaches to this problem also proposed several notions of equivalence, which are stricter than simply Turing equivalence, in order to avoid output like the folk theorem discussed above. The strictness of the chosen notion of equivalence dictates the minimal set of control flow structures needed. The 1988 [[JACM]] paper by Lyle Ramshaw surveys the field up to that point, as well proposing its own method.<ref>{{Cite journal | doi = 10.1145/48014.48021| title = Eliminating go to's while preserving program structure| journal = Journal of the ACM| volume = 35| issue = 4| pages = 893–920| year = 1988| last1 = Ramshaw | first1 = L. }}</ref> Ramshaw's algorithm was used for example in some Java [[decompiler]]s because the [[Java virtual machine]] code has branch instructions with targets expressed as offsets, but the high-level Java language only has multi-level <code>break</code> and <code>continue</code> statements.<ref name="Nolan2004">{{cite book|author=Godfrey Nolan|title=Decompiling Java|year=2004|publisher=Apress|isbn=978-1-4302-0739-9|page=142}}</ref><ref>https://www.usenix.org/legacy/publications/library/proceedings/coots97/full_papers/proebsting2/proebsting2.pdf</ref><ref>http://www.openjit.org/publications/pro1999-06/decompiler-pro-199906.pdf</ref> Ammarguellat (1992) proposed a transformation method that goes back to enforcing single-exit.<ref name="amma92">{{cite journal | doi = 10.1109/32.126773 | title=A control-flow normalization algorithm and its complexity | journal=IEEE Transactions on Software Engineering | date=1992 | volume=18 | issue=3 | pages=237–251 | first=Z. | last=Ammarguellat}}</ref>

==Application to Cobol==

{{More citations needed section|date=August 2013}}

In the 1980s [[IBM]] researcher [[Harlan Mills]] oversaw the development of the [[COBOL Structuring Facility]], which applied a structuring algorithm to [[COBOL]] code. Mills's transformation involved the following steps for each procedure.

Line 101 ⟶ 81:

#Construct a sequence that initializes L to 1 and executes the loop.

Note that thisThis construction can be improved by converting some cases of the selection statement into subprocedures.

==See also==

*[[Structured programming]]

*[[Turing completeness]]

==Notes==

{{Reflist|2}}

==References==

* {{cite journal |last=Ammarguellat |first=Z. |title=A control-flow normalization algorithm and its complexity |journal=IEEE Transactions on Software Engineering |volume=18 |issue=3 |pages=237–251 |year=1992 |doi=10.1109/32.126773 }}

{{Reflist}}

* {{cite conference |last1=Ashcroft |first1=Edward |last2=Manna |first2=Zohar |author2-link=Zohar Manna|title=The translation of go to programs to 'while' programs |book-title=Proceedings of IFIP Congress |year=1971}}. Republished in {{harvnb|Yourdon|1979|pp=51–61}}

* {{cite journal |last=Bennett |first=C. H. |author-link=Charles H. Bennett (physicist)|title=Logical Reversibility of Computation |journal=IBM Journal of Research and Development |volume=17 |issue=6 |pages=525–532 |date=November 1973 |doi=10.1147/rd.176.0525 }}

* {{cite journal |last1=Böhm |first1=Corrado |author-link1= Corrado Böhm |last2= Jacopini |first2= Giuseppe |author-link2= :it:Giuseppe Jacopini |date=May 1966 |title=Flow Diagrams, Turing Machines and Languages with Only Two Formation Rules |journal=[[Communications of the ACM]] |volume=9 |issue=5 |pages=366–371 |doi=10.1145/355592.365646 |citeseerx=10.1.1.119.9119 |s2cid=10236439}}. Republished in {{harvnb|Yourdon|1979|pp=13–25}}

* {{cite journal |last=Brender |first=Ronald F. |title=The BLISS programming language: a history |journal=Software: Practice and Experience |volume=32 |issue=10 |pages=955–981 |year=2002 |doi=10.1002/spe.470 |s2cid=45466625|url = https://www.cs.tufts.edu/~nr/cs257/archive/ronald-brender/bliss.pdf}}

* {{cite report|last1= Burks|first1= Arthur W.|last2= Goldstine|first2= Herman|last3= von Neumann|first3= John|author1-link= Arthur W. Burks|author2-link= Herman Goldstine|author3-link = John von Neumann|title= Preliminary discussion of the Logical Design of an Electronic Computing Instrument|publisher= Institute for Advanced Study|___location= Princeton, NJ|year= 1947}}

* {{cite journal |last=Cooper |first=David C. |title=Böhm and Jacopini's reduction of flow charts |journal=Communications of the ACM |volume=10 |issue=8 |page=463 |date=August 1967 |doi=10.1145/363534.363539 |doi-access=free }}

* {{cite journal|last=Dijkstra|first=Edsger|author-link=Edsger W. Dijkstra|year=1968|title=Go To Statement Considered Harmful|journal=Communications of the ACM|volume=11|issue=3|pages=147–148|doi=10.1145/362929.362947|s2cid=17469809 |doi-access=free}}. Republished in {{harvnb|Yourdon|1979|pp=29–33}}

* {{cite journal |last=Harel |first=David |author-link=David Harel|title=On Folk Theorems |url=http://www.wisdom.weizmann.ac.il/~dharel/SCANNED.PAPERS/OnFolkTheorems.pdf|journal=Communications of the ACM |volume=23 |issue=7 |pages=379–389 |year=1980 |doi=10.1145/358886.358892 |s2cid=16300625 }}

* {{cite book |last=Jorgensen |first=Paul C. |title=Software Testing: A Craftsman's Approach |edition=2nd |publisher=CRC Press |year=2002 |pages=150–153 |isbn=978-0-8493-0809-3 }}

* {{cite journal |last=Knuth |first=Donald |author-link=Donald Knuth|title=Structured Programming with go to Statements |journal=Computing Surveys |volume=6 |issue=4 |pages=261–301 |year=1974 |doi=10.1145/356635.356640 |s2cid=207630080 |citeseerx=10.1.1.103.6084 }}. Republished in {{harvnb|Yourdon|1979|pp=259–321}}

* {{cite conference |last=Kosaraju |first=S. Rao |author-link=S. Rao Kosaraju|title=Analysis of structured programs |book-title=Proceedings of the Fifth Annual ACM Symposium on Theory of Computing |date=May 1973 |pages=240–252 |publisher=ACM}},{{cite journal |last=Kosaraju |first=S. Rao |author-mask=0|title=Analysis of Structured Programs |journal=Journal of Computer and System Sciences |volume=9 |issue=3 |pages=232–255 |year=1974 |orig-year=1973|doi=10.1016/S0022-0000(74)80043-7 }}

* {{cite conference |last1=Kozen |first1=Dexter|author1-link=Dexter Kozen|last2=Tseng |first2=Wei-Lung Dustin |title=Mathematics of Program Construction – The Böhm–Jacopini Theorem is False, Propositionally |url= https://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf|book-title=MPC 2008 |series=Lecture Notes in Computer Science |volume=5133 |pages=177–192 |year=2008 |doi=10.1007/978-3-540-70594-9_11 |isbn=978-3-540-70593-2 |citeseerx=10.1.1.218.9241 }}

* {{cite book |last1=Louden |first1=Kenneth C. |last2=Lambert |first2=Kenneth A. |title=Programming Languages: Principles and Practices |edition=3rd |publisher=Cengage Learning |year=2011 |isbn=978-1-111-52941-3 }}

* {{cite web |last1=Maruyama |first1=Fuyuhiko |last2=Ogawa |first2=Hirotaka |last3=Matsuoka |first3=Satoshi |date=1999|url=http://www.openjit.org/publications/pro1999-06/decompiler-pro-199906.pdf |title=An Effective Decompilation Algorithm for Java Bytecodes |website=www.openjit.org |language=ja |access-date=2025-07-12}}

*{{cite journal|last=McCabe |first=Thomas J.|date=December 1976 |journal=IEEE Transactions on Software Engineering |issue=4 |pages=315–318 |title=A Complexity Measure|url=https://books.google.com/books?id=vtNWAAAAMAAJ&pg=PA3 |doi=10.1109/tse.1976.233837 |volume=SE-2|s2cid=9116234 }}

* {{cite book |last=Mills |first=Bruce Ian |title=Theoretical Introduction to Programming |publisher=Springer |year=2005 |page=279 |isbn=978-1-84628-263-8 }}

* {{cite book |last=Nolan |first=Godfrey |title=Decompiling Java |publisher=Apress |year=2004 |page=142 |isbn=978-1-4302-0739-9 }}

* {{cite web |last1=Proebsting|first1=Todd A.|last2=Watterson|first2=Scott A.|date=1997|title=Krakatoa: Decompilation in Java |url=https://www.usenix.org/legacy/publications/library/proceedings/coots97/full_papers/proebsting2/proebsting2.pdf|website=usenix.org |access-date=2025-07-12}}

* {{cite journal |last=Ramshaw |first=L. |title=Eliminating go to's while preserving program structure |journal=Journal of the ACM |volume=35 |issue=4 |pages=893–920 |year=1988 |doi=10.1145/48014.48021 |doi-access = free |s2cid=31001665 }}

* {{cite journal |last=Roberts |first=E. |title=Loop Exits and Structured Programming: Reopening the Debate |journal=ACM SIGCSE Bulletin |volume=27 |issue=1 |pages=268–272 |year=1995 |url=http://cs.stanford.edu/people/eroberts/papers/SIGCSE-1995/LoopExits.pdf|archive-url=https://web.archive.org/web/20140725130816/http://cs.stanford.edu/people/eroberts/papers/SIGCSE-1995/LoopExits.pdf|url-status=live|archive-date=2014-07-25}}

* {{cite web|author=University at Buffalo|title=CSE 111, Fall 2004, BOEHM-JACOPINI THEOREM |url=http://www.cse.buffalo.edu/faculty/sael/cse111/Fall2004/lectures/boehm-jacopini.html|archive-url=https://web.archive.org/web/20041122222935/http://www.cse.buffalo.edu/~rapaport/111F04/greatidea3.html |url-status=dead |archive-date=2004-11-22|publisher=University at Buffalo |date=2004-11-22 |access-date=2025-07-12}}

* {{cite book |last=Watt |first=David Anthony |author1-link=David Watt (computer scientist)|last2=Findlay |first2=William |title=Programming Language Design Concepts |publisher=John Wiley & Sons |year=2004 |isbn=978-0-470-85320-7 }}

* {{cite journal |last=Williams |first=M. H. |title=Flowchart Schemata and the Problem of Nomenclature |journal=The Computer Journal |volume=26 |issue=3 |pages=270–276 |year=1983 |doi=10.1093/comjnl/26.3.270 }}

* {{cite journal |last1=Yokoyama |first1=Tetsuo |last2=Axelsen |first2=Holger Bock |last3=Glück |first3=Robert |title=Fundamentals of reversible flowchart languages |journal=Theoretical Computer Science |date=January 2016 |volume=611 |pages=87–115 |doi=10.1016/j.tcs.2015.07.046|doi-access=free}}

* {{cite book |editor-last=Yourdon |editor-first=E. N. |editor-link=Edward Yourdon |title=Classics in Software Engineering |publisher=Yourdon Press |___location=New York, NY|year=1979 |pages=xi, 424 |isbn=978-0-917072-14-7 |lccn=79-63449}}

==Further reading==

Material not yet covered above:

* {{cite journal | doi = 10.1145/322169.322180 | title=Space-Time Trade-Offs in Structured Programming: An Improved Combinatorial Embedding Theorem | journal=Journal of the ACM | date=1980 | volume=27 | issue=1 | pages=123–127 | first=Richard A. | last=DeMillo}}

* {{cite book | doi = 10.1007/3-540-57785-8_128 | title=One binary horn clause is enough | volume=775 | date=1994 | pages=19–32 | first=Philippe | last=Devienne| series=Lecture Notes in Computer Science | isbn=978-3-540-57785-0 | citeseerx=10.1.1.14.537 }}

* {{cite journal

==External links==

|last1=DeMillo

* http://www.cs.uwlax.edu/~riley/CS421/lect8_boehm.ppt a slightly more detailed explanation of the construction used in the folk theorem's proof, with a concrete example of transformed program

|first1=Richard A.

|author1-link=Richard DeMillo

|last2=Eisenstat

|first2=Stanley C.

|last3=Lipton

|first3=Richard J.

|title=Space‑Time Trade‑Offs in Structured Programming: An Improved Combinatorial Embedding Theorem

|journal=[[Journal of the ACM]]

|volume=27

|issue=1

|pages=123–127

|date=January 1980

|doi=10.1145/322169.322180

|s2cid=15669719

| doi-access=free

}}

* {{cite conference

|last1=Devienne |first1=Philippe

|last2=Lebègue |first2=Patrick

|last3=Routier |first3=Jean-Christophe

|last4=Würtz |first4=Jörg

|title=One binary Horn clause is enough

|book-title=Proceedings of the 11th Symposium on Theoretical Aspects of Computer Science (STACS ’94)

|series=Lecture Notes in Computer Science

|volume=775

|pages=21–32

|date=February 1994

|doi=10.1007/3-540-57785-8_128

|isbn=978-3-540-57785-0

|citeseerx=10.1.1.14.537

}}

[[Category:Programming language theory]]

[[Category:Models of computation]]

[[Category:Theorems in computational complexity theory]]