Last updated on

Property-based testing

Welcome to week 12 of CS-214 — Software Construction!

As usual, ⭐️ indicates the most important exercises and questions and 🔥 indicates the most challenging ones. Exercises or questions marked 🧪 are intended to build up to concepts used in this week’s lab.

You do not need to complete all exercises to succeed in this class, and you do not need to do all exercises in the order they are written.

We strongly encourage you to solve the exercises on paper first, in groups. After completing a first draft on paper, you may want to check your solutions on your computer. To do so, you can download the scaffold code (ZIP).

Most of the tests we have worked with so far have checked whether a program behaves correctly on a given set of example inputs, where we specify what the “correct behavior” is for each input (e.g. by checking the observed output against the hard-coded expected output). But often, we have a more abstract understanding of what it means for the program to be correct: we want the program’s output to satisfy certain properties for all inputs. In practice, the set of all possible inputs may be too large to be worth testing exhaustively (or even infinite), so we instead run the program on some randomly generated inputs. This technique is called property-based testing (PBT).

Note that PBT does not give us a 100% guarantee that the program satisfies the stated properties, because the randomly generated inputs cover only a fraction of the whole space of possible inputs. However, it still increases our confidence in the correctness of the program, and has only a moderate cost in terms of time and effort, making it a valuable component of the software correctness toolkit.

For this exercise, we will use ScalaCheck, a Scala PBT library.

mSort

Problem 1 in the 2024 midterm gave you the implementation of an algorithm mSort and asked, “for each of the following properties, indicate whether it is true for all lists ls of type List[Int]”. Below is the implementation of mSort. The implementations of some helper functions were summarized with require-ensuring clauses in the midterm, but they are included in full below.

def mSort(ls: List[Int]): List[Int] =
  ls match
    case Nil            => Nil
    case a :: Nil       => a :: Nil
    case a :: b :: tail =>
      val (ll, lr) = split(tail)
      merge(mSort(ll), mSort(lr))

    /** Check if a given list is sorted */
def isSortedAscending(ls: List[Int]): Boolean =
  ls == ls.sortWith(_ < _)

/** Given two sorted lists, merge them into a new sorted list */
def merge(ll: List[Int], lr: List[Int]): List[Int] = {
  require(isSortedAscending(ll) && isSortedAscending(lr))

  (ll, lr) match
    case (Nil, _) => lr
    case (_, Nil) => ll
    case (lh :: lt, rh :: rt) =>
      if lh < rh then lh :: merge(lt, lr)
      else rh :: merge(ll, rt)
}.ensuring { l =>
  l == (ll ++ lr).sortWith(_ < _)
}

/** Split a list into two lists containing the first and second halves
  * respectively
  */
def split[A](ls: List[A]): (List[A], List[A]) = {
  val (ll, lr) = ls.splitAt(ls.length / 2)
  (ll, lr)

}.ensuring { case (ll, lr) =>
  ls == ll ++ lr && ll.length == ls.length / 2
}

src/main/scala/pbt/MSort.scala

And here are the properties under consideration:

// Property 1
mSort(ls).length <= 1

// Property 2
mSort(ls).length <= 2

// Property 3
isSortedAscending(mSort(ls))

// Property 4
mSort(ls).length == ls.length

// Property 5
mSort(ls).length <= ls.length

  1. Specify those properties in MSortTests.scala using ScalaCheck. If you are not sure how to use the library, consult its documentation. Change their names from “Property X” to a more descriptive but concise phrase.

    property("Property 1") =
  ???

property("Property 2") =
  ???

property("Property 3") =
  ???

property("Property 4") =
  ???

property("Property 5") =
  ???

    src/test/scala/pbt/MSortTests.scala

  2. Run the tests with test in SBT and see if the properties hold. If a property fails, you will see a message like:

    failing seed for MyTest.myproperty is 8BrWGTql0mzLgIvMVGiNy0ElC7pOMWhVE3xcntwGbOF=
[info] ! MyTest.myproperty: Falsified after 8 passed tests.
[info] > ARG_0: List("0", "0")
[info] > ARG_0_ORIGINAL: List("-1375979208", "2147483647")
    • The “seed”, 8BrW…, is for the pseudorandom input generator. It is printed so that you can reproduce the failure with the “same” random inputs if needed: testOnly -- -initialSeed 8BrW….
    • ARG_0 refers to the first (zero-indexed) argument to the property. ARG_0_ORIGINAL is the original input that triggered the failure; ScalaCheck tries to automatically simplify and minimize such inputs for easier debugging, and ARG_0 is the minimal input it could find.

  3. If a property doesn’t hold, decide whether it should hold for a correct implementation or the property itself is incorrect. Fix the implementation of mSort so that the right properties hold.

