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.
     (cf, https://leino.science/papers/krml233.pdf)

   For a similar data structure, see vstte12_ring_buffer.mlw
*)

use int.Int
use seq.Seq
use array.Array
use array.ToSeq

type t 'a = {
  mutable data: array 'a;
  mutable m: int;
  mutable n: int;
  ghost mutable contents: Seq.seq 'a; (* = data[m..n[ *)
}
invariant { 0 < length data }
invariant { 0 <= m <= n <= length data }
invariant { Seq.length contents = n - m }
invariant { contents == data[m..n] } (* coercion `to_seq` is inserted here *)
by { data = Array.make 1 (any 'a); m = 0; n = 0; contents = Seq.empty }

let create (x: 'a) : t 'a
  ensures { Seq.(result.contents == empty) }
=
  { data = Array.make 10 x;
    m = 0; n = 0;
    contents = Seq.empty; }

let dequeue (q: t 'a) : (r: 'a)
  requires { Seq.length q.contents > 0 }
  writes   { q.m, q.contents }
  ensures  { Seq.(old q.contents == cons r q.contents) }
=
  let r = q.data[q.m] in
  q.m <- q.m + 1;
  ghost Seq.(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  { Seq.(q.contents == snoc (old q.contents) x) }
=
  q.data[q.n] <- x;
  q.n <- q.n + 1;
  ghost Seq.(q.contents <- Seq.snoc q.contents x)