Proving with the Help of Property-Based Testing
Exposing the QuickCheck Interface in Agda for Agda2Hs
M.L.C. Sloof (TU Delft - Electrical Engineering, Mathematics and Computer Science)
J.G.H. Cockx – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
N. Burke – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
A. Panichella – Graduation committee member (TU Delft - Electrical Engineering, Mathematics and Computer Science)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Testing constitutes an important part of software development for many engineers. Agda2Hs, a transpiler from Agda to Haskell, currently does not provide such testing functionality. Agda enables developers to express and formally verify properties directly within the source code, whereas Haskell benefits from an extensive ecosystem of tools and developers. By transpiling verified Agda code to Haskell, Agda2Hs offers the potential to combine the advantages of both languages. However, constructing formal proofs in Agda is challenging, as it requires the same creativity and insight needed for mathematical reasoning. Consequently, a proposition with a bug may be mistakenly seen as difficult to prove. Property-based testing can provide confidence in the correctness of a proposition before a proof is completed. This paper presents these testing functionalities in Agda2Hs by porting QuickCheck to Agda. Furthermore, correspondence proofs are introduced, which enable programmers to show formally that a test asserts the same property as a proposition.