Mutation testing effectiveness for checking QuickCheck tests derived from Agda type signatures

Abstract

agda2hs is a compiler that allows compilation of dependently typed Agda language into readable Haskell modules. This has a benefit that a formal proof of correctness can be carried out on Agda side, and then used in more realistic context in Haskell. However, sometimes it might be beneficial to compile yet unproven functions to Haskell, to be able to use traditional testing methods to quickly discard incorrect implementations. In this paper, I explore the usefulness of using mutation testing in validating such property tests. I present modifications made to the existing Haskell MuCheck library to accommodate this workflow: a QuickCheck test adapter, an annotation mechanism that links tests to the functions they cover, and a way to mark already proven functions so they are not mutated. I evaluate the tool on several test cases, both written by hand and generated from Agda, including sorting algorithms and lambda calculus with De Bruijn indices. I find that the share of mutants equivalent to the original code varies greatly between functions, which makes the ratio of killed mutants hard to interpret on its own. The current implementation does not prove very practical at this stage, and I propose some improvements that could make this a useful tool for this particular workflow.