Skip to content

Lecture 4.1: Property-based testing sort and flip_tree

Last Thursday, we built out all of the essentials necessary to operationalize PBT. Today we will use this to find some counterexamples in our sort function, followed by stating a second property for binarytrees and formalizing this with PBT.

From last class, we implemented the following: 

(* P1 *)
let rec sorted (ys : int list) : bool
  = match ys with
  | [] -> true
  | x :: [] -> true
  | i :: j :: ys' -> i <= j && sorted (j :: ys')


(* P2 *)
let rec ndups (e : int) (xs : int list) : int =
  match xs with
  | [] -> 0
  | x :: xs' -> (if e = x then 1 else 0) + (ndups e xs')

let equal_element_count (xs : int list) (ys : int list) : bool
  =  all xs (fun e -> ndups e xs = ndups e ys)
  && all ys (fun e -> ndups e xs = ndups e ys)

(* the spec *)
let sort_spec (xs : int list) (sort : int list -> int list) =
  let ys = sort xs in
  sorted ys && equal_element_count xs ys

(* generate a random list *)
let gen_uniform_list (len_bound : int) : int list =
  let len = Random.int len_bound in
  List.init len (fun _ix -> Random.int 100)

let rec forall_list (gen : unit -> int list) (prop : int list -> bool) (trials : int) : int list option =
    if trials <= 0
    then None (* No counter-example found *)
    else 
      let xs = gen () in 
      if prop xs
      then forall_list gen prop (trials - 1)
      else Some xs

Testing a sort function

there are many ways to implement a bad sort function:

  • we could define a constant function, perhaps returning []
  • we could define an identity function
  • we could reverse the input list, or perform any sort of nonsense, so long return an int list.
utop# let bad_sort (xs : int list) = xs ;; 
val bad_sort : int list -> int list

utop # forall_list (gen_uniform_list 5) (fun xs -> sort_spec xs bad_sort) 32;;
- : int list option = Some [62; 10; 65; 96]

Next up, let's actually write a sorting algorithm: insertion sort

Of course, we can also figure out whether a good sorting algorithm is counter-example-free. Let's use insertion sort:

(* sort the given list of ints in ascending order *)
let rec isort (xs : int list) =
  match xs with
  | [] -> []
  | y :: ys -> insert y (isort ys)
Most of the work will happen in the helper function, which places an element y "at the correct spot:"

(* insert the given int at its spot in ascending order *)
let rec insert (x : int) (xs : int list) : int list =
  match xs with
  | [] -> []
  | y :: xs' ->
    if x <= y                   
    then y :: x :: insert x xs'
    else y :: insert x xs'

There are three bugs in the above code. Can you spot them? At this point, we can run PBT and observe what issues arise to help us debug this code. Do this!

Let's fix the code 
(* insert the given int at its spot in ascending order *)
let rec insert (x : int) (xs : int list) : int list =
  match xs with
  | [] -> [x]            (* the base case should return a singleton list *)
  | y :: xs' ->
    if x <= y
    then x :: y ::       (* (2) x and y flipped; *)
                   xs'   (* (3) inserting more elements than necessary via recursion *)
    else y :: insert x xs'

Making the corrections, we can load this into utop:

utop# forall_list (gen_uniform_list 10) (fun xs -> 
    sort_spec xs isort
) 32;;
- : int list option = None

Properties on Binary trees

Let's look at a binary tree type in OCaml, from week 2, where the leaves are integers:

type bintree =
  | Leaf of int
  | Branch of bintree * bintree
A 'structural recursion design recipe'

Steps:

  1. copy the constructors into the pattern match
  2. remove all of statements
  3. convert all * into tuples
  4. replace all types with /unique/ variables names.
let rec bintree_func (bt : bintree) : ??? = 
  match bt with
  | Leaf v -> ... v ...
  | Branch (l, r) -> ... bintree_func l ... bintree_func r  ...

We are going to write a couple of functions on binary trees.

let rec sum_tree (t : bintree) : int = 
    match t with
    | Leaf i -> i 
    | Branch (x, y) -> sum_tree x + sum_tree y

let rec flip_tree (t : bintree) = 
    match t with
    | Leaf i -> Leaf i
    | Branch (x, y) -> Branch (flip_tree y, flip_tree x)

Formalizing a property about flip_tree

One property:

  • "when we flip a tree, we don't get the same tree back"
  • ∀ bt, not(flip_tree bt = bt)
let prop_flip_tree_not_equal (flip_tree : bintree -> bintree) =
  fun (bt : bintrees) -> not (flip_tree bt = bt)

Does this property hold?

in general, no! The mirror image of a symmetric tree is itself.

That said, it definitely is true that t = flip_tree (flip_tree t). In other words, if you flip a tree twice, you get back to the original tree. We say that flip_tree is involutive: applying the same function twice gets you back to the original value.

let prop_flip_tree_involutive (flip_tree : bintree -> bintree) =
  (* ∀ bt, flip_tree (flip_tree bt) = bt *)
  fun (bt : bintrees) -> 
    flip_tree (flip_tree bt) = bt

To test this we will need a generator of binary trees, and a testing harness:

let rec gen_bintree (leaf_bound : int) (n : int) : bintree =
  if n <= 0
  then Leaf (Random.int leaf_bound)
  else Branch (gen_bintree leaf_bound (n - 1), gen_bintree leaf_bound (n - 1))

let rec forall_bintree
    (gen : unit -> bintree)
    (prop : bintree -> bool)
    (trials : int)
    : bintree option = 
  if trials <= 0
  then None
  else
    let bt = gen () in
    if prop bt
    then forall_bintree gen prop (trials - 1)
    else Some bt

At this point, we can poke around the code in the repl:

utop# let gen = gen_bintree 10
utop# gen ;;
utop# gen 1 ();;
utop# gen 2 ();;
utop# gen 3 ();;
utop# forall_bintree (gen 3) prop_flip_tree_not_equal  1000 ;;
utop# forall_bintree (gen 3) prop_flip_tree_involutive 1000 ;;