The Community for Technology Leaders
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
89 ms
(Ver 3.3 (11022016))