A simple program whose derivation and proof is also
A simple program whose derivation and proof is also
复制标题
DOI：
10.1109/icfem.1997.630419
复制
发表时间：
1997-11
期刊：
影响因子：
--
通讯作者：
Jinyun Xue;Ruth Davis
中科院分区：
文献类型：
--
作者：
Jinyun Xue;Ruth Davis
本文给出了Knuth(D.Knuth，1990)将二进制小数转换为十进制小数的程序的一个示例推导和证明。使用的主要技术是划分和递归方法，即对问题进行划分，推导出用递归表示的算法，最后以直接的方式将算法转换为程序。这个例子的实践给了我们更多的信心，即划分和递归是推导和证明通用算法和程序的一种可行的方法。
The article presents a sample derivation and proof for Knuth's program (D. Knuth, 1990) that translates a binary fraction to a decimal fraction. The main technique used 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.