why3/examples/queue_two_lists.mlw

(** 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

(** the module above is a valid implementation of queue.Queue *)
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