Automatic Program Verification IV:Proof of Termination within a Weak Logic of Programs.

摘要

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 verifier. (Author)