Skip to content

Homework 4

Due: Friday, February 6th at 11:59pm.

Submission Instructions

Start with the template code here.

  • Replace each failwith "TODO" with your solution.
  • Be sure to test your solutions in utop or in tests alongside your submission. To load your file into utop, use #use "hw4.ml";;.
  • Submit your version of hw4.ml to the HW4 assignment on Gradescope. Only submit hw4.ml; NOT any other files or folders.
  • At the top of the template file, there is a comment for you to write in approximately how many hours you spent on the assignment. Filling this in is optional, but helpful feedback for the instructors.

Q0: Designing a simple specification for int lists:

Design a function duplicate_element. Given a list of values that can be checked for equality, if there exists at least one that appears more than once, return one of those repeated integers. If there are no duplicates, it should return none. First write the signature, an informal purpose statement in the form of a comment, and a formal purpose as a prop_duplicate_element that ensures that the returned element does indeed appear more than once. If none is returned, prop_duplicate_element should validate that the list indeed did not contain any duplicates. Implement the function (hint: sorting first might help) and use the provided forall function to ensure your function works. You could also try to write regular unit tests, but they might be fragile—why would that be?

The duplicate_element function you define must be polymorphic, and you will use the polymorphic forall, but you only need to consider random positive integers for your implementations.

[Note: The description was changed on 4/2 to clarify that your prop_duplicate_element should also validate that returning none is valid.]

Priority Queues

In this homework, you will analyze an API for a priority queue. A priority queue is a data structure that allows you to push/pop elements into and out of it, but each element is also associated to a priority given by an integer. In addition to pushing and popping elements, you will also be able to modify priorities, as well as peek at the top of the queue (but without removing the element) and take the size of the priority queue. A priority queue will take in arbitrary elements 'a.

For the remaining questions, you must implement the following functions for a priority queue backed by a polymorphic list ('a * int) list. The interface to your priority queue will be defined by the following operations:

  • empty : unit -> 'a pqueue, returning the empty queue.
  • push : 'a pqueue -> 'a -> int -> 'a pqueue, where we add an element with some priority given by the integer onto the queue, returning the modified queue;
  • peek : 'a pqueue -> ('a * int) option, which returns the highest-priority element of the queue (if it exists);
  • size : 'a pqueue -> int, which returns the number of elements in the queue;
  • pop : 'a pqueue -> 'a pqueue, which returns a new queue with the highest-priority element removed (according to peek); and
  • increment : 'a pqueue -> 'a pqueue, which adds 1 to the priority of everything in the queue.

(By highest priority, we mean the largest.) For peek, tiebreaks in priority can be resolved arbitrarily. For pop, the element returned by peek should be the one removed. Note that if we push s with priority i twice into the queue, then there are two copies of that element (and thus if one is popped, the other will remain).

We will package these up into the following record type:

type 'a pq_ops = {
    empty : unit -> 'a pqueue;
    push : 'a pqueue -> 'a -> int -> 'a pqueue;
    peek : 'a pqueue -> ('a * int) option;
    size : 'a pqueue -> int;
    pop : 'a pqueue -> 'a pqueue;
    increment : 'a pqueue -> 'a pqueue;
}

In this homework, you will: create and encode a test suite for priority queues; evaluate various examples against your test suite; and implement a priority queue which must pass your test suite. We will design our tests by letting empty, push, pop, and increment be the ways that we can create queues; and letting peek and size be the way in which we make an observation over queues. Thus, every test will be about the behavior of peek and size on a particular queue.

Q1: Constructing a Test Suite

First, write down a number of property that should hold for any priority queue.

Each property should universally quantify over zero or more variables (including some of type pqueue, standing for the type of priority queue we will be testing), and then give an equation that specifies what should happen when we peek into some use of the queue. For each property, give a short, informal English description of what the property means.

Two example properties are provided below:

Property 1: If we push onto the empty queue, then peek, we get the thing we pushed with the same priority.
------
forall x : 'a, forall i : int,
    peek (push empty x i) = Some (x, i)

Property 2: When we push two elements onto a queue, and then take the size,
this gives the same result as reversing the pushes.
-----
forall q : pqueue, forall x : 'a, forall y : 'a, forall i : int, forall j : int,
    size (push (push q x i) y j) =
    size (push (push q y j) x i)

Write each of your properties in the above format, in the space designated in the template. Your properties will be named "Property 3", "Property 4", and so on; and should go in the comment block looking like the following

(* *** PROPERTIES GO HERE ***

*)
Q1: Grading Criteria

Whether you have written at least two additional properties in the above format, which:

1. Gives a brief English description of the property; and
2. Gives a formal property, which can quantify over variables of type `pqueue`, `'a`, and `int`, that specifies the behavior of `size` or `peek` on a particular constructed queue.

Q2: Constructing a test suite

Now that you have written your properties from Q1, you will encode these into OCaml. In this question, you will do this by writing each property as a function that takes in the quantified variables (as well as the priority queue implementation), and then compute whether the property is satisfied in these inputs.

For our two example properties, we write:

