Advances in Property-Based Testing for $\alpha$Prolog
Abstract
Check is a light-weight property-based testing tool built on top of Prolog, a logic programming language based on nominal logic. Prolog is particularly suited to the validation of the meta-theory of formal systems, for example correctness of compiler translations involving name-binding, alpha-equivalence and capture-avoiding substitution. In this paper we describe an alternative to the negation elimination algorithm underlying Check that substantially improves its effectiveness. To substantiate this claim we compare the checker performances w.r.t. two of its main competitors in the logical framework niche, namely the QuickCheck/Nitpick combination offered by Isabelle/HOL and the random testing facility in PLT-Redex.
Cite
@article{arxiv.1604.08345,
title = {Advances in Property-Based Testing for $\alpha$Prolog},
author = {James Cheney and Alberto Momigliano and Matteo Pessina},
journal= {arXiv preprint arXiv:1604.08345},
year = {2016}
}
Comments
To appear, Tests and Proofs 2016; includes appendix with details not in the conference version