Wiki Agenda Contact English version

Circular queue in an array

Problem 3 of the second verified software competition.

The ZIP file below contains both the source code, the Why3 proof session file and the Coq scripts of the proofs made in Coq. The Why3 source code is then displayed, followed by a summary of the proofs.


Auteurs: Jean-Christophe Filliâtre / Andrei Paskevich

Catégories: Array Data Structure / Data Structures / Ghost code

Outils: Why3

Références: The 2nd Verified Software Competition

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


download ZIP archive
(* 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 int.Int
  use option.Option
  use list.List
  use import list.NthLengthAppend as L
  use import array.Array as A

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

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

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

  (* code *)

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

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

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

  let push (b: buffer 'a) (x: 'a) : unit
    requires { length b < size b }
    writes   { b.data.elts, b.len, b.sequence }
    ensures  { length b = (old (length b)) + 1 }
    ensures  { 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 = A.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) : '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) : 'a
    requires { length b > 0 }
    writes   { b.first, b.len, b.sequence }
    ensures  { length b = (old (length b)) - 1 }
    ensures  { 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 = A.length b.data in
    b.first <- b.first + 1;
    if b.first = n then b.first <- 0;
    r
end

module Harness

  use RingBuffer
  use 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 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

With sequences instead of lists

module RingBufferSeq

  use int.Int
  use import seq.Seq as S
  use import array.Array as A

  type buffer 'a = {
    mutable first: int;
    mutable len  : int;
            data : array 'a;
    ghost mutable sequence: S.seq 'a;
  }
  invariant {
    let size = A.length data in
    0 <= first <  size /\
    0 <= len   <= size /\
    len = S.length sequence /\
    forall i: int. 0 <= i < len ->
      (first + i < size ->
         S.get sequence i = data[first + i]) /\
      (0 <= first + i - size ->
         S.get sequence i = data[first + i - size])
  }
  by { first = 0; len = 0; data = make 1 (any 'a); sequence = S.empty }

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

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

  (* code *)

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

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

  let clear (b: buffer 'a) : unit
    writes  { b.len, b.sequence }
    ensures { length b = 0 }
    ensures { b.sequence = S.empty }
  = ghost (b.sequence <- S.empty);
    b.len <- 0

  let push (b: buffer 'a) (x: 'a) : unit
    requires { length b < size b }
    writes   { b.data.elts, b.len, b.sequence }
    ensures  { length b = (old (length b)) + 1 }
    ensures  { b.sequence = S.snoc (old b.sequence) x }
  = ghost (b.sequence <- S.snoc b.sequence x);
    let i = b.first + b.len in
    let n = A.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) : 'a
    requires { length b > 0 }
    ensures  { result = S.get b.sequence 0 }
  = b.data[b.first]

  let pop (b: buffer 'a) : 'a
    requires { length b > 0 }
    writes   { b.first, b.len, b.sequence }
    ensures  { length b = (old (length b)) - 1 }
    ensures  { result = S.get (old b.sequence) 0 }
    ensures  { b.sequence = (old b.sequence)[1..] }
  = ghost (b.sequence <- b.sequence[1..]);
    let r = b.data[b.first] in
    b.len <- b.len - 1;
    let n = A.length b.data in
    b.first <- b.first + 1;
    if b.first = n then b.first <- 0;
    r
end

module HarnessSeq

  use seq.Seq
  use RingBufferSeq

  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 empty };
    push b 2;
    assert { sequence b == cons 1 (cons 2 empty) };
    push b 3;
    assert { sequence b == cons 1 (cons 2 (cons 3 empty)) };
    let x = pop b in assert { x = 1 };
    assert { sequence b == cons 2 (cons 3 empty) };
    push b 4;
    assert { sequence b == cons 2 (cons 3 (cons 4 empty)) };
    let x = pop b in assert { x = 2 };
    assert { sequence b == cons 3 (cons 4 empty) };
    let x = pop b in assert { x = 3 };
    assert { sequence b == cons 4 empty };
    let x = pop b in assert { x = 4 };
    ()

  use 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 empty) };
    let h = pop b in assert { h = x };
    assert { sequence b == cons y empty };
    push b z;
    assert { sequence b == cons y (cons z empty) };
    let h = pop b in assert { h = y };
    let h = pop b in assert { h = z }

end

Why3 Proof Results for Project "vstte12_ring_buffer"

Theory "vstte12_ring_buffer.RingBuffer": fully verified

ObligationsCVC3 2.4.1CVC4 1.5CVC5 1.0.5Eprover 2.0
VC for buffer---0.02------
VC for create---0.04------
VC for length---0.01------
VC for clear---0.06------
VC for push------0.08---
VC for head------------
split_goal_right
index in array bounds---0.04------
postcondition---------0.39
VC for pop------------
split_goal_right
unreachable point---0.03------
index in array bounds---0.02------
type invariant------------
split_goal_right
type invariant---0.01------
type invariant---0.03------
type invariant---0.02------
type invariant---0.03------
type invariant---0.04------
type invariant0.04---------
type invariant---0.04------
postcondition---0.03------
postcondition---------0.42
type invariant------------
split_goal_right
type invariant---0.02------
type invariant---0.03------
type invariant---0.02------
type invariant---0.03------
type invariant---0.04------
type invariant0.05---------
type invariant0.06---------
postcondition---0.02------
postcondition---------0.57

Theory "vstte12_ring_buffer.Harness": fully verified

ObligationsCVC4 1.5
VC for harness0.12
VC for harness20.28
VC for test0.12

Theory "vstte12_ring_buffer.RingBufferSeq": fully verified

ObligationsCVC4 1.5Z3 4.11.2
VC for buffer0.04---
VC for create0.03---
VC for length0.01---
VC for clear0.06---
VC for push0.16---
VC for head0.04---
VC for pop---0.03

Theory "vstte12_ring_buffer.HarnessSeq": fully verified

ObligationsCVC4 1.5Z3 4.11.2
VC for harness0.18---
VC for harness2---1.00
VC for test---0.25