(** This is a cleaned up implementation of the alternative model-based specification. *)
(** You can use this as a starting point for exercise 1. *)
open QCheck
module MyQueue : sig
type 'a t
val empty : unit -> 'a t
val pop : 'a t -> unit (* may throw exception *)
val top : 'a t -> 'a option
val push : 'a -> 'a t -> unit
val elements : 'a t -> 'a list
end =
struct
type 'a t = 'a Queue.t
let empty = Queue.create
let pop q = ignore (Queue.pop q)
let top q = try Some (Queue.top q)
with Queue.Empty -> None
let push = Queue.push
let elements q =
let elems = Queue.fold (fun acc e -> e::acc) [] q in
List.rev elems
end
type command =
| Push of int
| Pop
| Top
(* to_string : command -> string *)
let to_string a = match a with
| Push n -> "(Push " ^ (string_of_int n) ^ ")"
| Pop -> "Pop"
| Top -> "Top"
(* commands_to_string : command list -> string *)
let commands_to_string = Print.list to_string
(* commands : int -> command list Gen.t *)
let rec commands num rs =
Gen.oneof
([ Gen.return [];
Gen.map2 (fun i cmds -> (Push i)::cmds) Gen.int (commands (num+1));
Gen.map (fun cmds -> Top::cmds) (commands num) ]
@ if num = 0
then []
else [ Gen.map (fun cmds -> Pop::cmds) (commands (num-1)) ]) rs
let arb_cmds n =
make ~print:commands_to_string (*~shrink:(Shrink.list ~shrink:Shrink.nil)*) (commands n)
(** Model-based specification *)
(* Our model. All operations return a new queue *)
let empty_m = []
let push_m n q = (), q @ [n]
let pop_m q = (), List.tl q
let top_m q = match q with
| [] -> (None, [])
| n::_ -> (Some n, q)
(* abstract : 'a MyQueue.t -> 'a list *)
let abstract q = MyQueue.elements q
(** Alternative model-based specification *)
(* This one simultaneously interprets commands over both the implementation and the model *)
(* interps_agree : command list -> int MyQueue.t -> int list -> bool *)
let rec interps_agree cmds q m = match cmds with
| [] -> true
| (Push n)::cmds' ->
let () = MyQueue.push n q in
let (),m' = push_m n m in
abstract q = m' && interps_agree cmds' q m'
| Pop::cmds' ->
let () = MyQueue.pop q in
let (),m' = pop_m m in
abstract q = m' && interps_agree cmds' q m'
| Top::cmds' ->
let opt = MyQueue.top q in
let opt',m' = top_m m in
opt = opt' && abstract q = m && interps_agree cmds' q m'
let alt_agreement =
Test.make ~name:"alternative agreement" ~count:1000
(arb_cmds 0)
(fun cmds -> let q = MyQueue.empty () in
let m = empty_m in
abstract q = m && interps_agree cmds q m)
;;
QCheck_runner.run_tests ~verbose:true [alt_agreement]