Reference solution:

let prop_clamp (lo, hi, x) =
  let r = clamp lo hi x in
  lo <= r && r <= hi

The property runs clamp and asserts the single fact that matters: the result is between lo and hi inclusive. It would catch a clamp that forgot either bound (returning x unchanged when it is too big, say). Note what it does not say: that r = x when x is already in range. That is a second, independent property worth adding.

Reference solution:

let prop_gcd_divides (a, b) =
  let g = gcd a b in
  a mod g = 0 && b mod g = 0

"Divides exactly" means the remainder is zero, so the property is a mod g = 0 && b mod g = 0. This is a good example of a property that is much easier to state than the function: we do not recompute the gcd to check it, we check the defining relationship. (Restricting the generator to positive inputs sidesteps gcd a 0 = a and the sign conventions, which would otherwise need their own cases.)

Reference solution:

let prop_insert (x, xs) =
  let sorted = List.sort compare xs in
  let result = insert x sorted in
  is_sorted result && List.length result = List.length sorted + 1

Sorting xs inside the property turns any random list into a valid input, which is cheaper than generating sorted lists directly. The conjunction states two independent facts: order is preserved, and no element was lost or duplicated. The length check is what catches a buggy insert that drops x on some path.

Reference solution:

let prop_merge (xs, ys) =
  let xs = List.sort compare xs and ys = List.sort compare ys in
  merge xs ys = List.sort compare (xs @ ys)

List.sort compare (xs @ ys) is an obviously-correct (if slower) way to get the merged result, so it makes a perfect oracle: any disagreement is a bug in merge. This is the seed of model-based testing, where the "reference" is a whole module rather than a one-line expression (Problem 8).

Reference solution:

open OUnit2
let suite_binary =
  "to_binary" >::: [
    "zero" >:: (fun _ ->
      assert_equal ~printer:(fun s -> s) "0" (to_binary 0));
    "one" >:: (fun _ ->
      assert_equal ~printer:(fun s -> s) "1" (to_binary 1));
    "six" >:: (fun _ ->
      assert_equal ~printer:(fun s -> s) "110" (to_binary 6));
    "thirteen" >:: (fun _ ->
      assert_equal ~printer:(fun s -> s) "1101" (to_binary 13));
    "negative raises" >:: (fun _ ->
      assert_raises (Invalid_argument "to_binary: negative")
        (fun () -> to_binary (-1)));
  ]

The ~printer turns a failure into a readable "expected 110, got ..." message instead of an opaque "not equal". The assert_raises case wraps the call in a thunk (fun () -> ...) so OUnit can run it and catch the exception; the expected exception must match exactly, including its string argument.

Reference solution:

open OUnit2
let suite_clamp =
  "clamp" >::: [
    "below"  >:: (fun _ -> assert_equal ~printer:string_of_int 0  (clamp 0 10 (-5)));
    "above"  >:: (fun _ -> assert_equal ~printer:string_of_int 10 (clamp 0 10 99));
    "inside" >:: (fun _ -> assert_equal ~printer:string_of_int 7  (clamp 0 10 7));
    "at lo"  >:: (fun _ -> assert_equal ~printer:string_of_int 0  (clamp 0 10 0));
    "at hi"  >:: (fun _ -> assert_equal ~printer:string_of_int 10 (clamp 0 10 10));
  ]

Five cases for the three branches plus the two boundary values where off-by-one bugs hide (< versus <=). The two "at" cases are the ones a property over random integers would almost never hit, which is exactly why hand-written boundary tests earn their keep.

Reference solution:

let gen_signed : int QCheck.Gen.t =
  QCheck.Gen.oneof_weighted [
    (1, QCheck.Gen.return 0);
    (3, QCheck.Gen.int_range (-1000) (-1));
    (3, QCheck.Gen.int_range 1 1000);
  ]

oneof_weighted picks one of the listed generators according to its weight, so return 0 guarantees zero turns up roughly one draw in seven, while the two ranges supply negatives and positives. This is the same idea as seeding a float generator with nan and infinity: if a value is special to the specification, the generator must actually produce it.

Reference solution:

let prop_counter cmds =
  let c = Counter.create () in
  let model = ref 0 in
  let step cmd =
    match cmd with
    | Incr  -> Counter.incr c;   model := !model + 1
    | Add n -> Counter.add c n;  model := !model + n
  in
  List.iter step cmds;
  Counter.get c = !model

The model is the simplest thing that could possibly track the counter's value: a bare int ref. step applies each command to both the real counter and the model, and at the end the two must agree. Because QCheck generates sequences of commands and shrinks failing ones, this single property exercises far more interleavings than you would write by hand, and reports the shortest command list that breaks the implementation.