Wiki Agenda Contact English version

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

ObligationsAlt-Ergo 2.3.0
VC for t0.01
VC for create0.03
VC for dequeue0.03
VC for enqueue0.03