A Proof Rule for Functions
David R. Musser · 1977
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.