Functional Programming and Property-Based Testing

test loop

This is a mirror of the elective course 'SM2-TES: Functional Programming and Property-Based Testing' offered in the spring 2020 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 and 2019 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.

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 U82

Lecturer: Jan Midtgaard

Course material

For the OCaml introduction we will use Jason Hickey's "Introduction to Objective Caml".

Schedule

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, 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 lec08.pdf, Sergey: Growing and Shrinking Polygons for Random Testing of Computational Geometry video, slides, paper exercises
09 Program generation and race condition testing with parallel state machines lec09.pdf, Hughes: Testing the Hard Stuff and Staying Sane exercises
10 Inference rules, Curry-Howard, program generation, and compiler testing lec10.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
11 Fuzzing lec11.pdf, Sanitizers: ASan, MSan, UBSan, American Fuzzy Lop (AFL) homepage, QuickStart guide, README, technical details, libFuzzer, OSS-Fuzz exercises
12 YouTube guest lecture: Yaron Minsky - Caml Trading Minsky - Caml Trading exercises
13 Project presentations, final course evaluation, course summary, and MSc topic suggestions lec13.pdf

Running QCheck from the toplevel

Running QCheck from utop

Building a QCheck test with ocamlbuild