A property is a Boolean claim about program behavior over a range of inputs. Rather than naming a few expected input-output pairs, it states an invariant: something that should remain true whenever suitable values are supplied. Property-based testing separates that behavioral specification from the work of constructing test cases. A generator supplies values under declared constraints, and a test runner searches those values for one that falsifies the claim. section 8.0 section 8.6
For a list reversal operation, reversing twice should return the original list. The first reverse may produce many arrangements, but the second must restore the starting value. Another useful claim relates the first element of a list to the last element of its reverse. Neither property defines reverse completely; together they form a partial specification that can be exercised across generated lists. section 8.1 section 8.1.2
Binding generated values to a predicate
A property combines a Gen[A], which produces test data, with an A => Boolean predicate. Prop.forAll asks that every generated A satisfy the predicate. Here the generator makes lists of bounded integers, while each predicate expresses one behavioral constraint. val intList = Gen.listOf(Gen.choose(0, 100)) val prop = Prop.forAll(intList)(ns => ns.reverse.reverse == ns) && Prop.forAll(intList)(ns => ns.headOption == ns.reverse.lastOption) section 8.1 section 8.1.2
Checking cannot establish truth over an infinite domain merely by trying random cases. A successful randomized run means the property was unfalsified by the cases tested; a failure supplies a counterexample and the number of prior successes. For a finite, practically small domain, exhaustive generation can test every input and justify reporting the property as proved. section 8.1 section 8.6
A property needs a composable result, not merely console output. If checking only prints, combining two properties would discard information and produce independent reports. Modeling a property as a computation that returns a Result preserves whether it passed, failed with a case and success count, or was proved. This makes conjunction and other Boolean-style combinators meaningful. section 8.1.3 section 8.2.3
Useful properties often expose assumptions and relationships rather than duplicate an implementation:
- For nonempty lists, max must be an element of the list and no element may exceed it; generating empty lists reveals that List.max is undefined there. section 8.2.2 section 8.6
- For sorted lists, ordering and preservation of elements can both be checked. section 8.2.2 section 8.6
- For sum, reversing a list must not change the result, and sums of partitions can be recombined. section 8.1 section 8.6
- For takeWhile, every returned element must satisfy its predicate; testing this thoroughly also requires generated functions. section 8.3
Properties also express laws of abstractions. A hardcoded equality such as mapping over a parallel computation can be verified once, while a quantified law varies both generated values and execution environments. When repeated plumbing hides the intended law, a specialized combinator such as forAllPar can restore the statement’s clarity. Properties therefore test APIs at the level of their algebraic relationships, not only their individual examples. section 8.0 section 8.2.3
Listing 8.1 ScalaCheck properties
import org.scalacheck.{Gen, Prop}
val intList = Gen.listOf(Gen.choose(0, 100)) #1
val prop = #2
Prop.forAll(intList)(ns =>
ns.reverse.reverse == ns) && #3
Prop.forAll(intList)(ns =>
ns.headOption == ns.reverse.lastOption) #4
val failingProp =
Prop.forAll(intList)(ns => ns.reverse == ns) #5
Compare two valid invariants with a deliberately false one. The failing predicate claims every list equals its reverse, so a generated asymmetric list is enough to refute it. section 8.1
