Testing

A counterexample generation framework for ACL2

Test formulas before and during a proof attempt, to find counterexamples and witnesses potentially saving time and effort and providing more intuition into the conjecture under scrutiny. The testing framework is tightly coupled with the data definition (See data-definitions) framework. test? guarantees printing counterexamples in terms of the top goals variables. See test? for more details and examples. The framework can be configured via a bunch of parameters whose documention you will find below. In particular, see num-trials, verbosity-level, testing-enabled.

To understand more about how testing works, please refer to the following paper http://www.ccs.neu.edu/home/harshrc/ITaITP.pdf

Subtopics

Backtrack-limit
Maximum number of backtracks allowed (per variable)
Get-ACL2s-random-testing-hints-enabled
Get current setting for random-testing-hints-enabled
Num-counterexamples
Number of Counterexamples to be shown
Num-trials
Max number of tries to find counterexamples
Num-witnesses
Number of Witnesses to be shown
Sampling-method
Specify sampling method to be used to instantiate variables
Search-strategy
Specify the search strategy to be used
Set-ACL2s-random-testing-enabled
Control enabling/disabling testing hint
Subgoal-timeout
Testing timeout (in seconds) per subgoal
Test?
Random testing using the ACL2 prover, generating counterexamples to top-level conjecture.
Testing-enabled
Testing enable/disable flag
Verbosity-level
Control verbosity of Testing