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