Title
Simple program whose derivation and proof is also
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.
Year
DOI
Venue
1997
null
Proceedings of the International Conference on Formal Engineering Methods, ICFEM
Keywords
DocType
Volume
null
Conference
null
Issue
ISSN
ISBN
null
null
0-8186-8002-4
Citations 
PageRank 
References 
5
0.59
1
Authors
2
Name
Order
Citations
PageRank
Jinyun Xue150.59
Ruth E. Davis250.59