ProVal

(* The 2nd Verified Software Competition (VSTTE 2012)
   https://sites.google.com/site/vstte2012/compet

   Problem 3:
   Queue data structure implemented using a ring buffer

   Alternative solution using a model stored in a ghost field *)

module RingBuffer

  use import int.Int
  use import list.NthLengthAppend as L
  use import array.Array

  type buffer 'a = {
    mutable first: int;
    mutable len  : int;
            data : array 'a;
    ghost mutable sequence: list 'a;
  }
  invariant {
    let size = Array.length self.data in
    0 <= self.first <  size /\
    0 <= self.len   <= size /\
    self.len = L.length self.sequence /\
    forall i: int. 0 <= i < self.len ->
      (self.first + i < size ->
         nth i self.sequence = Some self.data[self.first + i]) /\
      (0 <= self.first + i - size ->
         nth i self.sequence = Some self.data[self.first + i - size])
  }

  (* total capacity of the buffer *)
  function size (b: buffer 'a) : int = Array.length b.data

  (* length = number of elements *)
  function length (b: buffer 'a) : int = b.len

  (* code *)

  let create (n: int) (dummy: 'a)
    requires { n > 0 }
    ensures { size result = n /\ result.sequence = Nil }
  = { first = 0; len = 0; data = make n dummy; sequence = Nil }

  let length (b: buffer 'a)
    ensures { result = length b }
  = b.len

  let clear (b: buffer 'a)
    ensures { length b = 0 /\ b.sequence = Nil }
  = ghost b.sequence <- Nil;
    b.len <- 0

  let push (b: buffer 'a) (x: 'a)
    requires { length b < size b }
    ensures { length b = (old (length b)) + 1 /\
      b.sequence = (old b.sequence) ++ Cons x Nil }
  = ghost b.sequence <- b.sequence ++ Cons x Nil;
    let i = b.first + b.len in
    let n = Array.length b.data in
    b.data[if i >= n then i - n else i] <- x;
    b.len <- b.len + 1

  let head (b: buffer 'a)
    requires { length b > 0 }
    ensures { match b.sequence with Nil -> false | Cons x _ -> result = x end }
  = b.data[b.first]

  let pop (b: buffer 'a)
    requires { length b > 0 }
    ensures { length b = (old (length b)) - 1 /\
      match old b.sequence with
      | Nil -> false
      | Cons x l -> result = x /\ b.sequence = l end }
  = ghost match b.sequence with Nil -> absurd | Cons _ s -> b.sequence <- s end;
    let r = b.data[b.first] in
    b.len <- b.len - 1;
    let n = Array.length b.data in
    b.first <- b.first + 1;
    if b.first = n then b.first <- 0;
    r
end

module Harness

  use import RingBuffer
  use import list.List

  let harness () =
    let b = create 10 0 in
    push b 1;
    push b 2;
    push b 3;
    let x = pop b in assert { x = 1 };
    let x = pop b in assert { x = 2 };
    let x = pop b in assert { x = 3 };
    ()

  let harness2 () =
    let b = create 3 0 in
    push b 1;
    assert { sequence b = Cons 1 Nil };
    push b 2;
    assert { sequence b = Cons 1 (Cons 2 Nil) };
    push b 3;
    assert { sequence b = Cons 1 (Cons 2 (Cons 3 Nil)) };
    let x = pop b in assert { x = 1 };
    assert { sequence b = Cons 2 (Cons 3 Nil) };
    push b 4;
    assert { sequence b = Cons 2 (Cons 3 (Cons 4 Nil)) };
    let x = pop b in assert { x = 2 };
    assert { sequence b = Cons 3 (Cons 4 Nil) };
    let x = pop b in assert { x = 3 };
    assert { sequence b = Cons 4 Nil };
    let x = pop b in assert { x = 4 };
    ()

  use import int.Int

  let test (x: int) (y: int) (z: int) =
    let b = create 2 0 in
    push b x;
    push b y;
    assert { sequence b = Cons x (Cons y Nil) };
    let h = pop b in assert { h = x };
    assert { sequence b = Cons y Nil };
    push b z;
    assert { sequence b = Cons y (Cons z Nil) };
    let h = pop b in assert { h = y };
    let h = pop b in assert { h = z }

end