A Proof Rule for Functions
UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
Pagination or Media Count:
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.
- Computer Programming and Software