A Proof Rule for Functions

Abstract

This report gives a rule of inference which permits a natural form of reasoning about programs containing functions. The rule was obtained by modifying the function rule of Clint and Hoare to include a premise which requires consistency of preconditions and postconditions, and a premise which requires deterministic computation. Examples of use of the rule and versions tailored to the Pascal and Euclid languages are also given.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1977
Accession Number
ADA046298

Entities

People

  • David R. Musser

Organizations

  • University of Southern California

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Computations
  • Computer Programming
  • Consistency
  • Information Processing
  • Information Science
  • Language
  • New Jersey
  • Notation
  • Programming Languages
  • Reasoning
  • Side Effects
  • Verification

Readers

  • Artificial Intelligence
  • Computer Science.

Technology Areas

  • AI & ML
  • AI & ML - Machine Learning Algorithms
  • AI & ML - Machine Translation