Report Number: CS-TR-76-558
Institution: Stanford University, Department of Computer Science
Title: Is "sometime" sometimes better than "always"? Intermittent
assertions in proving program correctness
Author: Manna, Z ohar
Author: Waldinger, Richard J.
Date: March 1977
Abstract: This paper explores a technique for proving the correctness
and termination of programs simultaneously. This approach,
which we call the intermittent-assertion method, involves
documenting the program with assertions that must be true at
some time when control passes through the corresponding
point, but that need not be true every time. The method,
introduced by Burstall, promises to provide a valuable
complement to the more conventional methods.
We first introduce the intermittent-assertion method with a
number of examples of correctness and termination proofs.
Some of these proofs are markedly simpler than their
conventional counterparts. On the other hand, we show that a
proof of correctness or termination by any of the
conventional techniques can be rephrased directly as a proof
using intermittent assertions. Finally, we show how the
intermittent assertion method can be applied to prove the
validity of program transformations and the correctness of
continuously operating programs.
This is a revised and simplified version of a previous paper
with the same title (AIM-281, June 1976).