Mechanically verifying real-valued algorithms in acl2
Ruben A. Gamboa, Robert S. Boyer · 1999
ACL2 is a theorem prover over a total, first-order, mostly quantifier-free logic, supporting defined and constrained functions, equality and congruence rewriting, induction, and other reasoning techniques. Based on the Boyer-Moore theorem prover, ACL2 manages to retain much of the flavor of its predecessor, while providing a large number of enhancements, one of which is the direct support of rational and complex-rational numbers. It was originally hoped that having a rich number system, specifically including the complex plane, would enable ACL2 to verify algorithms such as the Fast Fourier Transform (FFT). Using Misra's powerlist notation, we have shown how ACL2 can be used to verify complex algorithms, such as Batcher sorting, parallel prefix sum, and carry-lookahead adders. However, while the powerlist notation permits a simple proof of the correctness of the FFT, this proof is technically out of ACL2's reach, because by explicitly excluding the irrationals from its number system, AC...