Software Engineering II (50% option only)

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

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.

Recommended book:

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