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