<![CDATA[
# Specifications
Today we will prove that some functions satisfy their specifications.
We'll also practice determining whether one specification refines another.
##### Exercise: spec axiom [✭]
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.*
□
## 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 [✭✭✭]
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)`
□
## Refinement
##### Exercise: Hasse [✭✭✭]
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
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
```
□
## Additional exercises
##### Exercise: mem lemmas [✭✭✭]
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)`
□
## Challenge 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
```
]]>