vstte12_ring_buffer.mlw 3.85 KB
Newer Older
1 2 3 4 5

(* The 2nd Verified Software Competition (VSTTE 2012)
   https://sites.google.com/site/vstte2012/compet

   Problem 3:
6 7 8
   Queue data structure implemented using a ring buffer

   Alternative solution using a model stored in a ghost field *)
9 10 11 12

module RingBuffer

  use import int.Int
13
  use import list.NthLengthAppend as L
14
  use import array.Array
15

16
  type buffer 'a = {
17 18 19
    mutable first: int;
    mutable len  : int;
            data : array 'a;
20 21 22 23 24 25 26 27 28 29 30 31
    ghost mutable sequence: list 'a;
  }
  invariant {
    let size = Array.length self.data in
    0 <= self.first <  size /\
    0 <= self.len   <= size /\
    self.len = L.length self.sequence /\
    forall i: int. 0 <= i < self.len ->
      (self.first + i < size ->
         nth i self.sequence = Some self.data[self.first + i]) /\
      (0 <= self.first + i - size ->
         nth i self.sequence = Some self.data[self.first + i - size])
32
  }
33 34 35 36 37 38 39 40 41

  (* total capacity of the buffer *)
  function size (b: buffer 'a) : int = Array.length b.data

  (* length = number of elements *)
  function length (b: buffer 'a) : int = b.len

  (* code *)

42
  let create (n: int) (dummy: 'a) : buffer 'a
43
    requires { n > 0 }
44 45
    ensures  { size result = n }
    ensures  { result.sequence = Nil }
46
  = { first = 0; len = 0; data = make n dummy; sequence = Nil }
47

48
  let length (b: buffer 'a) : int
49 50 51
    ensures { result = length b }
  = b.len

52 53 54 55
  let clear (b: buffer 'a) : unit
    writes  { b.len, b.sequence }
    ensures { length b = 0 }
    ensures { b.sequence = Nil }
56 57
  = ghost b.sequence <- Nil;
    b.len <- 0
58

59
  let push (b: buffer 'a) (x: 'a) : unit
60
    requires { length b < size b }
61 62 63
    writes   { b.data.elts, b.len, b.sequence }
    ensures  { length b = (old (length b)) + 1 }
    ensures  { b.sequence = (old b.sequence) ++ Cons x Nil }
64 65
  = ghost b.sequence <- b.sequence ++ Cons x Nil;
    let i = b.first + b.len in
66 67 68 69
    let n = Array.length b.data in
    b.data[if i >= n then i - n else i] <- x;
    b.len <- b.len + 1

70
  let head (b: buffer 'a) : 'a
71
    requires { length b > 0 }
72
    ensures  { match b.sequence with Nil -> false | Cons x _ -> result = x end }
73
  = b.data[b.first]
74

75
  let pop (b: buffer 'a) : 'a
76
    requires { length b > 0 }
77 78 79 80 81
    writes   { b.first, b.len, b.sequence }
    ensures  { length b = (old (length b)) - 1 }
    ensures  { match old b.sequence with
               | Nil -> false
               | Cons x l -> result = x /\ b.sequence = l end }
82 83
  = ghost match b.sequence with Nil -> absurd | Cons _ s -> b.sequence <- s end;
    let r = b.data[b.first] in
84 85 86 87 88 89 90 91 92
    b.len <- b.len - 1;
    let n = Array.length b.data in
    b.first <- b.first + 1;
    if b.first = n then b.first <- 0;
    r
end

module Harness

93
  use import RingBuffer
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
  use import list.List

  let harness () =
    let b = create 10 0 in
    push b 1;
    push b 2;
    push b 3;
    let x = pop b in assert { x = 1 };
    let x = pop b in assert { x = 2 };
    let x = pop b in assert { x = 3 };
    ()

  let harness2 () =
    let b = create 3 0 in
    push b 1;
    assert { sequence b = Cons 1 Nil };
    push b 2;
    assert { sequence b = Cons 1 (Cons 2 Nil) };
    push b 3;
    assert { sequence b = Cons 1 (Cons 2 (Cons 3 Nil)) };
    let x = pop b in assert { x = 1 };
    assert { sequence b = Cons 2 (Cons 3 Nil) };
    push b 4;
    assert { sequence b = Cons 2 (Cons 3 (Cons 4 Nil)) };
    let x = pop b in assert { x = 2 };
    assert { sequence b = Cons 3 (Cons 4 Nil) };
    let x = pop b in assert { x = 3 };
    assert { sequence b = Cons 4 Nil };
    let x = pop b in assert { x = 4 };
    ()

  use import int.Int

  let test (x: int) (y: int) (z: int) =
    let b = create 2 0 in
    push b x;
    push b y;
    assert { sequence b = Cons x (Cons y Nil) };
    let h = pop b in assert { h = x };
    assert { sequence b = Cons y Nil };
    push b z;
    assert { sequence b = Cons y (Cons z Nil) };
    let h = pop b in assert { h = y };
    let h = pop b in assert { h = z }

end