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).
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
For the OCaml introduction we will use Jason
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||
|02||Recursive functions, tuples and lists,
labeled and optional arguments, testing implication properties.
|03||Algebraic data types + generators, observing generators,
exceptions + testing exception-throwing code
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)|
Code for Patricia tree model
Midtgaard: QuickChecking Patricia Trees
|05||Guest lecture: Jeppe Pedersen, MIR
stateful data structures (stateful testing postponed)
|06||Stateful testing with algebraic and model-based specifications||
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||
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
Sanitizers: ASan, MSan, UBSan
American Fuzzy Lop (AFL), libFuzzer, OSS-Fuzz
AFL: QuickStart guide, README, technical details
|11||Preliminary project presentations + course evaluation|