Using the checker

The αCheck system is an extension of αProlog to support checking for counterexamples to simple specifications. For example, if you have specified a simple core language and type system using αProlog rules, then you can

This system is described in greater detail in several papers, listed at the end of this page. Several of the examples mentioned in the papers are also stored in the checker-examples repository. Reading those papers in concert with these instructions and the examples is recommended to get a good idea of what the system is capable of and how to use it; however, the "user interface" to the checker has changed somewhat over time, there may be inconsistencies.

Basics

Suppose we have some αProlog program, for example, defining the standard lambda calculus syntax, operational semantics, and typing rules. We now wonder if these definitions are all correct and consistent with one another. (Concretely, we imagine) The standard formalization of the intended relationship between these things is type soundness, which we can define as follows:

(Preservation)
if E has type T and E can take an evaluation step to E' then E' has type T
(Progress)
if E has type T then either E is a value or E can take an evaluation step to E'

Using αCheck, we can instruct the system to automatically search for counterexamples to these statements, that is, automatically test them, up to some resource bound. The syntax for this is as follows:

#check "tc_pres" 5 : tc([],E,T), step(E,E') => tc([],E',T).
#check "tc_prog" 5 : tc([],E,T) => not_stuck(E).

where, at the moment, a disjunctive conclusion such as value(E);step(E,_) currently needs to be defined by an auxiliary rule as part of the program.

These directives give names to the checks, give a resource bound, and state the property that the check should test. Properties are basically of the form

H1,...,Hn => C

where Hi and C are atoms.

The number 5 is a resource bound. The exact meaning of the resource bound is not particularly straightforward to explain, but basically smaller bounds search less of the search space than larger bounds, and if you make the bound large enough, eventually you will find a counterexample if there is one. In practice, bounds of around 5-10 seem to have the right balance, being large enough to find interesting small counterexamples. The search uses iterative deepening so if you choose a too-large bound you will get an idea of what the largest sensible bound is from the progress message that is printed out during search.

Check directives are ignored by default in αProlog. To actually check them, enable checking using the -check-nf flag.

By default, counterexamples are printed and you can continue searching using ";" like with normal goals. However, checking is second-class in that you currently cannot do anything with the counterexample answer substitutions within αProlog besides look at them. (the only exception to this is the #save_to_file directive, described in Saving answers).

If you want it to be a run-time error if a test fails, use #validate. If a given test is intended to fail, and you want it to be an error if no counterexamples are found, then one can use the #invalidate directive instead. These directives are useful for automatically checking results are as expected rather than exploring the counterexamples.

Limitations

Not all features of αProlog are supported by αCheck. In particular, using the following in a specification is likely to lead to unpredictable behavior or errors complaining that these features are not supported:

• use of negation-as-failure or cut
• built-in arithmetic or other nonlogical predicates
• use of free names in the head of clauses (in fact, αProlog does not handle these correctly either).

Some features are explicitly not supported by check-ne, and might be allowed by -check-nf but lead to silent failures or incorrect results.

References

• James Cheney, Alberto Momigliano: Mechanized metatheory model-checking. PPDP 2007: 75-86
• James Cheney, Alberto Momigliano, Matteo Pessina: Advances in Property-Based Testing for \alpha Prolog. TAP 2016: 37-56
• Guglielmo Fachini, Alberto Momigliano: Validating the Meta-Theory of Programming Languages (Short Paper). SEFM 2017: 367-374
• James Cheney, Alberto Momigliano: αCheck: A mechanized metatheory model checker. TPLP 17(3): 311-352 (2017)
• Francesco Komauli, Alberto Momigliano: Property-Based Testing of the Meta-Theory of Abstract Machines: an Experience Report. CILC 2018: 22-39
• Alberto Momigliano, Mario Ornaghi: The Blame Game for Property-based Testing. CILC 2019: 4-13