(* The 2nd Verified Software Competition (VSTTE 2012) https://sites.google.com/site/vstte2012/compet Problem 3: Queue data structure implemented using a ring buffer Alternative solution using a model stored in a ghost field *) module RingBuffer use import int.Int use import option.Option use import list.List use import list.NthLengthAppend as L use import array.Array type buffer 'a = { mutable first: int; mutable len : int; data : array 'a; 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]) } (* 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 *) let create (n: int) (dummy: 'a) : buffer 'a requires { n > 0 } ensures { size result = n } ensures { result.sequence = Nil } = { first = 0; len = 0; data = make n dummy; sequence = Nil } let length (b: buffer 'a) : int ensures { result = length b } = b.len let clear (b: buffer 'a) : unit writes { b.len, b.sequence } ensures { length b = 0 } ensures { b.sequence = Nil } = ghost b.sequence <- Nil; b.len <- 0 let push (b: buffer 'a) (x: 'a) : unit requires { length b < size b } writes { b.data.elts, b.len, b.sequence } ensures { length b = (old (length b)) + 1 } ensures { b.sequence = (old b.sequence) ++ Cons x Nil } = ghost b.sequence <- b.sequence ++ Cons x Nil; let i = b.first + b.len in let n = Array.length b.data in b.data[if i >= n then i - n else i] <- x; b.len <- b.len + 1 let head (b: buffer 'a) : 'a requires { length b > 0 } ensures { match b.sequence with Nil -> false | Cons x _ -> result = x end } = b.data[b.first] let pop (b: buffer 'a) : 'a requires { length b > 0 } 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 } = ghost match b.sequence with Nil -> absurd | Cons _ s -> b.sequence <- s end; let r = b.data[b.first] in 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 use import RingBuffer 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 (** With sequences instead of lists *) module RingBufferSeq use import int.Int use import seq.Seq as S use import array.Array type buffer 'a = { mutable first: int; mutable len : int; data : array 'a; ghost mutable sequence: S.seq 'a; } invariant { let size = Array.length self.data in 0 <= self.first < size /\ 0 <= self.len <= size /\ self.len = S.length self.sequence /\ forall i: int. 0 <= i < self.len -> (self.first + i < size -> S.get self.sequence i = self.data[self.first + i]) /\ (0 <= self.first + i - size -> S.get self.sequence i = self.data[self.first + i - size]) } (* 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 *) let create (n: int) (dummy: 'a) : buffer 'a requires { n > 0 } ensures { size result = n } ensures { result.sequence = S.empty } = { first = 0; len = 0; data = make n dummy; sequence = S.empty } let length (b: buffer 'a) : int ensures { result = length b } = b.len let clear (b: buffer 'a) : unit writes { b.len, b.sequence } ensures { length b = 0 } ensures { b.sequence = S.empty } = ghost b.sequence <- S.empty; b.len <- 0 let push (b: buffer 'a) (x: 'a) : unit requires { length b < size b } writes { b.data.elts, b.len, b.sequence } ensures { length b = (old (length b)) + 1 } ensures { b.sequence = S.snoc (old b.sequence) x } = ghost b.sequence <- S.snoc b.sequence x; let i = b.first + b.len in let n = Array.length b.data in b.data[if i >= n then i - n else i] <- x; b.len <- b.len + 1 let head (b: buffer 'a) : 'a requires { length b > 0 } ensures { result = S.get b.sequence 0 } = b.data[b.first] let pop (b: buffer 'a) : 'a requires { length b > 0 } writes { b.first, b.len, b.sequence } ensures { length b = (old (length b)) - 1 } ensures { result = S.get (old b.sequence) 0 } ensures { b.sequence = (old b.sequence)[1 ..] } = ghost b.sequence <- b.sequence[1 ..]; let r = b.data[b.first] in 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 HarnessSeq use import seq.Seq use import RingBufferSeq 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 empty }; push b 2; assert { sequence b == cons 1 (cons 2 empty) }; push b 3; assert { sequence b == cons 1 (cons 2 (cons 3 empty)) }; let x = pop b in assert { x = 1 }; assert { sequence b == cons 2 (cons 3 empty) }; push b 4; assert { sequence b == cons 2 (cons 3 (cons 4 empty)) }; let x = pop b in assert { x = 2 }; assert { sequence b == cons 3 (cons 4 empty) }; let x = pop b in assert { x = 3 }; assert { sequence b == cons 4 empty }; 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 empty) }; let h = pop b in assert { h = x }; assert { sequence b == cons y empty }; push b z; assert { sequence b == cons y (cons z empty) }; let h = pop b in assert { h = y }; let h = pop b in assert { h = z } end