why3/examples/ring_buffer.mlw

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