**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 ```