** Next:** Easter Term 2003: Part
** Up:** Lent Term 2003: Part
** Previous:** Software Engineering I (50%
** Contents**

##

Software Engineering II (50% option only)

*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 books**

None (comprehensive notes supplied).

** Next:** Easter Term 2003: Part
** Up:** Lent Term 2003: Part
** Previous:** Software Engineering I (50%
** Contents**
*Christine Northeast*

*Wed Sep 4 14:43:05 BST 2002
*