Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Sometime=always+recursionalways on the equivalence of the intermittent and invariant assertions methods for proving properties of programs
Cousot P., Cousot R. Acta Informatica24 (1):1-31,1987.Type:Article
Date Reviewed: Nov 1 1988

This paper compares two verification methods for inevitability properties of nondeterministic transition systems, the “always” method and the “sometime” method. These methods are abstractions of program-verification techniques due to Floyd and Burstall, respectively.

The main research contribution of this paper is a translation that transforms proofs in the rich “sometime” method into proofs in the simpler “always” method. While this general translation avowedly does not yield natural proofs of correctness, it is mathematically satisfying. Unavoidably, some of the examples and constructions seem rather complex and make for arduous reading. Nevertheless, the paper should be of interest to researchers in the formal aspects of program verification.

Reviewer:  M. Abadi Review #: CR111905
Bookmark and Share
 
Invariants (F.3.1 ... )
 
 
Alternation And Nondeterminism (F.1.2 ... )
 
 
Assertions (F.3.1 ... )
 
 
Program And Recursion Schemes (F.3.3 ... )
 
 
Formal Definitions And Theory (D.3.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Invariants": Date
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
On the mechanical derivation of loop invariants
Chadha R., Plaisted D. Journal of Symbolic Computation 15(5-6): 705-744, 1993. Type: Article
Mar 1 1995
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