Formal Engineering Methods, International Conference on (1997)
Nov. 12, 1997 to Nov. 14, 1997
Jinyun Xue , Santa Clara University Santa Clara, CA
Ruth Davis , Santa Clara University Santa Clara, CA
This note presents a simple derivation and proof for Knuth's program that translates a binary fraction to a decimal fraction. The main technique used in this note is the partition-and-recur approach, that is, partitioning the problem, deriving an algorithm represented by recurrences, and finally transforming the algorithm to a program in a straightforward manner. Practice with this example has given us more confidence that partition-and-recur is a practicable approach for derivation and proof of general algorithms and programs.
J. Xue and R. Davis, "A Simple Program whose Derivation and proof is also," Formal Engineering Methods, International Conference on(ICFEM), Hiroshima, JAPAN, 1997, pp. 132.