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

*No. of lectures:* 6

*This course is a prerequisite for the Group Project *(*Part IB*)*.*

**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.).