Formal Engineering Methods, International Conference on (1997)

Hiroshima, JAPAN

Nov. 12, 1997 to Nov. 14, 1997

ISBN: 0-8186-8002-4

pp: 132

Jinyun Xue , Santa Clara University Santa Clara, CA

Ruth Davis , Santa Clara University Santa Clara, CA

ABSTRACT

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.

INDEX TERMS

CITATION

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.

doi:10.1109/ICFEM.1997.630419

CITATIONS