Programming by Expression Refinement: a Sequence of Examples
Joseph M. Morris · 1990
We describe by a sequence of examples a method, which we call expression refinement, for deriving programs from specifications. The method consists of making specifications using a rich notation for expressions; the expressions are then subjected to value-preserving transformations in which the rich notations are replaced by more primitive ones that are part of the implementation language. This leads to a style of programming that makes much use of recursive functions rather than loops and invariant relations. The technique is part of a larger effort to develop a fully formal and practical calculus of programming. Initial experience suggests that expression refinement is potentially a more attractive approach for formal programming than one relying principally on traditional approaches based on refinement of statements.