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

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 verifier.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1975
Accession Number
ADA019569

Entities

People

  • David C. Luckham
  • Norihisa Suzuki

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Artificial Intelligence
  • Automatic
  • Computational Science
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Instructions
  • Language
  • Mathematical Analysis
  • Numbers
  • Programming Languages
  • Square Roots
  • Universities

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Computer Science.