Commit 6640a5c5 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

vstte'10 : problem 5 completed

parent b865c0c4
......@@ -3,3 +3,4 @@ vstte10_max_sum
vstte10_inverting
vstte10_search_list
vstte10_queens
vstte10_aqueue
(* VSTTE'10 competition
Problem 5: amortized queue *)
{
use export list.List
use export list.Length
use export list.Append
use export list.Reverse
type queue 'a = Q (front : list 'a) (lenf : int)
(rear : list 'a) (lenr : int)
logic inv (q : queue 'a) =
length (front q) = lenf q and
length (rear q) = lenr q and
lenf q >= lenr q
logic model (q : queue 'a) : list 'a =
append (front q) (reverse (rear q))
}
let create f lf r lr =
{ lf = length f and lr = length r }
if lf >= lr then
Q f lf r lr
else
let f = append f (reverse r) in
Q f (lf + lr) Nil 0
: queue 'a
{ inv result and model result = append f (reverse r) }
let empty () =
{}
Q Nil 0 Nil 0 : queue 'a
{ inv result and model result = Nil }
let head (q : queue 'a) =
{ inv q and model q <> Nil }
match front q with
| Nil -> absurd
| Cons x _ -> x
end
{ match model q with Nil -> false | Cons x _ -> result = x end }
let tail (q : queue 'a) =
{ inv q and model q <> Nil }
match front q with
| Nil -> absurd
| Cons _ r -> create r (lenf q - 1) (rear q) (lenr q)
end
{ inv result and
match model q with Nil -> false | Cons _ r -> model result = r end }
let enqueue (x : 'a) (q : queue 'a) =
{ inv q }
create (front q) (lenf q) (Cons x (rear q)) (lenr q + 1)
{ inv result and model result = append (model q) (Cons x Nil) }
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_aqueue.gui"
End:
*)
......@@ -17,6 +17,8 @@ theory Length
lemma Length_nonnegative : forall l:list 'a. length(l) >= 0
lemma Length_nil : forall l:list 'a. length l = 0 <-> l = Nil
end
theory Mem
......@@ -35,10 +37,50 @@ theory Nth
use import int.Int
logic nth (n : int) (l : list 'a) : option 'a = match l with
| Nil -> None
| Cons x r -> if n = 0 then Some x else nth (n - 1) r
| Nil -> None
| Cons x r -> if n = 0 then Some x else nth (n - 1) r
end
end
theory Append
use export List
logic append (l1 l2 : list 'a) : list 'a = match l1 with
| Nil -> l2
| Cons x1 r1 -> Cons x1 (append r1 l2)
end
lemma Append_assoc :
forall l1 l2 l3 : list 'a.
append l1 (append l2 l3) = append (append l1 l2) l3
lemma Append_l_nil :
forall l : list 'a. append l Nil = l
use import Length
use import int.Int
lemma Append_length :
forall l1 l2 : list 'a. length (append l1 l2) = length l1 + length l2
end
theory Reverse
use export List
use import Append
logic reverse (l : list 'a) : list 'a = match l with
| Nil -> Nil
| Cons x r -> append (reverse r) (Cons x Nil)
end
use import Length
lemma Reverse_length :
forall l : list 'a. length (reverse l) = length l
end
theory Sorted
......
Markdown is supported
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