Is "Sometime" Sometimes Better than "Always"? (Intermittent
Assertions in Proving Program Correctness)

This paper explores a technique for proving the
correctness and termination of programs simultaneously. 
 This approach, 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.  The intermittent-assertion method
is presented 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, it is shown that a proof of correctness
or termination by any of the conventional 
techniques can be rephrased directly as a proof using
intermittent assertions.  Finally, it is shown 
how the intermittent-assertion method can be applied
to prove the validity of program transformations 
and the correctness of continuously operating programs.

CACM February, 1978

Manna, Z.
Waldinger, R.

intermittent assertions, correctness of programs,
termination of programs, program verification, 
program transformation, continuously operating programs.

5.24

CA780209 JB March 28, 1978  2:04 PM

2021	4	3014
2222	4	3014
2227	4	3014
2315	4	3014
2326	4	3014
2470	4	3014
2732	4	3014
2865	4	3014
2896	4	3014
2943	4	3014
3014	4	3014
3014	4	3014
3068	4	3014
3077	4	3014
3143	4	3014
1834	5	3014
2981	5	3014
3014	5	3014
3014	5	3014
3014	5	3014
3157	5	3014
3014	6	3014