Advances in Property-Based Testing for $\alpha$Prolog

TL;DR

This paper presents improvements to property-based testing in $eta$Prolog, enhancing its effectiveness for validating formal systems involving complex name-binding and substitution, with performance comparisons to existing tools.

Contribution

It introduces an alternative negation elimination algorithm for $eta$Prolog's property-based testing, significantly improving its effectiveness over previous methods.

Findings

Enhanced testing effectiveness demonstrated

Performance surpasses QuickCheck/Nitpick and PLT-Redex

Applicable to formal systems with complex name-binding

Abstract

$\alpha$Check is a light-weight property-based testing tool built on top of $\alpha$Prolog, a logic programming language based on nominal logic. $\alpha$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 $\alpha$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.