Finding Specifications of While Statements Using Patterns

A formal correctness proof of code containing loops such as while statements typically uses the technique of proof-by-induction, and often the most difficult part of carrying out an inductive proof is formulating a correct induction hypothesis, a specification for a loop statement. An incorrect induction hypothesis will surely lead to a proof failure. In this paper we propose a systematic way for identifying specifications of while statements. The key idea of our approach is to categorize and document common patterns of while statements along with their specifications. This is based on our observation that similarly-structured while statements frequently have similarly-structured specifications. Thus, a catalog of code and specification patterns can be used as a good reference for finding and formulating a specification of a while statement. We explain our approach using functional program verification in which a program is viewed as a mathematical function from one program state to another, and a correctness proof is done by comparing two functions, the implemented and the specified. However, we believe our approach is applicable to other verification techniques such as Hoare logic using pre- and post-conditions