# Specifications Today we will prove that some functions satisfy their specifications. We'll also practice determining whether one specification refines another. ##### Exercise: spec axiom [&#10029;] Verify the correctness of f, assuming that g satisfies its specification:  (* 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.* &square; ## List max In the next exercise, we'll verify the following function lmax:  (* postcondition: [lmax lst] is the largest element in [lst]. * precondition: [lst] is not empty and has finite length. *) let rec lmax = function | [] -> failwith "Empty" | [x] -> x | h::t -> max h (lmax t)  Here are specifications for two functions that we will need:  (* postcondition: [max x y] is the maximum of [x] and [y]. * precondition: none. *) val max : int -> int -> int (* postcondition: [mem x lst] is true iff [x] is equal to a member of [lst]. * precondition: [lst] has finite length. *) val mem : int -> int list -> bool  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. * **Definition:** L(x,lst) iff mem x lst and for all y such that mem y lst, it holds that x >= y. ##### Exercise: lmax [&#10029;&#10029;&#10029;] Verify the correctness of lmax by proving the following theorem: **Theorem:** if lst<>[], then L(lmax lst,lst). *Hint: use structural induction with two base cases: one for the empty list, and another for the list with a single element.* Here are some facts about mem that you might want to use as lemmas: * **Lemma:** mem x [x] * **Lemma:** if mem y [x] then y=x. * **Lemma:** mem h (h::t) * **Lemma:** mem x t implies mem x (h::t) &square; ## Refinement ##### Exercise: Hasse [&#10029;&#10029;&#10029;] 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 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  &square; ## Additional exercises ##### Exercise: mem lemmas [&#10029;&#10029;&#10029;] Here is an implementation of mem : int -> int list -> bool:  let rec mem x = function | [] -> false | h::t -> x=h || mem x t  Prove these lemmas: * **Lemma:** mem x [x] * **Lemma:** if mem y [x] then y=x. * **Lemma:** mem h (h::t) * **Lemma:** mem x t implies mem x (h::t) &square; ## Challenge exercise [&#10029;&#10029;&#10029;&#10029;] 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