**Exercise:** Verify the correctness of f:  (* postcondition: [g x] is 3110 * precondition: x >= 0 *) val g : int -> int (* postcondition: [f x] is 3110 * precondition: x >= 1 *) let f x = g (x-1)  *Hint: the proof is very short and uses the specification axiom.* **Exercise:** Verify the correctness of lmax. Assume nothing about the implementation of max other than what is said by its specification.  (* postcondition: [max x y] is the maximum of [x] and [y]. *) val max : int -> int -> int (* postcondition: [lmax lst] is the largest element in [lst]. * precondition: [lst] is not empty. *) let rec lmax = function | [] -> failwith "Empty" | [x] -> x | h::t -> max h (lmax t)  Let's begin by formalizing what it means to be the "largest element" of a list:  Notation: let L(x,lst) mean that x is the largest element of lst. Define: L(x,lst) iff mem x lst and for all y such that mem y lst, x >= y.  Recall that mem is the list membership function. Here are some facts about mem that you might want to use as lemmas:  Lemma: mem x [x] Lemma: the only y s.t. mem y [x] is x. Lemma: mem h (h::t) Lemma: mem x t => mem x (h::t)  Prove the following theorem:  Theorem: if lst<>[], L(lmax lst,lst).  *Hint: use structural induction and the specification axiom.* ** *Exercise:** Prove the lemmas you used above. **Exercise:** Consider the following specifications for functions a&ndash;h of type int list->int. Draw a [Hasse diagram][hasse] showing which function specifications refine each other. This diagram should include a node for each function name. If function spec A refines spec B then * the name B should appear higher in the diagram, and * there should be a line in the diagram connecting A and B, unless there is some third spec C such that A refines C and C refines B. [hasse]: https://en.wikipedia.org/wiki/Hasse_diagram  (* a(x) = y, where y is the last element in x. Requires: x contains at least three elements. *) (* b(x) = y, where y is the largest element in x. Requires: x is non-empty. *) (* c(x) = y, where y is the last element in x. Requires: x is non-empty and in ascending sorted order. *) (* d(x) = y, where y is the first element in x. Requires: x is non-empty. *) (* e(x) = y, where y is an element in x. Requires: x is non-empty. *) (* f(x) = y, where y is the last element in x. Requires: x is non-empty. *) (* g(x) = y, where y is the element in x with the largest absolute value. Requires: x is non-empty. *) (* h(x) = y, where y is the largest element in x. Requires: x is non-empty and in descending sorted order. *)  *Hint: Spec b refines e and h, so b should lie below both e and h in the diagram and should be connected to them, perhaps indirectly. Assuming there is no spec that lies between b and e or between b and h in the refinement ordering, that part of the diagram would look like this:*  e h \ / b  ** \*\*Exercise:** Here is an implementation of mergesort:  let rec length = function | [] -> 0 | _::t -> 1 + length t let rec take xs i = match xs with | [] -> [] | x::xs' -> if i>0 then x::take xs' (i-1) else [] let rec drop xs i = match xs with | [] -> [] | x::xs' -> if i>0 then drop xs' (i-1) else xs let rec merge xs ys = match (xs,ys) with | ([], ys) -> ys | (xs, []) -> xs | (x::xs',y::ys') -> if x <= y then x :: merge xs' ys else y :: merge xs ys' let rec mergesort = function | [] -> [] | [x] -> [x] | xs -> let k = length xs / 2 in merge (mergesort (take xs k)) (mergesort (drop xs k))  Our goal is to prove the correctness of mergesort. The first task is to invent a specification. The function must: 1. produce output that is ordered 2. produce output that is a rearrangement of the input. **1. Ordered:** For the former, we can define a predicate:  let rec ordered = function | [] -> true | [x] -> true | x::y::ys -> x <= y && ordered (y::ys)  As a lemma, prove  For all lists xs and ys, if ordered xs and ordered ys, then ordered (merge xs ys).  Then prove  For all lists xs, ordered (mergesort xs).  **2. Rearrangement:** For the latter, we define a function to represent a list as a multiset or *bag*:  let empty_bag = fun x -> 0 let singleton_bag x = fun y -> if x=y then 1 else 0 let bag_sum b1 b2 = fun y -> (b1 y) + (b2 y) let rec bag = function | [] -> empty_bag | h::t -> bag_sum (singleton_bag h) (bag t)  As lemmas, prove  For all bags b1 and b2, bag_sum b1 b2 ~ bag_sum b2 b1. For all bags b1, b2, and b3, bag_sum b1 (bag_sum b2 b3) ~ bag_sum (bag_sum b1 b2) b3. For all bags b, bag_sum empty_bag b ~ b. For all lists xs and integers k, bag_sum (bag (take xs k)) (bag (drop xs k)) ~ bag xs. For all lists xs and ys, bag(merge xs ys) ~ bag_sum (bag xs) (bag ys).  Then prove  For all lists xs, bag (mergesort xs) ~ bag xs.  **Finally:** Conclude that mergesort satisfies the following specification:  Postcondition: mergesort xs is a list zs such that ordered zs and bag zs = bag xs. Precondition: none