mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
276 lines
7.4 KiB
Plaintext
276 lines
7.4 KiB
Plaintext
|
|
(* 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 int.Int
|
|
use option.Option
|
|
use list.List
|
|
use import list.NthLengthAppend as L
|
|
use import array.Array as A
|
|
|
|
type buffer 'a = {
|
|
mutable first: int;
|
|
mutable len : int;
|
|
data : array 'a;
|
|
ghost mutable sequence: list 'a;
|
|
}
|
|
invariant {
|
|
let size = A.length data in
|
|
0 <= first < size /\
|
|
0 <= len <= size /\
|
|
len = L.length sequence /\
|
|
forall i: int. 0 <= i < len ->
|
|
(first + i < size ->
|
|
nth i sequence = Some data[first + i]) /\
|
|
(0 <= first + i - size ->
|
|
nth i sequence = Some data[first + i - size])
|
|
}
|
|
by { first = 0; len = 0; data = make 1 (any 'a); sequence = Nil }
|
|
|
|
(* total capacity of the buffer *)
|
|
function size (b: buffer 'a) : int = A.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 = A.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 = A.length b.data in
|
|
b.first <- b.first + 1;
|
|
if b.first = n then b.first <- 0;
|
|
r
|
|
end
|
|
|
|
module Harness
|
|
|
|
use RingBuffer
|
|
use 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 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 int.Int
|
|
use import seq.Seq as S
|
|
use import array.Array as A
|
|
|
|
type buffer 'a = {
|
|
mutable first: int;
|
|
mutable len : int;
|
|
data : array 'a;
|
|
ghost mutable sequence: S.seq 'a;
|
|
}
|
|
invariant {
|
|
let size = A.length data in
|
|
0 <= first < size /\
|
|
0 <= len <= size /\
|
|
len = S.length sequence /\
|
|
forall i: int. 0 <= i < len ->
|
|
(first + i < size ->
|
|
S.get sequence i = data[first + i]) /\
|
|
(0 <= first + i - size ->
|
|
S.get sequence i = data[first + i - size])
|
|
}
|
|
by { first = 0; len = 0; data = make 1 (any 'a); sequence = S.empty }
|
|
|
|
(* total capacity of the buffer *)
|
|
function size (b: buffer 'a) : int = A.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 = A.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 = A.length b.data in
|
|
b.first <- b.first + 1;
|
|
if b.first = n then b.first <- 0;
|
|
r
|
|
end
|
|
|
|
module HarnessSeq
|
|
|
|
use seq.Seq
|
|
use 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 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
|