class Forall
Constants
- C
- Fail
An error occurred while checking the property
- No
The property was not true of at least one tested input
- Ok
The property was true of all tested inputs
- Options
TODO: Is there a way to provide a default implementation of `shrink`? Will it interefere with a user-given implementation?
- Vacuous
Couldn't find enough suitable inputs to test
Public Class Methods
check(input, random, options = nil, &prop)
click to toggle source
# File lib/forall.rb, line 30 def check(input, random, options = nil, &prop) options ||= Options.new options.max_shrink ||= 100 if input.exhaustive? options.max_ok ||= input.size * 0.90 options.max_skip ||= input.size * 0.10 else options.max_ok ||= 100 options.max_skip ||= options.max_ok * 0.10 end if prop.arity == 1 _prop = prop prop = lambda{|x,_| _prop.call(x) } end raise ArgumentError, "property must take one or two arguments" \ unless prop.arity == 2 counter = Counter.new input.each(random) do |example| return Ok.new(random.seed, counter) if counter.ok >= options.max_ok return Vacuous.new(random.seed, counter) if counter.skip >= options.max_skip catch(:skip) do if prop.call(example, counter) counter.ok += 1 else return no(random, counter, input.shrink, example, options, prop) end end rescue Exception => error counter.fail += 1 return fail(random, counter, input.shrink, example, options, prop, error) end # Didn't meet ok_max because input was exhausted Ok.new(random.seed, counter) end
Private Class Methods
_weight(xs, min, max)
click to toggle source
# File lib/forall.rb, line 80 def _weight(xs, min, max) n = xs.length.to_f r = max - min xs.map.with_index{|x, k| C.new(x, max-r*k/n, 0) } end
fail(random, counter, shrink, shrunk, options, prop, error)
click to toggle source
Search for a simpler example that causes the same exception
# File lib/forall.rb, line 166 def fail(random, counter, shrink, shrunk, options, prop, error) return Fail.new(random.seed, counter, shrunk, error) if shrink.nil? fitness = 0 queue = _weight(shrink.call(shrunk), 0, 1) _counter = counter.shrunk until queue.empty? or _counter.total >= options.max_shrink c = queue.shift catch(:skip) do if prop.call(c.value, _counter) _counter.ok += 1 else _counter.no += 1 end rescue => e # TODO: Do we care if this exception is different from `error`? if c.fitness > fitness fitness = c.fitness shrunk = c.value end _counter.fail += 1 queue.concat(_weight(shrink.call(c.value), c.fitness+0.5, c.fitness+1.0)) queue.sort_by!{|x| -x.fitness } end end Fail.new(random.seed, counter, shrunk, error) end
no(random, counter, shrink, shrunk, options, prop)
click to toggle source
Search for the simplest counterexample
# File lib/forall.rb, line 89 def no(random, counter, shrink, shrunk, options, prop) return No.new(random.seed, counter, shrunk) if shrink.nil? # The problem of finding the smallest counterexample can be described in # terms of local search. The search space has a graph structure (think of # a tree with duplicate nodes) and candidate solutions are examples drawn # from the domain over which the property holds. The criterion to be # maximized is the simplicity of a counterexample -- simple is not meant # in any particular formal sense. The neighborhood relation is described # by the user-provided function `shrink`, which should return candidate # solutions that are only incrementally simpler than its argument. # # For ease of use, the user does not need to provide a function to # calculate the criterion (simplicity) of a candidate solution. Instead, # it is inferred by the number of edges in its path from the root and by # the relative order in which it was returned among other candidate # solutions (the first being simplest). There is also no requirement for # a user-supplied heuristic to rank partial solutions, as it would often # be difficult to estimate an optimal solution let alone calculate some # quantifiable difference between it and any other partial solution. # # The solution space is finite (eventually `shrink` must return an empty # list), but because we have a self-imposed computational budget, its not # feasible to exhaustively search for the deepest leaf in the tree. We can # conjure a heuristic based on a candidate solution's ratio of ancestors # that are examples or counterexamples. If one candidate solution was # generated among many which did not disprove the property, and another # candidate solution was generated among many counterexamples, we will # assume the first candidate is less likely to produce more # counterexamples than the second. # # shrunk # | # [✓] [✕] [✓] # 1.0 0.8 0.6 # / \ # [✕] [✓] [✕] [✓] [✓] # 2.0 1.8 1.6 1.6 1.4 # / / \ / \ # # The computational budget is in terms of how many candidate solutions we # will test to determine if they are counterexamples. As a result, the # heuristic value of a candidate solution would seem to require testing # each of its ancestors and their siblings. For now that is what we'll do, # but in the future there may be a way to make do with partial information # and reserve the budget for exploring the tree more deeply. fitness = 0 queue = _weight(shrink.call(shrunk), 0, 1) _counter = counter.shrunk until queue.empty? or _counter.total >= options.max_shrink c = queue.shift catch(:skip) do if prop.call(c.value, _counter) _counter.ok += 1 else if c.fitness > fitness fitness = c.fitness shrunk = c.value end _counter.no += 1 queue.concat(_weight(shrink.call(c.value), c.fitness+0.5, c.fitness+1.0)) queue.sort_by!{|x| -x.fitness } end rescue => e _counter.fail += 1 raise e end end No.new(random.seed, counter, shrunk) end
weight(xs, min, max)
click to toggle source
# File lib/forall.rb, line 74 def weight(xs, min, max) n = xs.length.to_f r = max - min xs.map.with_index{|x, k| [x, max-r*k/n] } end