This is a mirror of the elective course 'SM2-TES: Functional Programming and Property-Based Testing' offered in the spring 2021 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 the spring of 2018, 2019, and 2020 at SDU and in January 2016 and 2017 as 02913: Advanced Analysis Techniques at DTU Compute, the Technical University of Denmark (DTU).
This course material is posted here for the purpose of information sharing. I don't believe in password-protected course administration systems. As a scholar I (continue to) benefit from freely available online material. This is a personal contribution to uphold such an eco-system.
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: Tuesdays 12:15-16:00 (+ Fridays 12-16) online over Zoom
Lecturer: Jan Midtgaard
For the OCaml introduction we will use Jason Hickey's "Introduction to Objective Caml".
The GitHub repository for the course incl. OCaml installation instructions
QCheck: QCheck API documentation, source code
qcstm: OPAM package, GitHub repository
Source code of minimal QCheck example (also see screencasts below)
| Lecture | Topic | Material | Notes and exercises |
|---|---|---|---|
| 01 | Installation, OCaml, QCheck, BNF grammars | Hickey chap.1,2,3-3.1.1, lec01.pdf, grammar.pdf | exercises |
| 02 | Recursive functions, tuples and lists, labeled and optional arguments, testing implication properties | Hickey chap.3.1.2-3.3,4,5, lec02.pdf | exercises |
| 03 | Algebraic data types, references, records, exceptions, generator composition, observing generators | Hickey chap.6-6.4,6.6,7,8,9, lec03.pdf | exercises |
| 04 | Modules, shrinking, and model-based testing of Patricia trees | Hickey chap.11,12 (+ parts of chap.13), lec04.pdf, qc-model.pdf, Midtgaard: QuickChecking Patricia Trees | exercises |
| 05 | Model-based testing of stateful code with a state-machine framework | lec05.pdf, State-machine lecture note | exercises |
| 06 | Case study: LevelDB + code in other languages, tail-calls, function generation, more on properties | lec06.pdf, Norton: QuickCheck A Silver Bullet for testing? (QuickChecking Google's LevelDB), Wlaschin: Choosing properties for property-based testing | exercises |
| 07 | Other frameworks, case study: Volvo/AUTOSAR, project ideas + details | lec07.pdf, Hughes: Certifying your car with Erlang, Arts-al: Testing AUTOSAR software with QuickCheck | exercises |
| 08 | Case study: computational geometry, coverage, program generation | lec08.pdf, Sergey: Growing and Shrinking Polygons for Random Testing of Computational Geometry video, slides, paper | exercises |
| 09 | Inference rules, Curry-Howard, program generation, and compiler testing | lec09.pdf, Pałka-al: Testing an optimising compiler by generating random lambda terms, Wadler: Propositions as Types, Midtgaard-al: Effect-Driven QuickChecking of Compilers | exercises |
| 10 | Race condition testing with parallel state machines, Stack-Driven Program Generation of WebAssembly, Integrated shrinking | lec10.pdf, Hughes: Testing the Hard Stuff and Staying Sane, aplas20.pdf Jacob Stanley: Gens N'Roses - Appetite for Reduction | exercises |
| 11 | Sanitizers and Fuzz Testing | lec11.pdf, Sanitizers: ASan, MSan, UBSan, American Fuzzy Lop (AFL) homepage, QuickStart guide, README, technical details, libFuzzer, OSS-Fuzz | exercises |
| 12 | Project presentations, final course evaluation, course summary | lec12.pdf |
