A Method, Based on Plans, for Understanding How a Loop Implements a Computation

Abstract

The plan method analyzes the structure of a program. The plan which results from applying the method represents this structure by specifying how the parts of the program interact. This paper demonstrates the utility of the plan method by showing how a plan for a loop can be used to help prove the correctness of a loop. The plan does this by providing a convenient description of what the loop does. This paper also shows how a plan for a loop can be developed based on the code for the loop without the assistance of any commentary. This is possible primarily because most loops are built up in stereotyped ways according to a few fundamental plan types. An experiment is presented which supports the claim that a small number of plan types cover a large percentage of actual cases.