Functional Programming and Property-Based Testing

This is a mirror of the elective course 'SM2-TES: Functional Programming and Property-Based Testing' offered in the spring 2018 on the MSc education in Software Engineering at the Maersk Mc-Kinney Moller Institute, University of Southern Denmark.

Previous versions of the course were given in January 2016 and 2017 as 02913: Advanced Analysis Techniques at DTU Compute, the Technical University of Denmark (DTU).

Course content

The course is two-fold.

On the one hand it introduces functional programming: Immutable data, algebraic datatypes, pattern matching, recursion, functions as first-class values, proper tail calls, type-directed programming and functional programming patterns.

On the other hand it introduces 'Property-based testing' (QuickCheck) (next generation automated testing) expressed within the functional programming context: Generators, properties, shrinking, statistics of generators, type-directed testing, testing of imperative code while touching upon a number of more general testing concepts as debugging, unit-testing, corner cases, blackbox and whitebox testing and fuzzing.

Finally the course covers a number of real-world case studies of property-based testing, e.g., an automated test of the AUTOSAR specification for Volvo.


The course consists of a mix of lectures and practical exercises, held in weekly 4-hour sessions.

Lectures: Mondays 12:15-16:00 in room U24A

Lecturer: Jan Midtgaard

Course material

For the OCaml introduction we will use Jason Hickey's "Introduction to Objective Caml".
An English/Danish dictionary of commonly used terms
OCaml installation instructions
Source code of minimal QCheck example, also see screencasts below
QCheck API documentation
QCheck source code


Lecture Topic Material Notes and exercises
01 Intro - OCaml, QuickCheck, BNF grammars Hickey chap.1,2,3-3.1.1
02 Recursive functions, tuples and lists,
labeled and optional arguments, testing implication properties.
Hickey chap.3.1.2-3.3,4,5
lec02.pdf Makefile
03 Algebraic data types + generators, observing generators,
exceptions + testing exception-throwing code
Hickey chap.6-6.4,6.6,7,8,9
lec03.pdf Makefile
Red-Black trees on Wikipedia
Okasaki: Red-Black Trees in a Functional Setting
04 OCaml's module system, shrinking,
model-based testing of Patricia trees
Hickey, chap.11,12 (+ parts of chap.13)
qc-model.pdf Makefile
Code for Patricia tree model
Midtgaard: QuickChecking Patricia Trees
05 Guest lecture: Jeppe Pedersen, MIR
stateful data structures (stateful testing postponed)
lec05.pdf Makefile
06 Stateful testing with algebraic and model-based specifications lec06.pdf Makefile
Claessen-Hughes: QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs
Claessen-Hughes: Testing Monadic Code with QuickCheck
The queue implementation from the standard library
07 More on properties
Case studies: computational geometry + LevelDB
Sergey: Growing and Shrinking Polygons for Random Testing of Computational Geometry video, slides, paper
Wlaschin: Choosing properties for property-based testing
Norton: QuickCheck A Silver Bullet for testing? (QuickChecking Google's LevelDB)
Looking for ports?
Wikipedia's entry for QuickCheck
An overview of selected ports
Ask Google for ports
08 Other framework, project details,
Case study: AUTOSAR/Volvo
Hughes: Certifying your car with Erlang
The C POSIX standard
09 Case study: program generation and compiler testing lec09.pdf
Wadler: Propositions as Types
Pałka-al: Testing an optimising compiler by generating random lambda terms
Midtgaard-al: Effect-Driven QuickChecking of Compilers paper, code, Docker image
10 Fuzzing lec10.pdf
Sanitizers: ASan, MSan, UBSan
American Fuzzy Lop (AFL), libFuzzer, OSS-Fuzz
AFL: QuickStart guide, README, technical details
11 Preliminary project presentations + course evaluation

Running QCheck from the toplevel

Building a QCheck test with ocamlbuild