# 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

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...

...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:
(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 (insertP)

Here is a somewhat mangled definition of a function for inserting a new element into a sorted list of numbers:
Write a property that says "inserting a number x into a list l
always yields a list containing x." Make sure QuickChick finds
a counterexample.

☐

#### Exercise: 2 stars (insertP2)

Translate the following claim into a Conjecture (using In for list membership): "For all numbers x and y and lists l, if y is in l then it is also in the list that results from inserting x into l" (i.e., insert preserves all the elements already in l). Make sure QuickChick finds a counterexample.
☐

# Overview

- an
*executable property*like removeP, -
*generators*for random elements of the types of the inputs to the property (here, numbers and lists of numbers), -
*printers*for converting data structures like numbers and lists to strings when reporting counterexamples, and -
*shrinkers*, which are used to minimize counterexamples.

*typeclasses*, which QuickChick uses extensively both internally and in its programmatic interface to users. This is the Typeclasses chapter.

*quickChick*, that supports larger-scale projects and mutation testing.