Ring Buffer
Simple queue implemented using a ring buffer.
Auteurs: Jean-Christophe Filliâtre
Catégories: Array Data Structure / Data Structures
Outils: Why3
see also the index (by topic, by tool, by reference, by year)
Simple queue implemented using a ring buffer
From Developing Verified Programs with Dafny. K. Rustan M. Leino. Tutorial notes, ICSE 2013.
For a similar data structure, see vstte12_ring_buffer.mlw
use int.Int use seq.Seq as S use array.Array type t 'a = { mutable data: array 'a; mutable m: int; mutable n: int; ghost mutable contents: S.seq 'a; (* = data[m..n[ *) } invariant { 0 < length data } invariant { 0 <= m <= n <= length data } invariant { S.length contents = n - m } invariant { forall i. 0 <= i < m - n -> S.get contents i = data[m + i] } by { data = Array.make 1 (any 'a); m = 0; n = 0; contents = S.empty } let create (x: 'a) : t 'a ensures { S.(result.contents == empty) } = { data = Array.make 10 x; m = 0; n = 0; contents = S.empty; } let dequeue (q: t 'a) : (_r: 'a) requires { S.length q.contents > 0 } writes { q.m, q.contents } ensures { S.(q.contents == (old q.contents)[1..]) } = let r = q.data[q.m] in q.m <- q.m + 1; ghost S.(q.contents <- q.contents[1..]); r let enqueue (q: t 'a) (x: 'a) : unit requires { q.n < length q.data } writes { q.data.elts, q.n, q.contents } ensures { S.(q.contents == snoc (old q.contents) x) } = q.data[q.n] <- x; q.n <- q.n + 1; ghost S.(q.contents <- S.snoc q.contents x)
download ZIP archive
Why3 Proof Results for Project "ring_buffer"
Theory "ring_buffer.Top": fully verified
Obligations | Alt-Ergo 2.3.0 |
VC for t | 0.01 |
VC for create | 0.03 |
VC for dequeue | 0.03 |
VC for enqueue | 0.03 |