Specified Agda is Testable Haskell
Translating Agda Postconditions to QuickCheck Property Tests in agda2hs
A.W. Kierska (TU Delft - Electrical Engineering, Mathematics and Computer Science)
N. Burke – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
J.G.H. Cockx – 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
Formally verified code written in dependently typed languages can be integrated into larger, non-verified code bases through source-to-source translation. The agda2hs compiler enables such integration by translating verified Agda code to readable Haskell, erasing proofs and type indices in the process. The properties that a program is verified against are encoded as such proofs and type indices, and are therefore also erased. Yet being able to check these properties is important: in the agda2hs workflow, verified code may depend on unverified Haskell libraries whose properties are assumed without proof and never tested.
In this paper, we present an extension to agda2hs that extracts postconditions and translates them into Haskell QuickCheck property tests. Since postconditions in Agda are encoded at the type level, they are not executable and cannot be translated to Haskell directly. We address this by deriving semi-decision procedures that check whether a proposition holds for given inputs. We cover postconditions expressed as separate lemmas, sigma types, and indexed datatypes. We implement lemma-to-test translation as a working agda2hs extension; it requires the user to write the decision procedure by hand. We present the automatic derivation of such procedures as an algorithm design with worked examples.