Commit 31d43bf7 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new example in progress

parent 2814bd09
module MergesortQueue
use import int.Int
use import list.Length
use import list.Append
use import list.Permut
use import module queue.Queue
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
lemma Permut_cons_append:
forall x : 'a, l1 l2 : list 'a.
permut (Cons x l1 ++ l2) (l1 ++ Cons x l2)
lemma Permut_append:
forall l1 l2 k1 k2 : list 'a.
permut l1 k1 -> permut l2 k2 -> permut (l1 ++ l2) (k1 ++ k2)
lemma Permut_append_swap:
forall l1 l2 : list 'a.
permut (l1 ++ l2) (l2 ++ l1)
let merge (q1: t elt) (q2: t elt) (q: t elt) =
{ q.elts = Nil (* /\ sorted q1.elts /\ sorted q2.elts *) }
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
let x1 = peek q1 in
let x2 = peek q2 in
if le x1 x2 then push (pop q1) q else push (pop q2) q
{ permut q.elts (old q1.elts ++ old q2.elts) }
let rec mergesort (q: t elt) =
{ }
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
assert { q.elts = Nil };
assert { permut (q1.elts ++ q2.elts) (at q.elts 'L) };
mergesort q1;
mergesort q2;
merge q1 q2 q
{ (* sorted q.elts /\ *) permut q.elts (old q.elts) }
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/mergesort_queue.gui"
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment