1. Queue with even numbers

In Lecture 8 we specified and implemented a stack of odd integers (using a class invariant). Following the same approach, specify and implement a queue of even numbers.

2. Binary Trees

Continue working in the file Tree.dfy provided with Lecture 8. Ensure that your class invariant specifies a valid binary search tree. Also, implement the methods:

// RemoveMin() removes the minimum number
// in the tree. It returns the minimum and the new reference to the root.
method RemoveMin() returns (min: int, node: TreeNode?)

// Remove(x) removes element x from the tree, returning the
// new reference to the root
method Remove(x: int) returns (node: TreeNode?)

3. Linked Lists

Define a new class for polymorphic Linked Lists using the following internal representation:

class Node<T> {
  // element stored in the node
  var elem: T;
  // next node in the list, if any
  var next: Node?<T>;

...

}

Define a class invariant that characterizes acyclic linked lists. Also, define a constructor and methods for insertion and removal of an element. Define a method head that returns the first element and another one, called tail that returns the tail of the list.