mergesort_queue.mlw 1.63 KB
 Jean-Christophe Filliâtre committed Jan 20, 2012 1 2 3 4 5 6 7 `````` module MergesortQueue use import int.Int use import list.Length use import list.Append use import list.Permut `````` Andrei Paskevich committed Oct 13, 2012 8 `````` use import queue.Queue `````` Jean-Christophe Filliâtre committed Jan 20, 2012 9 10 11 12 13 14 15 16 17 18 19 `````` type elt predicate le elt elt axiom total_preorder1: forall x y: elt. le x y \/ le y x axiom total_preorder2: forall x y z: elt. le x y -> le y z -> le x z clone import list.Sorted with type t = elt, predicate le = le `````` Andrei Paskevich committed Oct 13, 2012 20 21 22 23 `````` let merge (q1: t elt) (q2: t elt) (q: t elt) requires { q.elts = Nil (* /\ sorted q1.elts /\ sorted q2.elts *) } ensures { permut q.elts (old q1.elts ++ old q2.elts) } = 'L: `````` Jean-Christophe Filliâtre committed Jan 20, 2012 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 `````` while length q1 > 0 || length q2 > 0 do invariant { permut (q.elts ++ q1.elts ++ q2.elts) (at q1.elts 'L ++ at q2.elts 'L) } variant { length q1.elts + length q2.elts } if length q1 = 0 then push (pop q2) q else if length q2 = 0 then push (pop q1) q else let x1 = peek q1 in let x2 = peek q2 in if le x1 x2 then push (pop q1) q else push (pop q2) q done (* `````` Andrei Paskevich committed Oct 13, 2012 39 40 41 42 `````` let rec mergesort (q: t elt) requires { } ensures { (* sorted q.elts /\ *) permut q.elts (old q.elts) } = 'L: `````` Jean-Christophe Filliâtre committed Jan 20, 2012 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 `````` if length q > 1 then begin let q1 = create () : t elt in let q2 = create () : t elt in while not (is_empty q) do invariant { permut (q1.elts ++ q2.elts ++ q.elts) (at q.elts 'L) } variant { length q.elts } let x = pop q in push x q1; if not (is_empty q) then let x = pop q in push x q2 done; assert { q.elts = Nil }; assert { permut (q1.elts ++ q2.elts) (at q.elts 'L) }; mergesort q1; mergesort q2; merge q1 q2 q end *) end``````