Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleMechanical inference of invariants for FOR-loops
Author(s) Stefan Kauer, Jürgen F.H. Winkler
TypeArticle in Journal
AbstractIn the mechanical verification of programs containing loops it is often necessary to provide loop invariants additionally to the specification in the form of pre and postconditions. In this paper we present a method for the mechanical inference of invariants for a practically relevant class of FOR-loops. The invariant is derived from the specification (pre, post) and the final bound of the loop only. The method is based on the technique “replacing a constant in post by a variable”, which has traditionally been used manually for the development of WHILE-loops. Our method is a complete mechanization of this heuristic for the verification of existing annotated FOR-loops. The range of applicability of the method is further extended by a technique called “bound transformation” and by taking common invariant conjuncts of pre and post into account. As a result, the method is applicable to the majority of FOR-loops occurring in practice. The incorporation of this method into an automatic program verifier would make the task of the SW engineer easier, because he has only to provide a pre–post-specification for a FOR-loop.
KeywordsMechanical verification, Mechanical inference of loop invariants, FOR-loop, RCPV
URL http://www.sciencedirect.com/science/article/pii/S0747717109000522
JournalJournal of Symbolic Computation
Pages1101 - 1113
NoteSpecial Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops
Translation No
Refereed No