Wiki Agenda Contact Version française

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.


Authors: Jean-Christophe Filliâtre / Andrei Paskevich

Topics: Array Data Structure / Data Structures / Ghost code

Tools: Why3

References: 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 import int.Int
  use import option.Option
  use import list.List
  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) : 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 = 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) : '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 = 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

With sequences instead of lists

module RingBufferSeq

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

  type buffer 'a = {
    mutable first: int;
    mutable len  : int;
            data : array 'a;
    ghost mutable sequence: S.seq 'a;
  }
  invariant {
    let size = Array.length self.data in
    0 <= self.first <  size /\
    0 <= self.len   <= size /\
    self.len = S.length self.sequence /\
    forall i: int. 0 <= i < self.len ->
      (self.first + i < size ->
         S.get self.sequence i = self.data[self.first + i]) /\
      (0 <= self.first + i - size ->
         S.get self.sequence i = 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) : 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 = 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) : '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 = Array.length b.data in
    b.first <- b.first + 1;
    if b.first = n then b.first <- 0;
    r
end

module HarnessSeq

  use import seq.Seq
  use import 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 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 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 in 4.09 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)Coq (8.4pl6)Z3 (4.3.2)
VC for create0.01---------
VC for length0.02---------
VC for clear0.01---------
VC for push------------
split_goal_wp
  1. index in array bounds0.01---------
2. type invariant------------
inline_goal
  1. type invariant------------
split_goal_wp
  1. VC for push0.02---------
2. VC for push0.02---------
3. VC for push0.02---------
4. VC for push0.01---------
5. VC for push0.03---------
6. VC for push0.16---------
7. VC for push0.08---------
3. type invariant0.01---------
4. postcondition0.02---------
5. postcondition0.01---------
VC for head------------
split_goal_wp
  1. index in array bounds0.02---------
2. postcondition------1.25---
VC for pop------------
split_goal_wp
  1. unreachable point0.00---------
2. index in array bounds0.02---------
3. type invariant------------
split_goal_wp
  1. VC for pop0.01---------
2. VC for pop0.02---------
3. VC for pop0.01---------
4. VC for pop0.020.02------
5. VC for pop0.01---------
6. VC for pop---0.06------
7. VC for pop0.02---------
4. postcondition0.01---------
5. postcondition------------
split_goal_wp
  1. VC for pop0.01---------
2. VC for pop---0.25------
3. VC for pop0.00---------
6. type invariant------------
split_goal_wp
  1. VC for pop0.01---------
2. VC for pop0.01---------
3. VC for pop0.02---------
4. VC for pop0.010.02------
5. VC for pop0.01---------
6. VC for pop---0.09------
7. VC for pop------------
7. postcondition0.01---------
8. postcondition------------
split_goal_wp
  1. VC for pop0.01---------
2. VC for pop------1.28---
3. VC for pop0.02---------

Theory "vstte12_ring_buffer.Harness": fully verified in 2.22 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)
VC for harness------
split_goal_wp
  1. precondition0.01---
2. precondition0.01---
3. precondition0.010.02
4. precondition0.02---
5. precondition0.02---
6. assertion0.18---
7. precondition0.03---
8. assertion0.25---
9. precondition0.04---
10. assertion0.30---
VC for harness2------
split_goal_wp
  1. precondition0.00---
2. precondition0.01---
3. assertion0.01---
4. precondition0.01---
5. assertion0.08---
6. precondition0.02---
7. assertion---0.04
8. precondition0.00---
9. assertion0.04---
10. assertion---0.06
11. precondition0.02---
12. assertion---0.06
13. precondition0.03---
14. assertion---0.06
15. assertion0.05---
16. precondition0.02---
17. assertion0.08---
18. assertion0.08---
19. precondition0.03---
20. assertion0.10---
VC for test------
split_goal_wp
  1. precondition0.01---
2. precondition0.01---
3. precondition0.02---
4. assertion0.17---
5. precondition0.01---
6. assertion0.04---
7. assertion0.02---
8. precondition0.01---
9. assertion0.08---
10. precondition0.03---
11. assertion0.05---
12. precondition0.03---
13. assertion0.05---

Theory "vstte12_ring_buffer.RingBufferSeq": fully verified in 0.11 s

ObligationsAlt-Ergo (0.99.1)
VC for create0.01
VC for length0.02
VC for clear0.01
VC for push0.02
VC for head0.02
VC for pop0.03

Theory "vstte12_ring_buffer.HarnessSeq": fully verified in 3.79 s

ObligationsAlt-Ergo (0.99.1)Z3 (3.2)Z3 (4.3.2)
VC for harness------0.02
VC for harness2---------
split_goal_wp
  1. precondition0.01------
2. precondition0.02------
3. assertion0.02------
4. precondition0.03------
5. assertion---0.02---
6. precondition0.02------
7. assertion------0.03
8. precondition0.02------
9. assertion0.04---0.02
10. assertion---0.09---
11. precondition0.04------
12. assertion------0.10
13. precondition0.04------
14. assertion0.05---0.02
15. assertion------0.08
16. precondition0.04---0.03
17. assertion0.04------
18. assertion------0.05
19. precondition0.04---0.02
20. assertion0.48------
VC for test---------
split_goal_wp
  1. precondition0.02---0.01
2. precondition0.02---0.01
3. precondition0.02---0.02
4. assertion0.45------
5. precondition0.02------
6. assertion------0.02
7. assertion------0.04
8. precondition0.03------
9. assertion1.65------
10. precondition0.02------
11. assertion0.04------
12. precondition0.03------
13. assertion------0.02