examples/vstte12_ring_buffer.mlw

   1
   2 (* The 2nd Verified Software Competition (VSTTE 2012)
   3    https://sites.google.com/site/vstte2012/compet
   4
   5    Problem 3:
   6    Queue data structure implemented using a ring buffer
   7
   8    Alternative solution using a model stored in a ghost field *)
   9
  10 module RingBuffer
  11
  12   use int.Int
  13   use option.Option
  14   use list.List
  15   use import list.NthLengthAppend as L
  16   use import array.Array as A
  17
  18   type buffer 'a = {
  19     mutable first: int;
  20     mutable len  : int;
  21             data : array 'a;
  22     ghost mutable sequence: list 'a;
  23   }
  24   invariant {
  25     let size = A.length data in
  26     0 <= first <  size /\
  27     0 <= len   <= size /\
  28     len = L.length sequence /\
  29     forall i: int. 0 <= i < len ->
  30       (first + i < size ->
  31          nth i sequence = Some data[first + i]) /\
  32       (0 <= first + i - size ->
  33          nth i sequence = Some data[first + i - size])
  34   }
  35   by { first = 0; len = 0; data = make 1 (any 'a); sequence = Nil }
  36
  37   (* total capacity of the buffer *)
  38   function size (b: buffer 'a) : int = A.length b.data
  39
  40   (* length = number of elements *)
  41   function length (b: buffer 'a) : int = b.len
  42
  43   (* code *)
  44
  45   let create (n: int) (dummy: 'a) : buffer 'a
  46     requires { n > 0 }
  47     ensures  { size result = n }
  48     ensures  { result.sequence = Nil }
  49   = { first = 0; len = 0; data = make n dummy; sequence = Nil }
  50
  51   let length (b: buffer 'a) : int
  52     ensures { result = length b }
  53   = b.len
  54
  55   let clear (b: buffer 'a) : unit
  56     writes  { b.len, b.sequence }
  57     ensures { length b = 0 }
  58     ensures { b.sequence = Nil }
  59   = ghost (b.sequence <- Nil);
  60     b.len <- 0
  61
  62   let push (b: buffer 'a) (x: 'a) : unit
  63     requires { length b < size b }
  64     writes   { b.data.elts, b.len, b.sequence }
  65     ensures  { length b = (old (length b)) + 1 }
  66     ensures  { b.sequence = (old b.sequence) ++ Cons x Nil }
  67   = ghost (b.sequence <- b.sequence ++ Cons x Nil);
  68     let i = b.first + b.len in
  69     let n = A.length b.data in
  70     b.data[if i >= n then i - n else i] <- x;
  71     b.len <- b.len + 1
  72
  73   let head (b: buffer 'a) : 'a
  74     requires { length b > 0 }
  75     ensures  { match b.sequence with Nil -> false | Cons x _ -> result = x end }
  76   = b.data[b.first]
  77
  78   let pop (b: buffer 'a) : 'a
  79     requires { length b > 0 }
  80     writes   { b.first, b.len, b.sequence }
  81     ensures  { length b = (old (length b)) - 1 }
  82     ensures  { match old b.sequence with
  83                | Nil -> false
  84                | Cons x l -> result = x /\ b.sequence = l end }
  85   = ghost match b.sequence with Nil -> absurd | Cons _ s -> b.sequence <- s end;
  86     let r = b.data[b.first] in
  87     b.len <- b.len - 1;
  88     let n = A.length b.data in
  89     b.first <- b.first + 1;
  90     if b.first = n then b.first <- 0;
  91     r
  92 end
  93
  94 module Harness
  95
  96   use RingBuffer
  97   use list.List
  98
  99   let harness () =
 100     let b = create 10 0 in
 101     push b 1;
 102     push b 2;
 103     push b 3;
 104     let x = pop b in assert { x = 1 };
 105     let x = pop b in assert { x = 2 };
 106     let x = pop b in assert { x = 3 };
 107     ()
 108
 109   let harness2 () =
 110     let b = create 3 0 in
 111     push b 1;
 112     assert { sequence b = Cons 1 Nil };
 113     push b 2;
 114     assert { sequence b = Cons 1 (Cons 2 Nil) };
 115     push b 3;
 116     assert { sequence b = Cons 1 (Cons 2 (Cons 3 Nil)) };
 117     let x = pop b in assert { x = 1 };
 118     assert { sequence b = Cons 2 (Cons 3 Nil) };
 119     push b 4;
 120     assert { sequence b = Cons 2 (Cons 3 (Cons 4 Nil)) };
 121     let x = pop b in assert { x = 2 };
 122     assert { sequence b = Cons 3 (Cons 4 Nil) };
 123     let x = pop b in assert { x = 3 };
 124     assert { sequence b = Cons 4 Nil };
 125     let x = pop b in assert { x = 4 };
 126     ()
 127
 128   use int.Int
 129
 130   let test (x: int) (y: int) (z: int) =
 131     let b = create 2 0 in
 132     push b x;
 133     push b y;
 134     assert { sequence b = Cons x (Cons y Nil) };
 135     let h = pop b in assert { h = x };
 136     assert { sequence b = Cons y Nil };
 137     push b z;
 138     assert { sequence b = Cons y (Cons z Nil) };
 139     let h = pop b in assert { h = y };
 140     let h = pop b in assert { h = z }
 141
 142 end
 143
 144 (** With sequences instead of lists *)
 145
 146 module RingBufferSeq
 147
 148   use int.Int
 149   use import seq.Seq as S
 150   use import array.Array as A
 151
 152   type buffer 'a = {
 153     mutable first: int;
 154     mutable len  : int;
 155             data : array 'a;
 156     ghost mutable sequence: S.seq 'a;
 157   }
 158   invariant {
 159     let size = A.length data in
 160     0 <= first <  size /\
 161     0 <= len   <= size /\
 162     len = S.length sequence /\
 163     forall i: int. 0 <= i < len ->
 164       (first + i < size ->
 165          S.get sequence i = data[first + i]) /\
 166       (0 <= first + i - size ->
 167          S.get sequence i = data[first + i - size])
 168   }
 169   by { first = 0; len = 0; data = make 1 (any 'a); sequence = S.empty }
 170
 171   (* total capacity of the buffer *)
 172   function size (b: buffer 'a) : int = A.length b.data
 173
 174   (* length = number of elements *)
 175   function length (b: buffer 'a) : int = b.len
 176
 177   (* code *)
 178
 179   let create (n: int) (dummy: 'a) : buffer 'a
 180     requires { n > 0 }
 181     ensures  { size result = n }
 182     ensures  { result.sequence = S.empty }
 183   = { first = 0; len = 0; data = make n dummy; sequence = S.empty }
 184
 185   let length (b: buffer 'a) : int
 186     ensures { result = length b }
 187   = b.len
 188
 189   let clear (b: buffer 'a) : unit
 190     writes  { b.len, b.sequence }
 191     ensures { length b = 0 }
 192     ensures { b.sequence = S.empty }
 193   = ghost (b.sequence <- S.empty);
 194     b.len <- 0
 195
 196   let push (b: buffer 'a) (x: 'a) : unit
 197     requires { length b < size b }
 198     writes   { b.data.elts, b.len, b.sequence }
 199     ensures  { length b = (old (length b)) + 1 }
 200     ensures  { b.sequence = S.snoc (old b.sequence) x }
 201   = ghost (b.sequence <- S.snoc b.sequence x);
 202     let i = b.first + b.len in
 203     let n = A.length b.data in
 204     b.data[if i >= n then i - n else i] <- x;
 205     b.len <- b.len + 1
 206
 207   let head (b: buffer 'a) : 'a
 208     requires { length b > 0 }
 209     ensures  { result = S.get b.sequence 0 }
 210   = b.data[b.first]
 211
 212   let pop (b: buffer 'a) : 'a
 213     requires { length b > 0 }
 214     writes   { b.first, b.len, b.sequence }
 215     ensures  { length b = (old (length b)) - 1 }
 216     ensures  { result = S.get (old b.sequence) 0 }
 217     ensures  { b.sequence = (old b.sequence)[1..] }
 218   = ghost (b.sequence <- b.sequence[1..]);
 219     let r = b.data[b.first] in
 220     b.len <- b.len - 1;
 221     let n = A.length b.data in
 222     b.first <- b.first + 1;
 223     if b.first = n then b.first <- 0;
 224     r
 225 end
 226
 227 module HarnessSeq
 228
 229   use seq.Seq
 230   use RingBufferSeq
 231
 232   let harness () =
 233     let b = create 10 0 in
 234     push b 1;
 235     push b 2;
 236     push b 3;
 237     let x = pop b in assert { x = 1 };
 238     let x = pop b in assert { x = 2 };
 239     let x = pop b in assert { x = 3 };
 240     ()
 241
 242   let harness2 () =
 243     let b = create 3 0 in
 244     push b 1;
 245     assert { sequence b == cons 1 empty };
 246     push b 2;
 247     assert { sequence b == cons 1 (cons 2 empty) };
 248     push b 3;
 249     assert { sequence b == cons 1 (cons 2 (cons 3 empty)) };
 250     let x = pop b in assert { x = 1 };
 251     assert { sequence b == cons 2 (cons 3 empty) };
 252     push b 4;
 253     assert { sequence b == cons 2 (cons 3 (cons 4 empty)) };
 254     let x = pop b in assert { x = 2 };
 255     assert { sequence b == cons 3 (cons 4 empty) };
 256     let x = pop b in assert { x = 3 };
 257     assert { sequence b == cons 4 empty };
 258     let x = pop b in assert { x = 4 };
 259     ()
 260
 261   use int.Int
 262
 263   let test (x: int) (y: int) (z: int) =
 264     let b = create 2 0 in
 265     push b x;
 266     push b y;
 267     assert { sequence b == cons x (cons y empty) };
 268     let h = pop b in assert { h = x };
 269     assert { sequence b == cons y empty };
 270     push b z;
 271     assert { sequence b == cons y (cons z empty) };
 272     let h = pop b in assert { h = y };
 273     let h = pop b in assert { h = z }
 274
 275 end