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 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
Obligations | CVC3 2.4.1 | CVC4 1.5 | CVC5 1.0.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.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 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.11.2 |
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.03 |
Theory "vstte12_ring_buffer.HarnessSeq": fully verified
Obligations | CVC4 1.5 | Z3 4.11.2 |
VC for harness | 0.18 | --- |
VC for harness2 | --- | 1.00 |
VC for test | --- | 0.25 |