The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata

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

Topics: Array Data Structure

Tools: Why3

References: The 2nd Verified Software Competition

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

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