Mixing random and exhaustive testing

Unison's test.verify function lets you do both exhaustive test case generation and random generation (or a mix of the two). Let's start with exhaustive generation:

test.verify do
  use Nat +
  a = each [1, 2, 3, 4]
  b = each [4, 5, 6, 7]
  ensureEqual (a + b) (b + a)

[Ok "Passed"]

This is going to try all possible pairs taken from the two lists. It uses the Each ability. If we instead want randomness, we can do:

test.verify do
  use Nat +
  use Random natIn
  Each.repeat 50
  a = natIn 0 1000
  b = natIn 0 1000
  ensureEqual (a + b) (b + a)

[Ok "Passed"]

All right, but what if we want to mix the two? Suppose we want a to be exhaustively generated, but b to be Random? That's easy:

test.verify do
  use Nat +
  a = each [1, 2, 3, 4]
  Each.repeat 10
  b = Random.natIn 0 1000
  ensureEqual (a + b) (b + a)

[Ok "Passed"]

Notice that I moved the Each.repeat below the exhaustive generation of a. The effect this will have is that for each a that is selected, it will generation 10 random b values and check that the property holds.

But what if we want to combine exhaustive and random generation for a single value? That's easy too, just use Each.append:

test.verify do
  use Nat +
  a = Each.append (do each [1, 2, 3, 4]) do
    Each.repeat 10
    Random.natIn 0 1000
  b = each [4, 5, 6, 7]
  ensureEqual (a + b) (b + a)

[Ok "Passed"]

For generating a this will first use the provided list, then it will produce 10 random values.

Enjoy! See test.verify, Each, and Random.