Zhiping Shi1, Yupeng Zhang1, Yong Guan1, Liming Li1, Jie Zhang2
1Beijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing, 100048, China
2College of Information Science and Technology, Beijing University of Chemical Technology, Beijing, 100029, China
Tóm tắt
Traditionally, Discrete Fourier Transform (DFT) is performed with numerical or symbolic computation, which cannot guarantee 100% accurate analysis which may be necessary for safety-critical applications. Machine theorem proving is one of the formal methods that perform accurate analysis with completeness to some extent. This paper proposes the formalization of DFT in a higher-order logic theorem prover named HOL. We propose the formal definition of DFT and verify the fundamental properties of DFT. Two case studies are presented to illustrate usefulness and correctness of the formalized DFT, including formal verifications of Fast Fourier Transform (FFT) and cosine frequency shift.
Từ khóa
Tài liệu tham khảo
2002
1988
10.1007/3-540-44755-5_4
10.1007/3-540-60156-2_3
1989, Mechanizing programming logics in higher-order logic, 387
