Test input generators are an important part of
property-based testing (PBT)
frameworks. Because PBT is intended to test
deep semantic and structural properties of a
program, the outputs produced by these
generators can be complex data structures,
constrained to satisfy properties the
developer believes is most relevant to testing
the function of interest. An important
feature expected of these generators is that
they be capable of producing all
acceptable elements that satisfy the
function's input type and generator-provided
constraints. However, it is not readily
apparent how we might validate whether a
particular generator's output satisfies this
coverage requirement. Typically,
developers must rely on manual inspection and
post-mortem analysis of test runs to determine
if the generator is providing sufficient
coverage; these approaches are error-prone and
difficult to scale as generators become more
complex. To address this important concern,
we present a new refinement type-based
verification procedure for validating the
coverage provided by input test generators,
based on a novel interpretation of types that
embeds ``must-style'' underapproximate
reasoning principles as a fundamental part of
the type system. The types associated with
expressions now capture the set of values
guaranteed to be produced by the
expression, rather than the typical
formulation that uses types to represent the
set of values an expression may
produce. Beyond formalizing the notion of
coverage
types in the context of a rich core
language with higher-order procedures and
inductive datatypes, we also present a
detailed evaluation study to justify the
utility of our ideas.
Recipient of a Distinguished Paper Award at PLDI 2023
