Report Number: CS-TR-75-522
Institution: Stanford University, Department of Computer Science
Title: Automatic program verification IV: proof of termination
within a weak logic of programs.
Author: Luckham, David C.
Author: Suzuki, Norihisa
Date: October 1975
Abstract: A weak logic of programs is a formal system in which
statements that mean "the program halts" cannot be expressed.
In order to prove termination, we would usually have to use a
stronger logical system. In this paper we show how we can
prove termination of both iterative and recursive programs
within a weak logic by adding pieces of code and placing
restrictions on loop invariants and entry conditions. Thus,
most of the existing verifiers which are based on a weak
logic of programs can be used to prove termination of
programs without any modification. We give examples of proofs
of termination and of accurate bounds on computation time
that were obtained using the Stanford Pascal program