Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
A language-independent proof system for full program equivalence
Ciobâcă S., Lucanu D., Rusu V., Roşu G. Formal Aspects of Computing28 (3):469-497,2016.Type:Article
Date Reviewed: Jun 21 2016

The authors consider proving two programs “fully equivalent” (that is, either both do not terminate or both terminate with the same value). Both compute the Collatz sequence starting with a natural number n, which replaces in each iteration n > 1 by 3n+1 if n is odd, and by n/2 if n is even. It is not known whether this sequence is finite for all n.

Conventional program equivalence techniques split this problem into a case where the sequence terminates or a case where it does not. In this situation, this approach cannot work since there is no termination proof. The authors’ technique is to match formulas for selected configurations of the programs and build a logical relation between them, as a bisimulation is built between states of transition systems.

Logical relations were developed in the work of Jean-Yves Girard, Gordon Plotkin, and John Reynolds on the lambda calculus around 1973. The Collatz sequence programs give a nice example of the logical relation technique within standard Hoare logic. Only a few earlier examples are known; they occur in the study of fairness, for terminating [1,2] and for nonterminating [3] programs. The paper will be of interest to the program semantics and verification community.

Reviewer:  K. Lodaya Review #: CR144517 (1609-0671)
1) Apt, K. R.; Olderog, E.-R. Proof rules and transformations dealing with fairness. Science of Computer Programming 3, 1(1983), 65–100.
2) Grumberg, O.; Francez, N.; Makowsky, J. A.; de Roever, W. P. A proof rule for fair termination of guarded commands. Information and Control 66, 1/2(1985), 83–102.
3) Ramanujam, R.; Lodaya, K. Proving fairness of schedulers. In: Logics of programs (LNCS 193). 284-301, Springer, 1985.
Bookmark and Share
 
Correctness Proofs (D.2.4 ... )
 
 
Assertions (F.3.1 ... )
 
 
Semantics (D.3.1 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Correctness Proofs": Date
Using symbolic execution for verification of Ada tasking programs
Dillon L. (ed) ACM Transactions on Programming Languages and Systems 22(6): 643-669, 2000. Type: Article
Jul 1 1991
Reasoning about programs (videotape)
Dijkstra E. (ed), University Video Communications, Stanford, CA, 1990. Type: Book
Dec 1 1992
Error-free software
Baber R., John Wiley & Sons, Inc., New York, NY, 1991. Type: Book (9780471930167)
May 1 1994
more...

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