Quadtrees ⭐️

A few weeks ago, we tried to improve boids with a new data structure:

In an attempt at making a boids callback better, we have implemented a quadtree data structure to hold boid collections. Quadtrees are a two-dimensional analogue of binary search trees: they are used to organize point clouds in a way that supports quick filtering and lookups (in boids, this would allow us to quickly determine which boids are close to each other, in much less time than a linear filter of all boids).

We implemented a number of methods on the quadtree: size, insert, contains, filter, iterator and a fromCollection. Sadly, under release deadline pressure, our implementation was buggy. Your task in this exercise is to identify the bugs using property-based tests, find and fix them in the code, and finally (to finish the task we started) patch boids to use the quadtree.

Here is the type definition of a quadtree:

enum QuadTree[+T] extends Iterable[T]:
  case Empty
  case Leaf(t: List[WithPos[T]])
  case Quad(center: Vector2, nw: QuadTree[T], ne: QuadTree[T], sw: QuadTree[T], se: QuadTree[T])

src/main/scala/pbt/QuadTree.scala

Which properties?

First, write down, on paper, the properties that you think a quadtree with the methods mentioned above should satisfy. For example, what can you say about the size of a quadtree? How does the size change after inserting an element, or after filtering the quadtree with various predicates?

PBT with custom types

PBT works by generating random inputs of the right types for the properties being tested. ScalaCheck has predefined generators for standard types like Int and List, but not for the custom types we’ve defined, like Vector2 and QuadTree, so you will have to write those generators. Here is an example for Vector2:

case class PosBounds(xMin: Double, xMax: Double, yMin: Double, yMax: Double):
  val xRange = xMax - xMin
  val yRange = yMax - yMin
  def transformX(x: Double): Double = x * xRange + xMin
  def transformY(y: Double): Double = y * yRange + yMin
given PosBounds(-100, 100, -100, 100)

def position(using bounds: PosBounds): Gen[Vector2] =
  for
    x <- Gen.double
    y <- Gen.double
  yield Vector2(bounds.transformX(x), bounds.transformY(y))

src/test/scala/pbt/QuadTreeTests.scala

Gen.double uniformly samples the interval [0, 1), which we linearly transform to the interval specified in bounds. There is a default given instance of PosBounds, but code that calls position may pass in more specific instances.

Note that the generator does not explicitly use any randomness or specify the order in which random inputs are generated—it just generates one random input, delegating the randomness to Gen.double. In general, all the generators you write will be composed of these constructors (such as Gen.const) and combinators (such as Gen.listOfN) provided by ScalaCheck. Read the ScalaCheck user guide to learn how to use them. If you need even more details, consult the API documentation.

  1. Implement the generator for the WithPos class.

    def withPos(using bounds: PosBounds): Gen[WithPos[Double]] =
  ???

    src/test/scala/pbt/QuadTreeTests.scala

  2. Implement the generator for an Empty quadtree.

    val genEmpty: Gen[QuadTree[Double]] =
  ???

    src/test/scala/pbt/QuadTreeTests.scala

  3. Implement the generator for a Leaf quadtree. Respect the invariant that a leaf can only have up to 4 elements.

    def genLeaves(using bounds: PosBounds): Gen[QuadTree[Double]] =
  ???

    src/test/scala/pbt/QuadTreeTests.scala

  4. Implement the generator for a Quad quadtree. Use the bounds parameter to respect the invariant that all elements in the nw quadtree should be to the northwest of the pivot of the Quad, etc.

    def genQuads(using bounds: PosBounds): Gen[QuadTree[Double]] =
  ???

    src/test/scala/pbt/QuadTreeTests.scala

  5. Implement the generator for a QuadTree. Hint: “Generating case classes” in the ScalaCheck user guide.

    val genQuadTree: Gen[QuadTree[Double]] =
  ???

    src/test/scala/pbt/QuadTreeTests.scala

Implementing properties

Now that we have generators for our custom types, implement the properties you previously identified.

🔜 Technically, there is one more step before ScalaCheck can use our custom generators, involving given instances of the Arbitrary class. We’ve already written that code for you, so you can ignore it for now, but you can read the relevant sections of the user guide if you are curious. We will come back to this in a later exercise.

Fixing the bugs

Run the tests and see if the properties you wrote hold. If they don’t, either fix the implementation of the quadtree so that they do, or fix the properties to better reflect how a “correct” quadtree should behave.

🔥 There is one bug that is nearly unreachable with PBT, that causes an infinite recursion. Post on Ed if you are able to find it with PBT or with some other technique! And come to the verification lecture to find out how to do even better than PBT and eliminate such bugs entirely.

© 2023, 2024 EPFL. All rights reserved.