(** * Introduction *) Set Warnings "-extraction-opaque-accessed,-extraction". Set Warnings "-notation-overridden,-parsing". From QuickChick Require Import QuickChick. Require Import List ZArith. Import ListNotations. (* ################################################################# *) (** * A First Taste of Testing *) (** Consider the following definition of a function [remove], which takes a natural number [x] and a list of nats [l] and removes [x] from the list. *) Fixpoint remove (x : nat) (l : list nat) : list nat := match l with | [] => [] | h::t => if h =? x then t else h :: remove x t end. (** One possible specification for [remove] might be this property... *) Conjecture removeP : forall x l, ~ (In x (remove x l)). (** ...which says that [x] never occurs in the result of [remove x l] for any [x] and [l]. ([Conjecture foo...] means the same as [Theorem foo... Admitted.] Formally, [foo] is treated as an axiom.) *) (** Sadly, this property is false, as we would (eventually) discover if we were to try to prove it. *) (** A different -- perhaps much more efficient -- way to discover the discrepancy between the definition and specification is to _test_ it: *) (* QuickChick removeP. *) (** (Try uncommenting and evaluating the previous line.) *) (** The [QuickChick] command takes an "executable" property (we'll see later exactly what this means) and attempts to falsify it by running it on many randomly generated inputs, resulting in output like this: 0 [0, 0] Failed! After 17 tests and 12 shrinks This means that, if we run [remove] with [x] being [0] and [l] being the two-element list containing two zeros, then the property [removeP] fails. *) (** With this example in hand, we can see that the [then] branch of [remove] fails to make a recursive call, which means that only one occurence of [x] will be deleted. The last line of the output records that it took 17 tests to identify some fault-inducing input and 12 "shrinks" to reduce it to a minimal counterexample. *) (** **** Exercise: 1 star, standard, optional (insertP) Here is a somewhat mangled definition of a function for inserting a new element into a sorted list of numbers: *) Fixpoint insert x l := match l with | [] => [x] | y::t => if y