Queue implemented using two lists
Implementation of a mutable queue using two lists.
Auteurs: Léo Andrès
Catégories: Data Structures
Outils: Why3
see also the index (by topic, by tool, by reference, by year)
Implementation of a mutable queue using two lists.
Author: Léo Andrès (Univ. paris-Sud)
module Queue use int.Int use mach.peano.Peano use list.List use list.Length use list.Reverse use list.NthNoOpt use list.Append use seq.Seq use seq.FreeMonoid type t 'a = { mutable front: list 'a; (* entry *) mutable rear: list 'a; (* exit *) ghost mutable seq: Seq.seq 'a; } invariant { length seq = Length.length front + Length.length rear } invariant { Length.length front > 0 -> Length.length rear > 0 } invariant { forall i. 0 <= i < length seq -> seq[i] = let n = Length.length rear in if i < n then nth i rear else nth (Length.length front - 1 - (i - n)) front } meta coercion function seq let create () : t 'a ensures { result = empty } = { front = Nil; rear = Nil; seq = empty } let push (x: 'a) (q: t 'a) : unit writes { q } ensures { q = snoc (old q) x } = match q.front, q.rear with | Nil, Nil -> q.rear <- Cons x Nil | _ -> q.front <- Cons x q.front end; q.seq <- snoc q.seq x let rec lemma nth_append (i: int) (l1: list 'a) (l2: list 'a) requires { 0 <= i < Length.length l1 + Length.length l2 } ensures { nth i (Append.(++) l1 l2) = if i < Length.length l1 then nth i l1 else nth (i - Length.length l1) l2 } variant { l1 } = match l1 with | Nil -> () | Cons _ r1 -> if i > 0 then nth_append (i - 1) r1 l2 end (* TODO: move this to stdlib ? *) let rec lemma nth_rev (i: int) (l: list 'a) requires { 0 <= i < Length.length l } ensures { nth i l = nth (Length.length l - 1 - i) (reverse l) } variant { l } = match l with | Nil -> absurd | Cons _ s -> if i > 0 then nth_rev (i - 1) s end exception Empty let pop (q: t 'a) : 'a writes { q } ensures { (old q) <> empty } ensures { result = (old q)[0] } ensures { q = (old q)[1 ..] } raises { Empty -> q = old q = empty } = let res = match q.rear with | Nil -> raise Empty | Cons x Nil -> q.front, q.rear <- Nil, reverse q.front; x | Cons x s -> q.rear <- s; x end in q.seq <- q.seq [1 ..]; res let peek (q: t 'a) : 'a ensures { q <> empty } ensures { result = q[0] } raises { Empty -> q == empty } = match q.rear with | Nil -> raise Empty | Cons x _ -> x end let safe_pop (q: t 'a) : 'a requires { q <> empty } writes { q } ensures { result = (old q)[0] } ensures { q = (old q)[1 ..] } = try pop q with Empty -> absurd end let safe_peek (q: t 'a) : 'a requires { q <> empty } ensures { result = q[0] } = try peek q with Empty -> absurd end let clear (q: t 'a) : unit writes { q } ensures { q = empty } = q.seq <- empty; q.rear <- Nil; q.front <- Nil let copy (q: t 'a) : t 'a ensures { result == q } = { front = q.front; rear = q.rear; seq = q.seq } let is_empty (q: t 'a) ensures { result <-> q == empty } = match q.front, q.rear with | Nil, Nil -> true | _ -> false end let length (q: t 'a) : Peano.t ensures { result = Seq.length q.seq } = let rec length_aux (acc: Peano.t) (l: list 'a) : Peano.t ensures { result = acc + Length.length l } variant { l } = match l with | Nil -> acc | Cons _ s -> length_aux (Peano.succ acc) s end in length_aux (length_aux Peano.zero q.front) q.rear let transfer (q1: t 'a) (q2: t 'a) : unit writes { q1, q2 } ensures { q1 = empty } ensures { q2 = (old q2) ++ (old q1) } = match q2.rear with | Nil -> q2.front, q2.rear, q2.seq <- q1.front, q1.rear, q1.seq | _ -> q2.front <- Append.(++) q1.front (Append.(++) (reverse q1.rear) q2.front); q2.seq <- q2.seq ++ q1.seq; end; clear q1 end module Correct use Queue as Q clone queue.Queue with type t = Q.t, exception Empty = Q.Empty, val create = Q.create, val push = Q.push, val pop = Q.pop, val peek = Q.peek, val safe_pop = Q.safe_pop, val safe_peek = Q.safe_peek, val clear = Q.clear, val copy = Q.copy, val is_empty = Q.is_empty, val length = Q.length, val transfer = Q.transfer end
the module above is a valid implementation of queue.Queue
download ZIP archive
Why3 Proof Results for Project "queue_two_lists"
Theory "queue_two_lists.Queue": fully verified
Obligations | Alt-Ergo 2.3.0 | CVC4 1.6 | CVC5 1.0.5 | |
VC for t | --- | 0.06 | --- | |
VC for create | --- | 0.04 | --- | |
VC for push | 0.18 | --- | --- | |
VC for nth_append | 0.04 | --- | --- | |
VC for nth_rev | 0.02 | --- | --- | |
VC for pop | --- | --- | --- | |
split_vc | ||||
exceptional postcondition | 0.01 | --- | --- | |
precondition | 0.01 | --- | --- | |
type invariant | 0.01 | --- | --- | |
type invariant | 0.01 | --- | --- | |
type invariant | 0.07 | --- | --- | |
postcondition | 0.01 | --- | --- | |
postcondition | 0.01 | --- | --- | |
postcondition | 0.01 | --- | --- | |
precondition | 0.01 | --- | --- | |
type invariant | 0.01 | --- | --- | |
type invariant | 0.01 | --- | --- | |
type invariant | 1.64 | --- | --- | |
postcondition | 0.01 | --- | --- | |
postcondition | 0.01 | --- | --- | |
postcondition | 0.00 | --- | --- | |
VC for peek | 0.02 | --- | --- | |
VC for safe_pop | 0.01 | --- | --- | |
VC for safe_peek | 0.01 | --- | --- | |
VC for clear | 0.01 | --- | --- | |
VC for copy | 0.02 | --- | --- | |
VC for is_empty | --- | --- | 0.08 | |
VC for length | 0.02 | --- | --- | |
VC for transfer | --- | --- | --- | |
split_vc | ||||
type invariant | 0.01 | --- | --- | |
type invariant | 0.01 | --- | --- | |
type invariant | 0.01 | --- | --- | |
postcondition | 0.01 | --- | --- | |
postcondition | 0.02 | --- | --- | |
type invariant | 0.01 | --- | --- | |
type invariant | 0.02 | --- | --- | |
type invariant | 0.42 | --- | --- | |
postcondition | --- | 0.06 | --- | |
postcondition | 0.01 | --- | --- |
Theory "queue_two_lists.Correct": fully verified
Obligations | Alt-Ergo 2.3.0 | CVC4 1.6 |
VC for create'refn | --- | 0.03 |
VC for push'refn | --- | 0.06 |
VC for pop'refn | 0.01 | --- |
VC for peek'refn | --- | 0.05 |
VC for safe_pop'refn | --- | 0.04 |
VC for safe_peek'refn | --- | 0.05 |
VC for clear'refn | --- | 0.05 |
VC for copy'refn | --- | 0.02 |
VC for is_empty'refn | --- | 0.05 |
VC for length'refn | --- | 0.04 |
VC for transfer'refn | --- | 0.04 |