Ctrl+K

Exercises

6.11. Exercises#

Solutions to most exercises are available. Fall 2022 is the first public release of these solutions. Though they have been available to Cornell students for a few years, it is inevitable that wider circulation will reveal improvements that could be made. We are happy to add or correct solutions. Please make contributions through GitHub.

Exercise: spec game [★★★]

Pair up with another programmer and play the specification game with them. Take turns being the specifier and the devious programmer. Here are some suggested functions you could use:

  • num_vowels : string -> int

  • is_sorted : 'a list -> bool

  • sort : 'a list -> 'a list

  • max : 'a list -> 'a

  • is_prime : int -> bool

  • is_palindrome : string -> bool

  • second_largest : int list -> int

  • depth : 'a tree -> int

Exercise: poly spec [★★★]

Let’s create a data abstraction for single-variable integer polynomials of the form

\[ c_n x^n + \dotsb + c_1 x + c_0 . \]

Let’s assume that the polynomials are dense, meaning that they contain very few coefficients that are zero. Here is an incomplete interface for polynomials:

(** [Poly] represents immutable polynomials with integer coefficients. *)
module type Poly = sig
  (** [t] is the type of polynomials *)
  type t

  (** [eval x p] is [p] evaluated at [x]. Example: if [p] represents
      $3x^3 + x^2 + x$, then [eval 10 p] is [3110]. *)
  val eval : int -> t -> int
end

Finish the design of Poly by adding more operations to the interface. Consider what operations would be useful to a client of the abstraction:

  • How would they create polynomials?

  • How would they combine polynomials to get new polynomials?

  • How would they query a polynomial to find out what it represents?

Write specification comments for the operations that you invent. Keep in mind the spec game as you write them: could a devious programmer subvert your intentions?

Exercise: poly impl [★★★]

Implement your specification of Poly. As part of your implementation, you will need to choose a representation type t. Hint: recalling that our polynomials are dense might guide you in choosing a representation type that makes for an easier implementation.

Exercise: interval arithmetic [★★★★]

Specify and implement a data abstraction for interval arithmetic. Be sure to include the abstraction function, representation invariant, and rep_ok. Also implement a to_string function and a format that can be installed in the top level with #install_printer.

Exercise: function maps [★★★★]

Implement a map (aka dictionary) data structure with abstract type ('k, 'v) t. As the representation type, use 'k -> 'v. That is, a map is represented as an OCaml function from keys to values. Document the AF. You do not need an RI. Your solution will make heavy use of higher-order functions. Provide at least these values and operations: empty, mem, find, add, remove.

Exercise: set black box [★★★]

Go back to the implementation of sets with lists in the previous chapter. Based on the specification comments of Set, write an OUnit test suite for ListSet that does black-box testing of all its operations.

Exercise: set glass box [★★★]

Achieve as close to 100% code coverage with Bisect as you can for ListSet and UniqListSet.

Exercise: random lists [★★★]

Use QCheck.Gen.generate1 to generate a list whose length is between 5 and 10, and whose elements are integers between 0 and 100. Then use QCheck.Gen.generate to generate a 3-element list, each element of which is a list of the kind you just created with generate1.

Then use QCheck.make to create an arbitrary that represents a list whose length is between 5 and 10, and whose elements are integers between 0 and 100. The type of your arbitrary should be int list QCheck.arbitrary.

Finally, create and run a QCheck test that checks whether at least one element of an arbitrary list (of 5 to 10 elements, each between 0 and 100) is even. You’ll need to “upgrade” the is_even property to work on a list of integers rather than a single integer.

Each time you run the test, recall that it will generate 100 lists and check the property of them. If you run the test many times, you’ll likely see some successes and some failures.

Exercise: qcheck odd divisor [★★★]

Here is a buggy function:

(** [odd_divisor x] is an odd divisor of [x].
    Requires: [x >= 0]. *)
let odd_divisor x =
  if x < 3 then 1 else
    let rec search y =
      if y >= x then y  (* exceeded upper bound *)
      else if x mod y = 0 then y  (* found a divisor! *)
      else search (y + 2) (* skip evens *)
    in search 3

Write a QCheck test to determine whether the output of that function (on a positive integer, per its precondition; hint: there is an arbitrary that generates positive integers) is both odd and is a divisor of the input. You will discover that there is a bug in the function. What is the smallest integer that triggers that bug?

Exercise: qcheck avg [★★★★]

Here is a buggy function:

(** [avg [x1; ...; xn]] is [(x1 + ... + xn) / n].
     Requires: the input list is not empty. *)
