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.

Practicalities

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

Schedule

Lecture Topic Material Notes and exercises
01 Intro - OCaml, QuickCheck, BNF grammars Hickey chap.1,2,3-3.1.1
lec01.pdf
grammar.pdf
exercises01.txt
02 Recursive functions, tuples and lists,
labeled and optional arguments, testing implication properties.
Hickey chap.3.1.2-3.3,4,5
lec02.pdf
lec02.ml Makefile
exercises02.txt
03 Algebraic data types + generators, observing generators,
exceptions + testing exception-throwing code
Hickey chap.6-6.4,6.6,7,8,9
lec03.pdf
lec03.ml Makefile
Red-Black trees on Wikipedia
Okasaki: Red-Black Trees in a Functional Setting
exercises03.txt
04 OCaml's module system, shrinking,
model-based testing of Patricia trees
Hickey, chap.11,12 (+ parts of chap.13)
lec04.pdf
qc-model.pdf
lec04.ml Makefile
Code for Patricia tree model
Midtgaard: QuickChecking Patricia Trees
exercises04.txt
05 Guest lecture: Jeppe Pedersen, MIR
stateful data structures (stateful testing postponed)
lec05.pdf
lec05.ml Makefile
exercises05.txt
06 Stateful testing with algebraic and model-based specifications lec06.pdf
lec06.ml 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
exercises06.txt
exercises1.ml
07 More on properties
Case studies: computational geometry + LevelDB
lec07.pdf
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
exercises07.txt
08 Other framework, project details,
Case study: AUTOSAR/Volvo
lec08.pdf
Hughes: Certifying your car with Erlang
The C POSIX standard
exercises08.txt
09 Case study: program generation and compiler testing lec09.pdf
icfp17-slides.pdf
lec09.zip
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
exercises09.txt
10 Fuzzing lec10.pdf
examples.zip
Sanitizers: ASan, MSan, UBSan
American Fuzzy Lop (AFL), libFuzzer, OSS-Fuzz
AFL: QuickStart guide, README, technical details
exercises10.txt
11 Preliminary project presentations + course evaluation

Running QCheck from the toplevel

Building a QCheck test with ocamlbuild