A CALCULUS OF FUNCTIONS FOR PROGRAM DERIVATION

Abstract

This paper is about how to calculate programs. We introduce a notation for describing functions, outline a calculus for manipulating function descriptions, and prove two general theorems for implementing certain functions efficiently. Like useful calculi in other branches of mathematics, the calculus of functions consists of a body of knowledge expressed as basic algebraic identities, technical lemmas and more general theorems. We illustrate the calculational approach to program construction by posing and solving a simple problem about coding sequences.