Physical Sciences and Mathematics Commons^™

A Systematic Derivation Of Loop Specifications Using Patterns, Aditi Barua, Yoonsik Cheon

Departmental Technical Reports (CS)

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 …