Wiki Agenda Contact Version française

Amortized Queue, in Why3

Queue with good amortized complexity using linked lists, Why3 version


Authors: Jean-Christophe Filliâtre

Topics: List Data Structure / Data Structures

Tools: Why3

References: The 1st Verified Software Competition / The VerifyThis Benchmarks

see also the index (by topic, by tool, by reference, by year)


(*
   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
   Problem 5: amortized queue

   Author: Jean-Christophe Filliatre (CNRS)
   Tool:   Why3 (see http://why3.lri.fr/)
*)

module AmortizedQueue

  use import int.Int
  use import option.Option
  use import list.ListRich

  type queue 'a = { front: list 'a; lenf: int;
                    rear : list 'a; lenr: int; }
    invariant { length self.front = self.lenf >= length self.rear = self.lenr }

  function sequence (q: queue 'a) : list 'a =
    q.front ++ reverse q.rear

  let empty () ensures { sequence result = Nil }
  = { front = Nil; lenf = 0; rear = Nil; lenr = 0 } : queue 'a

  let head (q: queue 'a)
    requires { sequence q <> Nil }
    ensures { hd (sequence q) = Some result }
  = match q.front with
      | Nil      -> absurd
      | Cons x _ -> x
    end

  let create (f: list 'a) (lf: int) (r: list 'a) (lr: int)
    requires { lf = length f /\ lr = length r }
    ensures { sequence result = f ++ reverse r }
  = if lf >= lr then
      { front = f; lenf = lf; rear = r; lenr = lr }
    else
      let f = f ++ reverse r in
      { front = f; lenf = lf + lr; rear = Nil; lenr = 0 }

  let tail (q: queue 'a)
    requires { sequence q <> Nil }
    ensures { tl (sequence q) = Some (sequence result) }
  = match q.front with
      | Nil      -> absurd
      | Cons _ r -> create r (q.lenf - 1) q.rear q.lenr
    end

  let enqueue (x: 'a) (q: queue 'a)
    ensures { sequence result = sequence q ++ Cons x Nil }
  = create q.front q.lenf (Cons x q.rear) (q.lenr + 1)

end

download ZIP archive

Why3 Proof Results for Project "vstte10_aqueue"

Theory "vstte10_aqueue.AmortizedQueue": fully verified in 0.17 s

ObligationsAlt-Ergo (0.99.1)
VC for empty0.01
VC for head0.03
VC for create0.02
VC for tail---
split_goal_wp
  1. unreachable point0.02
2. precondition0.02
3. postcondition0.05
VC for enqueue0.02