8.1 KiB
8.1 KiB
(*
Write appropriate definitions and specifications for
functions split and merge, used by the merge sort
algorithm defined below in the module.
Note that the verification of mergesort relies only
on the specifications ("contracts") of the auxiliary
functions, and not on their code. As such, it is crucial
to include in them every aspect required for the
verification conditions of the sorting algorithm
to be successfully discharged.
Note also that although Why3 is capable of automatically
proving the termination of functions with simple recursive
patterns, that does not apply to the mergesort function.
We thus include in the contract the variant "length l",
which is valid since the function is recursively called
on lists that are shorter than l.
*)
module MergeSort
use int.Int
use list.List
use list.Length
use list.Permut
use list.Append
use list.SortedInt
let rec function split (l :list int) : (list int, list int)
ensures { let (l1, l2) = result in permut l (l1++l2) }
ensures {let (l1,l2) = result in length l<2 || (length l>=2 &&
length l1<length l2 && length l2 < length l1)}
= match l with
| Nil -> (Nil, Nil)
| Cons x Nil -> (l, Nil)
| Cons x (Cons y t) -> let (l1, l2) = split t
in (Cons x l1, Cons y l2)
end
let rec function merge (l1 l2 :list int) : list int
requires { sorted l1 && sorted l2 }
ensures { sorted result}
ensures {permut result (l1++l2)}
= match l1, l2 with
Nil, _ -> l2
| _, Nil -> l1
| (Cons x l1'), (Cons y l2') -> if x<=y
then Cons x (merge l1' l2)
else Cons y (merge l1 l2')
end
let rec function mergesort (l :list int)
ensures { sorted result }
ensures { permut l result }
variant { length l }
=
match l with
| Nil -> Nil
| Cons x Nil -> Cons x Nil
| _ -> let (l1,l2) = split l
in merge (mergesort l1) (mergesort l2)
end
predicate is_a_sorting_algorithm (f: list int -> list int) =
forall al :list int. permut al (f al) /\ sorted (f al)
goal is_a_sorting_algorithm : is_a_sorting_algorithm mergesort
end
(*
The selection sort algorithm sorts an array
by successively placing in each position the
“next minimum” element, as follows:
[40, 20, 10, 30, 60, 0, 80]
[0, 20, 10, 30, 60, 40, 80]
[0, 10, 20, 30, 60, 40, 80]
[0, 10, 20, 30, 60, 40, 80]
[0, 10, 20, 30, 60, 40, 80]
[0, 10, 20, 30, 40, 60, 80]
[0, 10, 20, 30, 40, 60, 80]
[0, 10, 20, 30, 40, 60, 80]
1. Complete the contract of function swap, writing
adequate pre- and post-conditions.
Recall that "length a" gives you the allocated length
of array a.
2. Write a contract for function select.
Write also one or more loop invariants that allow
you to prove the correctness of the function.
Note that a loop variant is not required, since
"for" loops are bounded.
3. Write one or more loop invariants that allow you to prove
the correctness of selection_sort_1.
You may need to modify the contract of select in order
for the loop invariant of selection_sort_1 to be proved.
4. Finally, write the algorithm selection_sort_2, which does
not use the function select. It will have a nested loop;
write invariants for both loops and prove the correctness
of the algorithm.
*)
module SelectionSort
use int.Int
use ref.Ref
use array.Array
use array.IntArraySorted
use array.ArrayPermut
use array.ArrayEq
let swap (a: array int) (i: int) (j: int)
requires { 0 <= i< length a && 0 <= j< length a }
ensures { (old a)[i] = a[j] && (old a)[j] = a[i] }
ensures { forall k:int. 0<=k<length a -> k<>i -> k<>j -> (old a)[i] = a[j]}
ensures { permut_all (old a) a }
= let v = a[i] in
a[i] <- a[j];
a[j] <- v
(* returns the index of a minimum of
the segment of a between indexes i and length a -1.
*)
let select (a: array int) (i: int) : int
requires { 0 <= i < length a}
ensures { i <= result < length a }
ensures { forall k:int. 0<=k<length a -> a[result] <= a[k]}
= let ref min = i in
for j = i + 1 to length a - 1 do
invariant { i <= min < j }
invariant { forall k:int. i <= k < j -> a[min] <= a[k] }
if a[j] < a[min] then min <- j
done;
min
let selection_sort_1 (a: array int)
ensures { sorted a }
ensures { permut_all (old a) a }
= for i = 0 to length a - 1 do
invariant { sorted_sub a 0 i }
invariant { forall k1 k2:int. 0<= k1<i<=k2<length a -> a[k1]<=a[k2]}
invariant { permut_all (old a) a }
let min = select a i
in if min <> i then swap a min i
done
let selection_sort_2 (a: array int) =
ensures { sorted a }
ensures { permut_all (old a) a }
...
end