Software Specification and Testing 2016

Software testing consist of checking whether a given system meets some prior specification. Without knowing which specifications a system should meet it is impossible to test the system. An informal description of demands is not enough for this. The specification has to be (more or less) formal.

This is the reason why we start the course with a training in writing specifications in the language of predicate logic.

Actual code can be tested, given a formal specification, with the help of a random test generator. We will illustrate this test method for a number of example programs written in the functional programming language Haskell.

We assume you all have managed to install a working Haskell system on your laptop. The easiest way to get a working system is by downloading Stack or the Haskell Platform from here.

Stack is a tool for Haskell project development that offers a functional approach to package management in Haskell. See here.

Teaching Staff

  1. Jan van Eijck (lectures, workshop sessions).

  2. Kai Li (workshop sessions)

  3. Malvin Gattinger (workshop sessions)

  4. Ana Oprescu (homework assessment, computer lab supervision)

  5. Bert Lisser (homework assessment, computer lab supervision)

Dates

Sept 7 -- Oct 26, 2016

For details of the schedule, consult datanose

Set-up

The course consists of three components:

  1. Lectures: every Wednesday, 9.00 - 10.45

  2. Workshops using pen, paper, brains: every Wednesday, 11.00 -- 12.45.

  3. Computer Lab (using your own laptop): Wednesdays after 13.00 and Thursday throughout the day.

Note: starting in the second week, each lecture will be preceded by a lab feedback session conducted by Ana (Ana's Corner). Make sure to be in time for this. The feedback sessions begin at 9.00 sharp.

Final Exam

Wednesday October 26, 9--13. Two kinds of questions:

  1. Theory (questions as in the workshop sessions)

  2. Lab (problems as in the lab sessions)

Grading Algorithm

Course Goals

  1. Learn how to understand and write specifications in the language of predicate logic.

  2. Learn the basics of functional programming in Haskell.

  3. Learn how to use type-specification and abstraction to make programs more easily testable.

  4. Learn how to write formal specifications for testing Haskell code.

  5. Learn how to use random test generation for automating the test process.

  6. Learn how the functional programming paradigm relates to imperative programming.


Course contents

We will treat the following, roughly in this order

Resources

Reference


Week 1

  1. Sign up on github and send an email to Ana (see above for the address) with your github name, so we can invite you to the github repository for the course.

  2. Lecture: Informal Introduction to Haskell. Lecture notes week 1 Code for the lecture: Lecture1.hs.

  3. Workshop 1: Induction and Recursion. Here is a version with answers.

  4. Lab 1: Functional Programming and (Some) Logic. Code for lab: Lab1.hs. Lab Solutions with code.

  5. Reading: Chapters 1 and 2 of The Haskell Road. There is an opportunity for asking questions at the beginning of the next lecture.


Week 2

  1. Lecture: Use of pre- and postconditions for testing. Lecture notes week 2 Code for the lecture: Lecture2.hs.

  2. Workshop 2: reasoning with pre- and postconditions. Here is a version with answers. These slides of Kai Li give further explanation.

  3. Lab 2: triangle recognition, permutations, derangements, ROT13 encoding, IBAN validation. Code: Lab2.hs. Lab Solutions with code.

  4. Reading: Chapter 4 of The Haskell Road. There is an opportunity for asking questions at the beginning of the next lecture.


Week 3

  1. Lecture: More on Hoare Logic and Propositional Logic Lecture notes week 3 Code for the lecture: Lecture3.hs.

  2. Workshop 3: The Logic of Boolean Conditions. These slides of Kai Li give further explanation.

  3. Lab 3: Working with the logic of Boolean conditions. Code for the Lab. Lab Solutions with code.

  4. Reading: Chapter 5 of The Haskell Road. There is an opportunity for asking questions at the beginning of the next lecture.


Week 4

  1. Lecture: Functional Programming and Imperative Programming Lecture notes week 4. Code for the lecture: Lecture4.hs.

  2. Workshop 4: Working With Sets and Relations. Solutions are in Workshop4Answers.pdf.

  3. Lab 4: Working With Sets and Relations. Code for the Lab. Lab Solutions with code.

  4. Reading: Reread Chapters 4 and 5 of The Haskell Road. There is an opportunity for asking questions at the beginning of the next lecture.


Week 5

  1. Lecture: Constraint Solving with Sudokus. Lecture notes week 5. Code for the lecture: Lecture5.hs.

  2. Workshop 5: Further Exercises with Induction. Solutions are in Workshop5Answers.pdf.

  3. Lab 5: Solving Sudoku Puzzles. Code for the Lab. Lab Solutions with code.

  4. Reading: Study Chapter 7 of The Haskell Road. There is an opportunity for asking questions at the beginning of the next lecture.


Week 6

  1. Lecture: Modular Arithmetic and Cryptography Lecture notes week 6. Code for the lecture: Lecture6.hs.

  2. Workshop 6: Working with Trees. Answers. Code.

  3. Lab 6: Modular Arithmetic and Cryptography. Code for the Lab. Lab Solutions with code.

  4. Reading: left to you.


Week 7

  1. During Lecture time: Exam preparation ... Example Exam (Jan 2016).

  2. Instead of Workshop 11-13: Plenary session in Room F2.04. We discussed the answers to the example exam, with code in ResitExamAnswers.hs.


Week 8

Exam on Wednesday October 26, 9-13 am.

Please note that the exam is not at Science Park but at Roeterseilandcomplex (REC), in room C1.03.


The exam problems with worked solutions are here. And the code is in ExamOct2016Answers.hs.


Anonymised lab, exam and final results are here.