structured program theorem

The structured program theorem, also called the Böhm–Jacopini theorem, is a result in programming language theory. It states that a class of control-flow graphs (historically called flowcharts in this context) can compute any computable function if it combines subprograms in only three specific ways ( control structures). These are
#Executing one subprogram, and then another subprogram (sequence)
#Executing one of two subprograms according to the value of a boolean expression (selection)
#Repeatedly executing a subprogram as long as a boolean expression is true (iteration)

The structured chart subject to these constraints may however use additional variables in the form of bits (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 commands and exclusively uses subroutines, sequences, selection and iteration.

Origin and variants

The theorem is typically credited to a 1966 paper by Corrado Böhm and Giuseppe Jacopini. David Harel wrote in 1980 that the Böhm–Jacopini paper enjoyed "universal popularity", particularly with proponents of structured programming. Harel also noted that "due to its rather technical style he 1966 Böhm–Jacopini paperis apparently more often cited than read in detail" 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 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 von Neumann and Kleene.

Harel also writes that the more generic name was proposed by H.D. Mills as "The Structure Theorem" in the early 1970s.

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 while 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. Another, even older source that Harel traced the folk version of the theorem is Stephen Kleene's normal form theorem from 1936.

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. 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."

p := 1
while p > 0 do
if p = 1 then
perform step 1 from the flowchart
p := resulting successor step number of step 1 from the flowchart (0 if no successor)
end if
if p = 2 then
perform step 2 from the flowchart
p := resulting successor step number of step 2 from the flowchart (0 if no successor)
end if
...
if p = n then
perform step n from the flowchart
p := resulting successor step number of step n from the flowchart (0 if no successor)
end if
end while

Böhm and Jacopini's proof

The proof in Böhm and Jacopini's paper proceeds by induction on the structure of the flow chart. Because it employed 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.

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, " Go To Statement Considered Harmful," followed in 1968.

Some academics took a purist approach to the Böhm–Jacopini result and argued that even instructions like break and return 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 (designed in 1968–1969), which up to the mid-1990s was the preferred tool for teaching introductory programming classes in academia.Roberts, E. 995br>Loop Exits and Structured Programming: Reopening the Debate
" ACM SIGCSE Bulletin, (27)1: 268–272.

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. Among the first proposals for an automated transformation was a 1971 paper by Edward Ashcroft and Zohar Manna.

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. The latter issue is called the loop and a half problem in this context. 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.

In 1973, S. Rao Kosaraju

HOME


Content is Copyleft
Website design, code, and AI is Copyrighted (c) 2014-2017 by Stephen Payne


Consider donating to Wikimedia



As an Amazon Associate I earn from qualifying purchases