examples/ring_buffer.mlw

   1
   2 (** Simple queue implemented using a ring buffer
   3
   4    From
   5      Developing Verified Programs with Dafny.
   6      K. Rustan M. Leino. Tutorial notes, ICSE 2013.
   7
   8    For a similar data structure, see vstte12_ring_buffer.mlw
   9 *)
  10
  11 use int.Int
  12 use seq.Seq as S
  13 use array.Array
  14
  15 type t 'a = {
  16   mutable data: array 'a;
  17   mutable m: int;
  18   mutable n: int;
  19   ghost mutable contents: S.seq 'a; (* = data[m..n[ *)
  20 }
  21 invariant { 0 < length data }
  22 invariant { 0 <= m <= n <= length data }
  23 invariant { S.length contents = n - m }
  24 invariant { forall i. 0 <= i < m - n -> S.get contents i = data[m + i] }
  25 by { data = Array.make 1 (any 'a); m = 0; n = 0; contents = S.empty }
  26
  27 let create (x: 'a) : t 'a
  28   ensures { S.(result.contents == empty) }
  29 =
  30   { data = Array.make 10 x;
  31     m = 0; n = 0;
  32     contents = S.empty; }
  33
  34 let dequeue (q: t 'a) : (_r: 'a)
  35   requires { S.length q.contents > 0 }
  36   writes   { q.m, q.contents }
  37   ensures  { S.(q.contents == (old q.contents)[1..]) }
  38 =
  39   let r = q.data[q.m] in
  40   q.m <- q.m + 1;
  41   ghost S.(q.contents <- q.contents[1..]);
  42   r
  43
  44 let enqueue (q: t 'a) (x: 'a) : unit
  45   requires { q.n < length q.data }
  46   writes   { q.data.elts, q.n, q.contents }
  47   ensures  { S.(q.contents == snoc (old q.contents) x) }
  48 =
  49   q.data[q.n] <- x;
  50   q.n <- q.n + 1;
  51   ghost S.(q.contents <- S.snoc q.contents x)
  52