Next: Easter Term 2002: Part
Up: Lent Term 2002: Part
Previous: Software Engineering I (50%
  Contents
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.).
Next: Easter Term 2002: Part
Up: Lent Term 2002: Part
Previous: Software Engineering I (50%
  Contents
Christine Northeast
Tue Sep 4 09:34:31 BST 2001