let prop1 (ops : 'a pq_ops) (x : string) (i : int) : bool =
  ops.peek (ops.push (ops.empty ()) x i) = Some (x, i)

let prop2 (ops : 'a pq_ops) (q : 's) (x : string) (y : string) (i : int) (j : int) : bool =
  ops.size (ops.push (ops.push q x i) y j)
  =
  ops.size (ops.push (ops.push q y j) x i)

Thus, since you have two more properties, they will look like

let prop3 (ops : 'a pq_ops) .... : bool = ....
let prop4 (ops : 'a pq_ops) .... : bool = ....
Q2 : Grading Criteria

Whether you have successfully transcribed your properties from Q1 into functions that take in the quantified variables as input.

Q3: Randomly Sampling Queues

To evaluate whether your formal properties actually hold, we will devise a way to sample random queues. Instead of generating the queues directly, we will represent sampled queues by an explicit sequence of instructions that will generate the queue. Given these instructions, we then can generate a queue directly.

We first have this datatype:

type 'a instruction = | Push of 'a * int | Pop | Increment

Then, you will do two things:

Q3.1 First, create a random generator for a list of instructions.

let gen_ins () : 'a instruction list = failwith "TODO"

Q3.1: Grading Criteria

Whether gen_ins type checks and uses randomness to create a list of instructions. Its usefulness will be determined in later questions.

Q3.2 Then, write a function that: given our priority queue implementation and a list of instructions, creates a queue by following these operations, which we will package into a record type:

let rec mk_queue
    (ops : 'a pq_ops)
    (xs : 'a instruction list) : 'a pqueue = failwith "TODO"

This function should return ops.empty () when no instructions are given.

Q3.2: Grading Criteria

Whether mk_queue correctly follows the list of instructions to create a pqueue of type 'a.

Q3.3 Additionally, implement functions to generate strings and integers, which will be useful for later tests:

let gen_string () : string = failwith "TODO"

let gen_priority () : int = failwith "TODO"

Later, we will use strings as elements of our priority queue

Q3.3: Grading Criteria

Whether gen_string and gen_priority use randomness to generate their output types.

Q4: Implementing Random Tests

Now that we have a way to generate queues using instructions, we will use these to implement random tests using your implemented properties from Q2. For each property you implemented in Q2, use forall (along with gen_pair) to sample the arguments for each property. (In contrast to HW3, we will just use forall and sample pairs via gen_pair to handle multiple arguments. These functions are contained within hw4.ml.)

For arguments of type 'a pqueue in your property, you should instead sample an 'a instruction list (say, xs) via gen_ins and pass the property the output of mk_queue ops xs. This will also cause the return type for your counter-example to not be an actual queue (of type 'a pqueue), but instead an 'a instruction list --- the way in which you arrived to that queue.

  • Call each random test propI_test, where I is the number of the property.
  • Each test should have type string pq_ops -> unit -> T option, where T is the type of counter-example and string elements are used as elements of your properties.

For example:

let prop1_test (ops : string pq_ops) () : (string * int) option =
    forall (gen_pair gen_string gen_priority) (fun (x, i) -> prop1 ops x i) 32

let prop2_test (ops : string pq_ops) () : (string instruction list * (string * (string * (int * int)))) option =
    forall (gen_pair gen_ins (gen_pair gen_string (gen_pair gen_string (gen_pair gen_priority gen_priority))))
               (fun (xs, (x, (y, (i, j)))) ->
                prop2 ops (mk_queue ops xs) x y i j
               ) 32

Since you have at least two properties, your code will look like

let prop3_test (ops : string pq_ops) () : ... option =
    forall ... (fun ... -> prop3 ops ....) 32

let prop4_test (ops : string pq_ops) () : ... option =
    forall ... (fun ... -> prop4 ops ....) 32

(The number of tests, 32, is completely arbitrary. Feel free to have any number you wish here.)

Q4: Grading Criteria

Whether your tests successfully use forall to call your properties.

One way to think about counterexamples you will encounter is that they denote the "history" of the queue, along with an observation. We say that these make up the trace of a data structure, for priority queues this includes:

  • a list of instructions (either Push (x, y), Pop, or Increment, where x : string and y : int); and
  • an observation, such as size, along with the output.

For example, a trace for a correct priority queue will look like:

Instructions: [Push ("A", 2); Push ("B", 3); Pop; Increment]
Observation:  peek returns Some ("A", 3)

Since after we push "A" and "B", then pop, we now have "A" with priority 2; then, after we increment, we only have "A" with priority 3 (For this problem, we read instructions as happening left-to-right).

Q5: Writing your implementation

Now, write your own implementation of a (correct) priority queue.

let empty (() : unit) : 'a pqueue = failwith "TODO"
let push (pq : 'a pqueue) (el : 'a) (priority : int) : 'a pqueue = failwith "TODO"
let peek (pq : 'a pqueue) : ('a * int) option = failwith "TODO"
let size (pq : 'a pqueue) : int = failwith "TODO"
let pop (pq : 'a pqueue) : 'a pqueue = failwith "TODO"
let increment (pq : 'a pqueue) : 'a pqueue = failwith "TODO"

Q6: Grading Criteria

Only if it type checks.

Q6: Demonstrating Correctness

Finally, use your test suite from Q4 to show that your queue is correct. To do this, you will write a function of type unit -> bool that will call all of your propI_tests, and ensure that they are all None:

(* We will provide my_pq_api, a global variable that packages up your implementations *)
let my_q_correct () : bool =
  prop1_test my_pq_api () = None &&
  prop2_test my_pq_api () = None
  (* TODO: Add in your tests here! *)

Q6: Grading Criteria

That you include all of your tests in my_q_correct and your implementation from Q6 is correct relative to these tests.