## 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.

Tools: Why3

References: The 2nd Verified Software Competition

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

```(* The 2nd Verified Software Competition (VSTTE 2012)

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

```

```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

 Obligations Alt-Ergo 2.0.0 CVC3 2.4.1 CVC4 1.5 Eprover 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.21 --- --- --- 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 invariant --- 0.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 invariant --- 0.05 --- --- type invariant --- 0.06 --- --- postcondition --- --- 0.02 --- postcondition --- --- --- 0.57

## Theory "vstte12_ring_buffer.Harness": fully verified

 Obligations CVC4 1.5 VC for harness 0.12 VC for harness2 0.28 VC for test 0.12

## Theory "vstte12_ring_buffer.RingBufferSeq": fully verified

 Obligations CVC4 1.5 Z3 4.6.0 VC for buffer 0.04 --- VC for create 0.03 --- VC for length 0.01 --- VC for clear 0.06 --- VC for push 0.16 --- VC for head 0.04 --- VC for pop --- 0.06

## Theory "vstte12_ring_buffer.HarnessSeq": fully verified

 Obligations CVC4 1.5 Z3 4.6.0 VC for harness 0.18 --- VC for harness2 --- 0.85 VC for test --- 0.23