A Systematic Derivation of Loop Specifications Using Patterns

Any non-trivial program contains loop control structures such as while, for and do statements. A formal correctness proof of code containing loop control structures is typically performed using an induction-based technique, and oftentimes the most challenging step of an inductive proof is formulating a correct induction hypothesis. An incorrectly-formulated induction hypothesis will surely lead to a failure of the proof. In this paper we propose a systematic approach for formulating and driving specifications of loop control structures for formal analysis and verification of programs. We explain our approach using while loops and a functional program verification technique in which a program is viewed as a mathematical function from one program state to another. The most common use of loop control structures is to iterate over a certain sequence of values and manipulate it, one value at a time. Many loops exhibit certain common flavors or patterns, and similarly-structured loops have similarly-structured specifications. Our approach is to categorize and document the common flavors or usage patterns of loop control structures as reusable specification patterns. One key idea of our pattern specification is to promote manipulation of individual values to the whole sequence iterated over by a loop. Our patterns are compositional and can be organized into a pattern hierarchy. A catalog of loop specification patterns can be a good resource for systematically formulating and deriving specifications of loops. Indeed, our case study indicates that our patterns are applicable to a wide range of programs from systems programming to scientific and business applications