Skip to content

Homework 4

Due: Monday, October 6 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.

Priority Queues

In this homework, you will analyze an API for priority queues. 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. We will take our type of elements to be string throughout. Then, a particular priority queue is given by type Q along with the following operations:

  • empty : Q, returning the empty queue.
  • push : Q -> string -> int -> Q, where we add the given string with priority given by the integer onto the queue, returning the modified queue;
  • peek : Q -> (string * int) option, which returns the highest-priority element of the queue (if it exists);
  • size : Q -> int, which returns the number of elements in the queue;
  • pop : Q -> Q, which returns a new queue with the highest-priority element removed (according to peek); and
  • increment : Q -> Q, 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).

Translated into our encoding of APIs in OCaml, we get the following interface:

type 's pq_ops = { 
    empty : 's;
    push : 's -> string -> int -> 's;
    peek : 's -> (string * int) option;
    size : 's -> int;
    pop : 's -> 's;
    increment : 's -> 's;
}
This interface is included in hw4.ml.

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 queue, standing for the type of 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 English description of what the property means.

We give two example properties below: 

Property 1: If we push onto the empty queue, then peek, we get the thing we pushed with the same priority. 
------
forall x : string, 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 : queue, forall x : string, forall y : string, 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. 

(* *** 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 queue, string, 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 : 's pq_ops) (x : string) (i : int) : bool = 
    ops.peek (ops.push ops.empty x i) = Some (x, i)

let prop2 (ops : 's 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 : 's pq_ops) .... : bool = .... 
let prop4 (ops : 's 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. In class we did this by making a function similar to gen_pq : 's pq_ops -> int -> 's, just returning the queue directly. While this works, it is a bit difficult to understand the counter-examples you would get from PBT. Instead, 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 instruction = | Push of string * int | Pop | Increment

Then, you will do two things:

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

let gen_ins () : 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 a priority queue implementation and a list of instructions, creates a queue by following these operations: 

let rec mk_queue (ops : 's pq_ops) (xs : instruction list) : 's = 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 queue of type 's.

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"

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 constrast 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 's (i.e., the queue) in your property, you should instead sample an instruction list (say, xs) via gen_ins and pass the property mk_queue ops xs. This will also cause the return type for your counter-example to not be an actual queue (of type 's), but instead an 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 's pq_ops -> unit -> T option, where T is the type of counter-example. For example: 

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

let prop2_test (ops : 's pq_ops) () : (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 : 's pq_ops) () : ... option = 
    forall ... (fun ... -> prop3 ops ....) 32

let prop4_test (ops : 's 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.

Q5: Writing your own implementation

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

type my_q = unit (* Replace with your chosen type! *)
let my_q_ops : my_q pq_ops = 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: 

let my_q_correct () : bool = 
    prop1_test my_q_ops () = None && 
    prop2_test my_q_ops () = None  
    (* TODO: Add in your tests here! )

Q7: Grading Criteria

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

Q7: Inspecting Buggy Traces

One way to think about a data structure is about the set of traces it generates. For our priority queue, a trace is given by:

  • 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.

In essence, a trace is the "history" of the queue along with a certain behavior of the queue on an observation. 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.)

Below, we will give you a variety of traces, and you will write (in a comment, indicated in hw4.ml) if the trace contains a correct observation or not. If it is incorrect, give the correct observation.

Q7: Grading Criteria

For each question below, whether:

  • You correctly identify which traces are correct; and
  • If you give the correct observations for each incorrect one.

Q7.1

Instructions: [Push ("A", 0); Push ("B"; 0); Pop; Increment; Increment; Push ("A", -1)]
Observation: size returns 2

To enter in hw4.ml: 

- Correct trace (Y/N):
- Corrected observation, if incorrect trace (write N/A if correct trace):

Q7.2

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

To enter in hw4.ml: 

- Correct trace (Y/N):
- Corrected observation, if incorrect trace (write N/A if correct trace):

Q7.3

Instructions:[Increment; Push ("C", 1); Push ("A", 0); Push ("B", 3); Push ("B", 1); Increment; Pop] 
Observation: size returns 4

To enter in hw4.ml: 

- Correct trace (Y/N):
- Corrected observation, if incorrect trace (write N/A if correct trace):

Q7.4

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

To enter in hw4.ml: 

- Correct trace (Y/N):
- Corrected observation, if incorrect trace (write N/A if correct trace):