#
Checkers.@test_formany
— Macro.
@test_formany [ntests = 100] [maxtests = 1000] [logto = ""] argument_data, prop
Checks prop
on randomly generated samples values specified in argument_data
. Returns Pass
if prop
holds for all values in the sample, Fail
if prop
does not hold for some sampled value, and Error
if a part of the code could not be evaluated or if insufficient non-vacuous tests are generated.
Arguments
-
argument_data
: a sequence of comma-separated expressions, where each expression specifies a dummy variable, a universe from which to sample it, and a restricted comprehension of that universe. In particular, expressions must have one of the following forms:a<x::T<b
ora>x::T>b
, wherex
is any symbol, treated as a dummy variable;T
is a type;a
&b
are arbitrary expressions to constrain the range of values forx
(provided thata<x::T<b
is meaningful givenT
and the types ofa
andb
);a<<x::T<b
,a<x::T<<b
,a>>x::T>b
ora>x::T>>b
, as above, but where using<<
will instruct@test_formany
to generate test cases away from that boundary, i.e. closer to the other boundary;a<x<b
etc., where the typeT
is omitted, and therefore defaults toFloat64
-
prop
: the property to be tested. Two types of properties are allowed:- any boolean-valued expression, referencing the dummy variables defined in
argument_data
, or - a property of the form
antecedent --> consequent
, whereantecedent
andconsequent
are themselves boolean-valued expressions that may reference dummy variables defined inargument_data
. This form is useful for expressing "if-then" relationships without thinking through how to generate test cases that satisfy the antecedent, as@test_formany
will do this for you; see below for more detail.
- any boolean-valued expression, referencing the dummy variables defined in
Optional keyword arguments include the following:
ntests = 100
: the number of tests thattest_formany
will perform
before returning Pass
.
maxtests = 1000
: the maximal number of times to attempt to generate
test cases that satisfy antecedent
, when the antecedent --> consequent
form is used.
logto = "path_to_file"
: the path to a file to which
a log of the actual test cases used will be recorded. Since @test_formany
is pseudo-random and might pass a test that you expect to fail (or vice versa), this can be useful for debugging to see which actual test cases were tested.
Details
@test_formany
generates a sample of test cases based on argument_data
, and tests prop
on these values, returning Pass
only if every test passes.
Basic Use
When prop
is just a boolean-valued expression, @test_formany
simply checks whether prop
holds for the values generated according to argument_data
.
Advanced Use: Conditional Properties and Vacuity Avoidance
When using ntests = [some integer]
, with a prop
of the form antecedent --> consequent
, @test_formany
will attempt to test ntests
cases where the conditional is not vacuous, i.e. ntests
cases where antecedent
evaluates to true. However, to prevent the test from looping infinitely, @test_formany
uses maxtests = [some integer]
to limit the number of total attempts it will make.
Consider the following example: you might wish to test this statement:
∀ 0 < x < 1, x^2 < 0.0001 --> x < 0.01
If you simply tested this statement with 100 randomly sampled values between 0 and 1, you would be unlikely actually ever to evaluate the consequent of the conditional, because most of the time x^2 < 0.0001 would not be true. So, you could use
@test_formany ntests=100 0 < x::Float64 < 1, x^2 < 0.0001 --> x < 0.01
to guarantee 100 tests where x^2 < 0.0001
was true.
However, by the same reasoning, you might actually be testing an expression for which the antecedent is itself virtually always false. Then you don't want the tests to continue forever–-you want to specify an upper bound on how many tests @test_formany
should run before it gives up. For example, using maxtests
in this case prevents @test_formany
from looping infinitely looking for a value that satisfies an impossible antecedent:
@test_formany ntests=100 maxtests=10_000 0 < x::Float64 < 1, (x < 1 && x > 2) --> x < 0.01
In this case, if the number of attempts to satisfy the antecedent exceeds maxtests
before ntests
tests do satisfy the antecedent, then @test_formany
will return Base.Test.Error
.
Keyword Argument Defaults
- If no keywords are specified,
@test_formany
assumesntests = 100, maxtests = 1000
. - If only
ntests
is specified,@test_formany
assumesmaxtests = 10*ntests
. - By default,
@test_formany
does not log output
Keyword arguments are order-invariant.
Exhaustion
@test_formany
tests a random sample of values specified by argument_data
, which in typical use will imply that it tests a random sample of values drawn from a mathematically infinite set. Consequently, @test_formany
is not exhaustive, and can therefore generate false positives, i.e. cases that generate Pass
even when a counter-example exists.
A similar and more complicated concern applies when using conditional properties. Here, the vacuity-avoidance arguments ntests
and maxtests
may result in false positives and false negatives: a conditional that is true, but with an unlikely-to-satisfy antecedent, mail fail to generate enough test cases to test the entire conditional, and therefore return Error
even when the property is true for the entire universe. On the other hand, a counter-example may still exists even when @test_formany
returns Pass
on a conditional property after testing many non-vacuous antecedents.
Examples
julia> @test_formany 100 > x::Float64 > 10, x+10 < y::Float64 << 1000, y-5 < z::Float64 < Inf, z > x+5 Test Passed Expression: (:((100 > x::Float64 > 10,x + 10 < y::Float64 << 1000,y - 5 < z::Float64 < Inf,z > x + 5)),) julia> @test_formany ntests = 1000 10 < x::Float64 < 100, x+10 < y::Float64 << 1000, y-5 < z::Float64 < Inf, z > x+6 String["x = 25.18875813550991","y = 35.192306691353075","z = 31.183953098939906"] Test Failed Expression: (:(ntests = 1000),:((100 > x::Float64 > 10,x + 10 < y::Float64 << 1000,y - 5 < z::Float64 < Inf,z > x + 6))) ## Failing to find enough non-vacuous test cases: julia> @test_formany -1000 < x::Float64 < 1000, x > 999 --> x+1 > 1000 Error During Test Test threw an exception of type ErrorException Expression: (:((-1000 < x::Float64 < 1000,$(Expr(:-->, :(x > 999), :(x + 1 > 1000))))),) Found only 1/100 values satisfying given antecedent. ## Test that `log` is an increasing function julia> @test_formany ntests=1000 Inf > x::Float64 > 0, Inf > y::Float64 > 0, x < y --> log(x) < log(y) Test Passed Expression: (:((Inf > x::Float64 > 0,Inf > y::Float64 > 0,$(Expr(:-->, :(x < y), :(log(x) < log(y)))))),:(ntests = 1000)) ## Test that f(x) = x^3 is convex on (-100,100) ## Fails, because f(x) = x^3 is not convex on that interval! julia> @test_formany 0 < a < 1,-100 < x < 100,-100 < y < 100,(a*x + (1-a)*y)^3 < a*x^3 + (1-a)*y^3 String["a = 0.39535367198058546","x = -13.538004569422625","y = 0.8504731053549079"] Test Failed Expression: (:((0 < a < 1,-100 < x < 100,-100 < y < 100,(a * x + (1 - a) * y) ^ 3 < a * x ^ 3 + (1 - a) * y ^ 3)),) ## Test that f(x) = x^3 is convex on (0,100) julia> @test_formany 0<a<1,0<x<100,0<y<100, (a*x+(1-a)*y)^3<=a*x^3+(1-a)*y^3 Test Passed Expression: (:((0 < a < 1,0 < x < 100,0 < y < 100,(a * x + (1 - a) * y) ^ 3 <= a * x ^ 3 + (1 - a) * y ^ 3)),) ## Test that Cobb-Douglas Utility is concave: ## First, define a helper function for concavity testing julia> function respects_concavity(f,t,x1,x2) f(t*x1+(1-t)*x2) > t * f(x1) + (1-t) * f(x2) end ## Same for weak concavity julia> function respects_weak_concavity(f,t,x1,x2) f(t*x1+(1-t)*x2) >= t * f(x1) + (1-t) * f(x2) end ## And one for Cobb-Douglas julia> function cobb_douglas(a,x) prod(x.^a) end ## The test below passes the @test_formany, ## since the probability of discovering a counter-example is zero. julia> @test_formany 0<t<1, 0<a<1, 1<x1<10, 1<x2<10, 1<y1<10, 1<y2<10, respects_concavity(x -> cobb_douglas( [a,1-a], x), t, [x1,y1], [x2,y2]) Test Passed Expression: (:((0 < t < 1,0 < a < 1,1 < x1 < 10,1 < x2 < 10,1 < y1 < 10,1 < y2 < 10,respects_concavity((x->begin # REPL[5], line 1: cobb_douglas([a,1 - a],x) end),t,[x1,y1],[x2,y2]))),) julia> @test_formany 0 < t < 1, 0 < a < 1, 1 < x1 < 10, 1 < x2 < 10, 1 < y1 < 10, 1 < y2 < 10,respects_weak_concavity(x -> cobb_douglas( [a,1-a], x), t, [x1,y1], [x2,y2]) Test Passed Expression: (:((0 < t < 1,0 < a < 1,1 < x1 < 10,1 < x2 < 10,1 < y1 < 10,1 < y2 < 10,respects_weak_concavity((x->begin # REPL[6], line 1: cobb_douglas([a,1 - a],x) end),t,[x1,y1],[x2,y2]))),) ## Handling Errors julia> @test_formany -1 < x < 1, abs( log(x) ) > 0 Error During Test Test threw an exception of type DomainError Expression: (:((-1 < x < 1,abs(log(x)) > 0)),) DomainError