let avg lst =
  let rec loop (s, n) = function
    | [] -> (s, n)
    | [ h ] -> (s + h, n + 1)
    | h1 :: h2 :: t -> if h1 = h2 then loop (s + h1, n + 1) t
      else loop (s + h1 + h2, n + 2) t
  in
  let (s, n) = loop (0, 0) lst
  in float_of_int s /. float_of_int n

Write a QCheck test that detects the bug. For the property that you check, construct your own reference implementation of average—that is, a less optimized version of avg that is obviously correct.

Exercise: exp [★★]

Prove that exp x (m + n) = exp x m * exp x n, where

let rec exp x n =
  if n = 0 then 1 else x * exp x (n - 1)

Proceed by induction on m.

Exercise: fibi [★★★]

Prove that forall n >= 1, fib n = fibi n (0, 1), where

let rec fib n =
  if n = 1 then 1
  else if n = 2 then 1
  else fib (n - 2) + fib (n - 1)

let rec fibi n (prev, curr) =
  if n = 1 then curr
  else fibi (n - 1) (curr, prev + curr)

Proceed by induction on n, rather than trying to apply the theorem about converting recursion into iteration.

Exercise: expsq [★★★]

Prove that expsq x n = exp x n, where

let rec expsq x n =
  if n = 0 then 1
  else if n = 1 then x
  else (if n mod 2 = 0 then 1 else x) * expsq (x * x) (n / 2)

Proceed by strong induction on n. Function expsq implements exponentiation by repeated squaring, which results in more efficient computation than exp.

Exercise: expsq simplified [★★★]

Redo the preceding exercise, but with this simplified version of the function. The simplified version requires less code, but requires an additional recursive call.

let rec expsq' x n =
  if n = 0 then 1
  else (if n mod 2 = 0 then 1 else x) * expsq' (x * x) (n / 2)

Exercise: mult [★★]

Prove that forall n, mult n Z = Z by induction on n, where:

let rec mult a b =
  match a with
  | Z -> Z
  | S k -> plus b (mult k b)

Exercise: append nil [★★]

Prove that forall lst, lst @ [] = lst by induction on lst.

Exercise: rev dist append [★★★]

Prove that reverse distributes over append, i.e., that forall lst1 lst2, rev (lst1 @ lst2) = rev lst2 @ rev lst1, where:

let rec rev = function
  | [] -> []
  | h :: t -> rev t @ [h]

(That is, of course, an inefficient implementation of rev.) You will need to choose which list to induct over. You will need the previous exercise as a lemma, as well as the associativity of append, which was proved in the notes above.

Exercise: rev involutive [★★★]

Prove that reverse is an involution, i.e., that forall lst, rev (rev lst) = lst. Proceed by induction on lst. You will need the previous exercise as a lemma.

Exercise: reflect size [★★★]

Prove that forall t, size (reflect t) = size t by induction on t, where:

let rec size = function
  | Leaf -> 0
  | Node (l, v, r) -> 1 + size l + size r

Exercise: fold theorem 2 [★★★★]

We proved that fold_left and fold_right yield the same results if their function argument is associative and commutative. But that doesn’t explain why these two implementations of concat yield the same results, because ( ^ ) is not commutative:

let concat_l lst = List.fold_left ( ^ ) "" lst
let concat_r lst = List.fold_right ( ^ ) lst ""

Formulate and prove a new theorem about when fold_left and fold_right yield the same results, under the relaxed assumption that their function argument is associative but not necessarily commutative. Hint: make a new assumption about the initial value of the accumulator.

Exercise: propositions [★★★★]

In propositional logic, we have atomic propositions, negation, conjunction, disjunction, and implication. For example, raining /\ snowing /\ cold is a proposition stating that it is simultaneously raining and snowing and cold (a weather condition known as Ithacating).

Define an OCaml type to represent propositions. Then state the induction principle for that type.

Exercise: list spec [★★★]

Design an OCaml interface for lists that has nil, cons, append, and length operations. Design the equational specification. Hint: the equations will look strikingly like the OCaml implementations of @ and List.length.

Exercise: bag spec [★★★★]

A bag or multiset is like a blend of a list and a set: like a set, order does not matter; like a list, elements may occur more than once. The number of times an element occurs is its multiplicity. An element that does not occur in the bag has multiplicity 0. Here is an OCaml signature for bags:

module type Bag = sig
  type 'a t
  val empty : 'a t
  val is_empty : 'a t -> bool
  val insert : 'a -> 'a t -> 'a t
  val mult : 'a -> 'a t -> int
  val remove : 'a -> 'a t -> 'a t
end

Categorize the operations in the Bag interface as generators, manipulators, or queries. Then design an equational specification for bags. For the remove operation, your specification should cause at most one occurrence of an element to be removed. That is, the multiplicity of that value should decrease by at most one.