DocumentCode
3345329
Title
A simple program whose derivation and proof is also
Author
Xue, Jinyun ; Davis, Ruth
Author_Institution
Comput. Software Inst., Jiangxi Normal Univ., Nanchang, China
fYear
1997
fDate
12-14 Nov. 1997
Firstpage
132
Lastpage
139
Abstract
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.
Keywords
mathematics; mathematics computing; program verification; theorem proving; Knuth program; binary fraction; decimal fraction; general algorithms; partition-and-recur approach; programming theory; proof; simple program derivation; Calculus; Computer languages; Partitioning algorithms; Problem-solving; Writing;
fLanguage
English
Publisher
ieee
Conference_Titel
Formal Engineering Methods., 1997. Proceedings., First IEEE International Conference on
Conference_Location
Hiroshima, Japan
Print_ISBN
0-8186-8002-4
Type
conf
DOI
10.1109/ICFEM.1997.630419
Filename
630419
Link To Document