Report Number: CSL-TR-75-92
Institution: Stanford University, Computer Systems Laboratory
Title: The complexity of control structures and program validation
Author: Davison, Joseph W.
Date: May 1975
Abstract: A preliminary examination of the influence of control structures on the complexity of the proof of correctness of computer programs. A block structured proof technique is defined and studied. Two parameters affecting the complexity of the proof are defined; the number of exits from a block, and the cycle rank of a block, a measure of loop complexity. Proof complexity classes of flowcharts are defined, with maximum values for these parameters. The question investigated is: How does restricting the complexity affect the class of functions realizable, assuming a given set of primitive actions and predicates: It is found that loop complexity may be traded for exits, and that for a given number of exits there are functions requiring any specific loop complexity. Further, it is shown that blocks with two exits are considerably more powerful than those with only one. In fact, for a given maximal loop complexity, there are functions that cannot be realized with one-exit blocks, but can be realized with two-exit blocks, even if the loop complexity is restricted to essentially one internal loop per block. Looking at it the other way around, the addition of a second exit to a block allows construction of flowcharts with any specified loop complexity. This result appears to be extendable to blocks with more exits, but this has not been completed. The work is primarily of a graph theoretical nature, and may also be interpreted as an examination of sequential control structures from the point of view of feedback loop complexity.
http://i.stanford.edu/pub/cstr/reports/csl/tr/75/92/CSL-TR-75-92.pdf