Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

Having nothing, nothing can he lose. -- William Shakespeare, "Henry VI"

rocksolid / Programming / Property Based Testing

o Property Based TestingAnonUser

Subject: Property Based Testing
From: AnonUser
Newsgroups: rocksolid.programming
Organization: RetroBBS
Date: Mon, 18 Nov 2019 12:28 UTC
From: (AnonUser)
Newsgroups: rocksolid.programming
Subject: Property Based Testing
Date: Mon, 18 Nov 2019 12:28:58 +0000
Organization: RetroBBS
Message-ID: <2b1854a8e6d9359aa1c7a09af559c8d7$>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Info:; posting-host="localhost:";
logging-data="15033"; mail-complaints-to=""
User-Agent: rslight (
To: rocksolid.programming
X-Comment-To: rocksolid.programming
X-FTN-PID: Synchronet 3.17a-Linux Dec 29 2018 GCC 6.3.0
X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on
X-Rslight-Site: $2y$10$UVIPP3GQVTWG/oyromg67.0GN70gVMwiN/P1iWbvTxUnq/18rXNjK
X-Gateway: [Synchronet 3.17a-Linux NewsLink 1.110]
View all headers
  To: rocksolid.programming
Title: Property Based Testing

While formal verification is the most reliable you can get, there also exists
property based testing which comes very close to it and it's easier and faster
to implement.

There's a paper on how the Haskell containers library was formally verified in
Coq (a proof assistant) by converting the Haskell code to Coq using hs-to-coq.
They verified that the containers library had _zero_ bugs in it and it is
likely due to them using property based tests for the library. I guess it being
written in Haskell also has a huge part in it being bug free.

verified containers package:
talk for the paper:

In short, property based testing means that you have a function and you verify
that it has specific properties. The most popular example is a sort function.

A sort function _must_ have the following properties:
* it may not change the length of the resulting list
* the resulting list must have each element the same amount of times pre and
post sort
* sorting a list twice must equal sorting the list once
* each consecutive value in a list must be greater or equal to the previous
value (ascending)

These properties are in a way formal proofs of a sort function.

QuickCheck is such a library that makes property based testing really easy. It
randomly generates input for your functions and finds the (minimal) examples
where your function doesn't satisfy those properties. If you need more
encouragement that property based testing is awesome, then check out the
computerphile video on "Code Checking Automation" on Youtube. John Huges helped
develop the Haskell language and also created QuickCheck.


It is also possible to use property based testing on state machines to ensure
that invalid states can not be reached.
Posted on RetroBBS


rocksolid light 0.8.3