Bridging the Gap in Software Verification - Agda Proofs to Haskell Test Case Generators
How can preconditions in Agda be translated to a QuickCheck generator in Haskell?
M.Z. Olszewski (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
Property-based testing is a popular testing paradigm, especially common in the functional programming language Haskell through the QuickCheck library. On the other hand, Agda is a dependently-typed language used as a proof assistant and for software verification. Because of the need for software verification, Agda2hs was created as a tool for translating code between these two, combining proven functionality with practical execution.
This work explores making QuickCheck-compatible generators based on properties encoded in Agda. This should allow automating early checking of Agda proofs for correctness, as well as enabling conversion of formal specifications to executable tests for Haskell projects. A procedure is presented that permits creating advanced generators and checkers, and it is later evaluated in terms of multifaceted performance metrics.