The Validity Problem of the 91-Function,

Abstract

Several methods for proving the weak and strong validity of algorithms are presented. For proving the weak validity (i.e., correctness) the authors use satisfiability methods, while for proving the strong validity (i.e., termination and correctness) the authors use unsatisfiability methods. Two types of algorithms are discussed: recursively defined functions and programs. Among the methods included are known methods due to Floyd, Manna, and McCarthy. All the methods are introduced quite informally by means of an example (the 91-function). (Modified author abstract)

Document Details

Document Type
Technical Report
Publication Date
Aug 19, 1968
Accession Number
AD0785164

Entities

People

  • Amir Pnueli
  • Zohar Manna

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Applied Computer Science
  • Artificial Intelligence

Fields of Study

  • Medicine

Readers

  • Finite Element Method (FEM) for solving Partial Differential Equations (PDEs)
  • Mathematical Modeling and Probability Theory.