Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
On the mechanical derivation of loop invariants
Chadha R., Plaisted D. Journal of Symbolic Computation15 (5-6):705-744,1993.Type:Article
Date Reviewed: Mar 1 1995

A method for automatically deriving loop invariants for loops in a flowchart program for the purpose of proving the partial correctness of the program is described. In fact, the authors present a method for deriving logical consequences of first-order formulas using resolution and a new extended unskolemization algorithm. They give some properties of this method, and explain its relation to program verification, namely how to apply it for generating loop invariants. The method can be applied when an axiomatization of the model of the data structures and primitive operations of the program language exists.

According to Cook’s completeness result [1], no complete method can exist for automatically deriving loop invariants for all possible loops. Most of the attempts to mechanically generate loop invariants have been heuristic, and have not been complete in any sense. The method described in the paper is complete in the sense that if a loop invariant exists for a loop in a given first-order language relative to a given finite set of first-order axioms, then the method produces a loop invariant for that loop. Unfortunately, not all interesting theories can be expressed by a finite set of first-order axioms.

The method has not been implemented, but it has been manually applied to many examples, and loop invariants were successfully derived for the programs used. The method works particularly well on programs without nested loops. Finally, the method seems to be a useful tool for the verification of very large programs.

Reviewer:  G. Ciobanu Review #: CR117876
1) Cook, S. A. Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 1 (1978), 70–90.
Bookmark and Share
 
Invariants (F.3.1 ... )
 
 
Correctness Proofs (D.2.4 ... )
 
 
Mechanical Verification (F.3.1 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Invariants": Date
Sometime=always+recursionalways on the equivalence of the intermittent and invariant assertions methods for proving properties of programs
Cousot P., Cousot R. Acta Informatica 24(1): 1-31, 1987. Type: Article
Nov 1 1988
Strongest invariant functions: their use in the systematic analysis of while statements
Mili A. (ed), Desharnais J., Gagné J. Acta Informatica 22(1): 47-66, 1985. Type: Article
Aug 1 1987
Variant construction from theoretical foundation to applications
Zheng J., Springer International Publishing, New York, NY, 2019.  409, Type: Book
Nov 11 2019

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy