Proving Termination with Multiset Orderings.

Abstract

A common tool for proving the termination of programs is the well-founded set, a set ordered in such a way as to admit no infinite descending sequences. The basic approach is to find a termination function that maps the elements of the program into some well-founded set, such that the value of the termination function is continually reduced throughout the computation. All too often, the termination functions required are difficult to find and are of a complexity out of proportion to the program under consideration. However, by providing more sophisticated well-founded sets, the corresponding termination functions can be simplified.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1978
Accession Number
ADA058601

Entities

People

  • Nachum Dershowitz
  • Zohar Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Air Force
  • Applied Mathematics
  • Arithmetic
  • Artificial Intelligence
  • Classification
  • Computations
  • Computer Science
  • Computers
  • Contracts
  • Governments
  • Iterations
  • Production
  • Security
  • Sequences
  • Standards
  • United States
  • Universities

Readers

  • Adaptive Control and Estimation with Uncertainty in Dynamic Systems.
  • Computational Linguistics
  • Microwave Engineering.