Accession Number:

ADA046298

Title:

A Proof Rule for Functions

Descriptive Note:

Research rept.

Corporate Author:

UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST

Personal Author(s):

Report Date:

1977-10-01

Pagination or Media Count:

10.0

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE