Skip to content
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
256 lines (195 sloc) 9.17 KB


Composition with Detailed Reporting

  • Propositions are composable using all operations available in first-order logic.
  • When propositions fail, care is taken to provide enough information to comprehend why, quickly. This is a goal even when the proposition is the composite of many underlying propositions of which, only a few failed.
  • Individual propositions can written to provide specialised info about why they fail, when they fail.

This property checks that each number in a list is even, divisible by 3 and divisible by 5:

val even = Prop.test[Int]("even", _ % 2 == 0)
val div3 = Prop.test[Int]("div3", _ % 3 == 0)
val div5 = Prop.test[Int]("div5", _ % 5 == 0)
val prop = (even & div3 & div5).forallF[List] rename "Example"

This is a sample failure report:

Property [Example] failed.

Input: [List(15, 30, 60, 25)].

Root causes:
  2 failed axioms, 2 causes of failure.
  ├─ even
  │  ├─ Invalid input [15]
  │  └─ Invalid input [25]
  └─ div3
     └─ Invalid input [25]

Failure tree:
  └─ (even ∧ div3 ∧ div5)
     ├─ even
     └─ div3

Runtime Assertion

In cases where we can't encode constraints using types, we generally write property-based tests. Just as the compiler cannot prove these constraints, nor can it prove that we've written data generators that will cover all cases. Thus as an additional safety check I like to validate the assumed laws at runtime using real data. I (may) also want these checks omitted from production code so as not to impact performance. Nyaya covers these scenarios.

  • Use the same code to validate real data at runtime, and test with random data in unit tests.
  • Runtime validation can be removed by specifying a scalac flag -Xelide-below.
object MyProps {
  val foo: Prop[Foo] = ...

case class Foo(a: Int, b: String) {
  import nyaya.prop._
  this assertSatisfies

Generating Random Data

Simply import nyaya.gen.Gen and follow the API.

Combinators are all in Gen instances and the companion object.


Type to generate Constraints Expression
String None. Gen.string
String Length between 4 and 12. Gen.string(4 to 12)
String Exactly 6 chars, A-Za-z0-9. Gen.alphaNumeric.string(6)
List[Int] None.
List[Int] Non-empty.
List[Int] Max 8 elements. to 8)
Set[Int] Each element ≥ 0. Gen.positiveInt.set
Map[Int, Option[Boolean]] None.
Map[Int, Option[Boolean]] ≤ 4 entries. to 4)
Map[String, Set[Int]] ≤ 4 elements per set.
≤ 10 map entries. to 4).mapBy(Gen.string)(0 to 10)

Note: Gen does not contain a .suchThat or .filter. Don't generate data just to throw it away. Instead, write an accurate generator. There are better ways than throw-away-retry.


Say we have these data types

  case class Id(value: Int)

  case class Blah(ids: Set[Id], prevCoord: Option[(Double, Double, Double)])

Generators for each are:

  val id: Gen[Id] =
    Gen.positiveInt map Id

   // Using for-comprehension
   val blah: Gen[Blah] =
     for {
       ids       <- id.set
       prevCoord <- Gen.double.triple.option
     } yield Blah(ids, prevCoord)

   // Quicker
   val blah: Gen[Blah] =
    Gen.apply2(Blah)(id.set, Gen.double.triple.option)

Testing with Random Data (pt.1)

  • Different settings for JVM/JS. By default…
    • JVM tests are large in quantity and data size, and they run in parallel.
    • JS tests are smaller in quantity and data size, and run on a single-thread.
  • Settings can be configured per-test or per-module if required. (Here, implicits are used for the Settings.)
  • A debug-mode is available in Settings to display verbose info about the testing and data-generation. It also has a nice little max line length so the output remains comprehensible. And it's in colour. Whoa!....
val gen : Gen[A] = ...
val prop: Prop[A] = ...

import nyaya.test.PropTest._

gen mustSatisfy prop        // Method 1
prop mustBeSatisfiedBy gen  // Method 2

Testing with Random Data (pt.2)

This is where things may start to differ from what you're used to... What happens when your proposition needs a little extra data just for testing? Wouldn't that require type gymnastics for composition? Yes. But there's another way...

When writing a suite of propositions to test behaviour, there are often many props with similar inputs. The strategy thus far has been to create a context (class) in which an iteration of random data has been generated (supplied via class constructor), and then test within that context. So instead of composing Prop[Set[A]] with Prop[(Set[A],A,A)] (which needs two As just for testing), you instead create a context class like class SetTest[A](s: Set[A], a1: A, a2: A) and within that use Eval instead of Prop, the difference being that Eval is evaluated immediately and doesn't need input later.

Eval has all the same logic operations that Prop has; implication, negation, forall, etc.

A nice benefit of this approach is that your data generators do less work. If you're testing 2 string props:

  1. (s: String) => s.reverse.reverse == s
  2. (a: String, b: String) => (a + b).length == a.length + b.length

then you gain nothing by ensuring that the reverse test gets a string different than a or b. It's more efficient to generate two strings and pick one to use for the reverse test.


See MultimapTest.scala for a real example.


You can prove a proposition by testing it with all possible, or legal values. Domain exists for this purpose and should be used in place of Gen.

// This is (the type of) proposition we want to prove
val prop: Prop[Option[Boolean]] = ...

// There are three possibilities: None, Some(false), Some(true)
// Establishing all possible values is easy
val domain: Prop[Option[Boolean]] =

import nyaya.test.PropTest._

domain mustProve prop       // Method 1
prop mustBeProvedBy domain  // Method 2


Validation is the easy part. Just use Prop.distinct.

case class Thing(id: Int, name: String)
case class AllThings(timestamp: Long, things: List[Thing])

val p: Prop[AllThings] = Prop.distinct("thing IDs", (_: AllThings)

Generation is normally much harder but with Nyaya, hopefully you'll find it easy. I sure do!

There is a class called Distinct that will ensure generated data is unique, usually with just a few combinators. I'll introduce it first by showing a few examples, with an explanation after.

// Let's start with something trivial: uniqueness in a List[Int]
val d =[List]
val g =

// How about people with unique names
case class Person(id: Long, name: String)
val g = Gen.apply2(Person)(Gen.long, Gen.string1)
val d = Distinct.str.contramap[Person](, (person, newName) => person.copy(name = newName))
g map

// The whole (a,b)=>a.copy(b=b) thing gets old after a while
// Let's use Monocle to create lenses!
case class Person(id: Long, name: String)

// Now let's generate a List[Person] with unique ids and names
val personGen = Gen.apply2(Person)(Gen.long, Gen.string1)

val distinctId   =
val distinctName =
val d            = (distinctId * distinctName).lift[List]

val g: Gen[List[Person]] = personGen.list map

It works by knowing how to provide a unique value when a duplicate is found, the behaviour of which is provided by Distinct.Fixer. Once a Fixer exists, it is then passed to a Distinct which is used for type navigation and composition.

Uniqueness doesn't have to be restricted to a single field; it can extend across multiple fields in multiple types. This is an example:

// Say we have these types...
import monocle.macros.Lenses

case class Id(value: Long)

case class Donkey(id: Id, name: String)

case class Horse (id: Id, happy: Boolean)

case class Farm(ds: List[Donkey], hs: Vector[Horse])

// Now say we want to prevent duplicate IDs between the donkeys and horses in Farm
// No duplicate IDs in Farm is acheived thus:

val distinctId     = Distinct.flong.xmap(Id)(_.value).distinct
val distinctDonkey =
val distinctHorse  =
val distinctFarm   = distinctDonkey.lift[List].at(Farm.ds) +

val farmGen : Gen[Farm] = ...
val farmGen2: Gen[Farm] = farmGen map

Other validation

  • Set membership tests. All give detailed info on failure.
    • Prop.whitelist - Test that all members are on a whitelist.
    • Prop.blacklist - Test that no members are on a blacklist.
    • Prop.allPresent - Test that no required items are missing.
  • CycleDetector - Easily detect cycles in recursive data.
    • Directed graphs.
    • Undirected graphs.
You can’t perform that action at this time.