๐ ๐
Checkers
NEWS  2020 Nov. 11
This package is currently not working.
I am looking into updating it for Julia 1.5
However, it seems that all of the functionality in this package can be replicated, albeit with slightly clunkier syntax, just using
@testset "Example" begin
for x in [Explicit Cases, Perhaps Constructed Using rand()]
@test Property(x)
end
end
Old Readme
Automated testing macros inspired by a Julia implementation of Koen Claessen and John Hughes' QuickCheck propertybased randomized tester.
Checkers lets you write quick propertybased tests:
julia> using Checkers
julia> f(x) = x^2
julia> @test_formany 10<x<10, f(x) >= 0
Test Passed
Expression: (:((10 < x < 10, f(x) >= 0)), :(mode = test_formany))
julia> @test_forall x in 10:10, f(x) >= 0
Test Passed
Expression: (x in 10:10, f(x) >= 0)
@test_forall x in 0:10, f(x) >= 0
julia> @test_forall x in 10:10, f(x) > 0 #Should fail b/c f(0) = 0
Test Failed
Expression: (x in 10:10, f(x) > 0)
ERROR: There was an error during testing
Quickstart Guide
This package provides three macros for test generation:
@test_forall
@test_formany
@test_exists
In each case, the basic format is
@[test] [set of values to test] [property to test]
The property is any expression that evaluates to a boolean, making reference to some dummy variable specified in the set of values to test.
The macros differ in how they specify and choose values to test:

Use
@test_forall
when you can specify the exact finite set of values to test. For example,3:3
specifies the exact set of 7 Int64 values, {3,2,1,0,1,2,3}, on which you wish to test the property. Because the user specifies the test universe completely, and that universe is finite, every value is tested and @test_forall returns only true positives and true negatives. 
Use
@test_formany
when you wish to specify a (possibly infinite) set of values to test by restricted comprehension from some universe. For example,3 < x::Float64 < 3
specifies that some number ofFloat64
sx
, satisfying the condition3 < x < 3
, will be tested for the property. Note that@test_formany
is meant to capture the idea of the universal quantifier, but is not universal on infinite sets, since the package will only run a finite number of tests. That is,@test_formany
may return a false positive, as it cannot be comprehensive. It will not, however, return a false negative. 
Use
@test_exists
like@test_formany
, but when you wish the test to pass when at least one value satisfies the property, rather than when all tested values satisfy the property. Like@test_formany
,@test_exists
simulates the existential quantifier, but is not strictly speaking complete. That is,@test_exists
may return a false negative, in the case that a value exists but was not lucky enough to be tested. It will not, however, return a false positive.
The Macros in More Detail
@test_forall
takes an expression specifying one or more dummy variables,
discrete sets of values for those variables, and an expression, and tests the
expression substituting every combination of the variables
(the Cartesian product of their possible value sets).
(Since Julia 0.5,
@test_forall x in [Collection], P(x)
is quite similar to
@test for x in [Collection] P(x) end
,
and we may deprecate / remove it for that reason.)
The property may be a conditional expression such as P(x) > Q(x)
,
in which case truth may be vacuous when P(x)
is false \forall x
tested.
@test_formany
functions like @test_forall
, but allows quantifying over
infinite sets such as [a,b] \subset \mathbb R
, etc. by sampling these
sets uniformly at random. It provides additional modifiers to control
how many tests it runs, which are especially helpful for ensuring
that conditionalexpression tests are not only passed vacuously.
@test_exists X
is essentially shorthand for ! (@test_formany !X)
.
Exhaustion
Note that @test_formany
and @test_exists
are not strictly speaking exhaustive
or true universal/existential quantifiers. @test_formany x Expr(x)
may pass
even when \exists x
s.t. Expr(x)
is false, and @test_exists x Expr(x)
may
fail even under the same circumstances. However, @test_forall
is exhaustive.
Tests that do not exhaust their universe take additional keyword arguments
ntests
and maxtests
to control how many tests to run.
Examples
Basic usage:
@test_forall x in 1:5, x^2 < 30
@test_formany 1 < x < 5, x^2 < 30
@test_exists 1 < x < 5, x^2 < 30
Control how many tests in @test_formany
:
@test_formany ntests = 10_000 1 < x < 5, x^2 < 30
Test a conditional property, passing only if 100 of the tests are not vacuous:
@test_formany ntests = 100 0 < x < Inf, 0 < y < Inf, x < y > log(x)<log(y)
Test a conditional property, passing only if 100 of the tests are not vacuous, but only allow 100 tests:
@test_formany ntests = 100 maxtests = 100 0 < x < 10, 0 < y < 10, x < y > x^2 < y^2
Test a conditional property, passing only if 100 of the test are not vacuous, but allow 100,000 tests:
@test_formany ntests = 100 maxtests = 100_000 0 < x < 10, 0 < y < 10, x < y > x^2 < y^2
Note that while the former (maxtests=100
) usually fails, the latter (maxtests=100_000
) passes.
This is because @test_formany
generates 100 random pairs of (x,y)
, but not all of them
are likely to satisfy x < y
. Therefore when maxtests=100
, it will not generate
enough pairs to test the consequent of the conditional expression.
See ?@test_forall
, etc. and examples/examples.jl
for more detailed information.
Logging
Test logging is available in @test_formany
to see which values were actually tested
by using the keyword logto
and supplying an output path:
@test_formany logto = "tests.csv" 1<x<5, x^2 < 30
Output
Test macros output results of type Base.Test.Pass
, Base.Test.Fail
,
or Base.Test.Error
in order to function seamlessly with Base.Test.@testset
.
@testset "Multiple tests" begin
@test_forall x in 1:5, x^2 < 30
@test_forall x in 1:6, x^2 < 30
end
See Also
Also of note are these more comprehensive (and we feel complicated) packages. Our goal is to provide a lightweight, readytouse outofthebox alternative:
License
The Checkers.jl package is licensed under the MIT "Expat" License:
Copyright (c) 2017: Efim Abrikosov & Philip Kalikman.
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
Credits
This package was codesigned and cowritten by Efim Abrikosov and Philip Kalikman while each was a graduate student at Yale University.

Efim wrote the majority of the code, which is based on but does not directly use the work of Patrick O'Leary

Philip designed the majority of the functionality and syntax, building on the work (in Haskell) of Koen Classen and John Hughes