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

```

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

 Obligations Alt-Ergo (0.99.1) CVC3 (2.4.1) Coq (8.6.1) Z3 (4.3.2) 1. VC for create 0.01 --- --- --- 2. VC for length 0.02 --- --- --- 3. VC for clear 0.01 --- --- --- 4. VC for push --- --- --- --- split_goal_wp 1. index in array bounds 0.01 --- --- --- 2. type invariant --- --- --- --- inline_goal 1. type invariant --- --- --- --- split_goal_wp 1. VC for push 0.02 --- --- --- 2. VC for push 0.02 --- --- --- 3. VC for push 0.02 --- --- --- 4. VC for push 0.01 --- --- --- 5. VC for push 0.03 --- --- --- 6. VC for push 0.16 --- --- --- 7. VC for push 0.08 --- --- --- 3. type invariant 0.01 --- --- --- 4. postcondition 0.02 --- --- --- 5. postcondition 0.01 --- --- --- 5. VC for head --- --- --- --- split_goal_wp 1. index in array bounds 0.02 --- --- --- 2. postcondition --- --- 0.62 --- 6. VC for pop --- --- --- --- split_goal_wp 1. unreachable point 0.00 --- --- --- 2. index in array bounds 0.02 --- --- --- 3. type invariant --- --- --- --- split_goal_wp 1. VC for pop 0.01 --- --- --- 2. VC for pop 0.02 --- --- --- 3. VC for pop 0.01 --- --- --- 4. VC for pop 0.02 0.02 --- --- 5. VC for pop 0.01 --- --- --- 6. VC for pop --- 0.06 --- --- 7. VC for pop 0.02 --- --- --- 4. postcondition 0.01 --- --- --- 5. postcondition --- --- --- --- split_goal_wp 1. VC for pop 0.01 --- --- --- 2. VC for pop --- 0.25 --- --- 3. VC for pop 0.00 --- --- --- 6. type invariant --- --- --- --- split_goal_wp 1. VC for pop 0.01 --- --- --- 2. VC for pop 0.01 --- --- --- 3. VC for pop 0.02 --- --- --- 4. VC for pop 0.01 0.02 --- --- 5. VC for pop 0.01 --- --- --- 6. VC for pop --- 0.09 --- --- 7. VC for pop --- --- --- --- 7. postcondition 0.01 --- --- --- 8. postcondition --- --- --- --- split_goal_wp 1. VC for pop 0.01 --- --- --- 2. VC for pop --- --- 0.52 --- 3. VC for pop 0.02 --- --- ---

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

 Obligations Alt-Ergo (0.99.1) CVC3 (2.4.1) 1. VC for harness --- --- split_goal_wp 1. precondition 0.01 --- 2. precondition 0.01 --- 3. precondition 0.01 0.02 4. precondition 0.02 --- 5. precondition 0.02 --- 6. assertion 0.18 --- 7. precondition 0.03 --- 8. assertion 0.25 --- 9. precondition 0.04 --- 10. assertion 0.30 --- 2. VC for harness2 --- --- split_goal_wp 1. precondition 0.00 --- 2. precondition 0.01 --- 3. assertion 0.01 --- 4. precondition 0.01 --- 5. assertion 0.08 --- 6. precondition 0.02 --- 7. assertion --- 0.04 8. precondition 0.00 --- 9. assertion 0.04 --- 10. assertion --- 0.06 11. precondition 0.02 --- 12. assertion --- 0.06 13. precondition 0.03 --- 14. assertion --- 0.06 15. assertion 0.05 --- 16. precondition 0.02 --- 17. assertion 0.08 --- 18. assertion 0.08 --- 19. precondition 0.03 --- 20. assertion 0.10 --- 3. VC for test --- --- split_goal_wp 1. precondition 0.01 --- 2. precondition 0.01 --- 3. precondition 0.02 --- 4. assertion 0.17 --- 5. precondition 0.01 --- 6. assertion 0.04 --- 7. assertion 0.02 --- 8. precondition 0.01 --- 9. assertion 0.08 --- 10. precondition 0.03 --- 11. assertion 0.05 --- 12. precondition 0.03 --- 13. assertion 0.05 ---

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

 Obligations Alt-Ergo (0.99.1) 1. VC for create 0.01 2. VC for length 0.02 3. VC for clear 0.01 4. VC for push 0.02 5. VC for head 0.02 6. VC for pop 0.03

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

 Obligations Alt-Ergo (0.99.1) Z3 (3.2) Z3 (4.3.2) 1. VC for harness --- --- 0.02 2. VC for harness2 --- --- --- split_goal_wp 1. precondition 0.01 --- --- 2. precondition 0.02 --- --- 3. assertion 0.02 --- --- 4. precondition 0.03 --- --- 5. assertion --- 0.02 --- 6. precondition 0.02 --- --- 7. assertion --- --- 0.03 8. precondition 0.02 --- --- 9. assertion 0.04 --- 0.02 10. assertion --- 0.09 --- 11. precondition 0.04 --- --- 12. assertion --- --- 0.10 13. precondition 0.04 --- --- 14. assertion 0.05 --- 0.02 15. assertion --- --- 0.08 16. precondition 0.04 --- 0.03 17. assertion 0.04 --- --- 18. assertion --- --- 0.05 19. precondition 0.04 --- 0.02 20. assertion 0.48 --- --- 3. VC for test --- --- --- split_goal_wp 1. precondition 0.02 --- 0.01 2. precondition 0.02 --- 0.01 3. precondition 0.02 --- 0.02 4. assertion 0.45 --- --- 5. precondition 0.02 --- --- 6. assertion --- --- 0.02 7. assertion --- --- 0.04 8. precondition 0.03 --- --- 9. assertion 1.93 --- --- 10. precondition 0.02 --- --- 11. assertion 0.04 --- --- 12. precondition 0.03 --- --- 13. assertion --- --- 0.02