Structured program theorem: Difference between revisions

Revision as of 08:44, 13 March 2024

Revision as of 19:59, 9 December 2024

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 bookjournal|url= http://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf |author=[[Dexter Kozen]] and Wei-Lung Dustin Tseng|title=Mathematics of Program Construction |chapter=- The Böhm–Jacopini Theorem is False, Propositionally |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 |access-date=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

#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)

Line 89:

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}}

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. | s2cid = 31001665| doi-access = free}}</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>{{Cite web | url=https://www.usenix.org/legacy/publications/library/proceedings/coots97/full_papers/proebsting2/proebsting2.pdf {{Bare| URLtitle=Krakatoa: Decompilation in Java PDF|date=March 2022website=www.usenix.org}}</ref><ref>{{Cite web | url=http://www.openjit.org/publications/pro1999-06/decompiler-pro-199906.pdf {{Bare| URLtitle=An Effective Decompilation Algorithm for Java Bytecodes PDF|date=March 2022website=www.openjit.org}}</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>