Software Engineering II

Lecturer: Dr L.C. Paulson (lcp@cl.cam.ac.uk)

No. of lectures: 6

Aims

The course has two distinct aims. First, it will present a variety of simple methods that an individual can use to write programs systematically. These will include top-down program refinement, systematic design of loops, and a variety of suggestions for improving program reliability. Second, it will survey formal methods for software engineering, introducing the Z specification language and program correctness proofs.

Lectures

• Program refinement. Top-down design of code. Example: printing a table of squares. Dealing with errors.

• Loop design. The basic while loop. The invariant. Defensive programming. Sentinels. Example of loop design.

• Fault avoidance, or preventing bugs. Slogans: Keep It Simple; Check Everything. The pursuit of efficiency; re-inventing the wheel. Compiler warnings and assert statements.

• Formal methods in software development. Formal specifications and specification languages. Some case studies using formal methods.

• Introduction to the Z specification language. Schemas. The state space: inspecting it, changing it. Spivey's Birthday Book.

• Proving ML programs correct. Structural induction on lists. Associativity of the append function. Generalising the induction formula. Example: equivalence of two functions for list reversal.

Objectives

At the end of the course, students should

• understand how to use top-down design, recognising its advantages and drawbacks

• be able to describe the main techniques for fault avoidance

• be able to state what formal methods can and cannot do

• be able to write and understand very simple Z schemas

• be able to show that a loop is correct by reasoning about its invariant

• be able to prove simple theorems about functional programs using induction

Recommended book

Paulson, L.C. (1996). ML for the Working Programmer. Cambridge University Press (2nd ed.).