Formal Program Design

The aim is to show how procedural programs can be developed rigorously from their mathematical specifications. In the first part, the emphasis is primarily on how to derive loops from invariants; this activity is called algorithm refinement.

The second part of the course deals with specification and data refinement. It shows how modules and systems can be specified abstractly, how algorithms can be developed using abstract datatypes, and how such abstract datatypes can be implemented using concrete datatypes, and that implementation formally justified.

Students may not take this course if they have previously taken either Formal Program Design I and Formal Program Design II.

At the end of the course students are expected to:

• Be able to specify modules, and in particular programs, abstractly
• Understand the criteria for algorithm refinement
• Be able to specify modules and systems, abstractly
• Perform rigorous and formal derivations of efficient programs from their abstract specifications
• Understand the criteria for algorithm refinement and data refinement

• Use of assertions to reason about program behaviour. Predicate notation as a language of assertions. Postconditions and preconditions, wp, specification statements. [1]
• The language of guarded commands; assignment, sequencing, repetition and alternation. Constants, blocks and arrays.Proof rules for program constructs. [2]
• Basic techniques for finding invariants: replacing a constant by a variable. Up loops and down loops. Simple examples, such as div/mod. [2]
• Arrays. Rules for reasoning about distributed operations:empty range and one-point rules; range split. Linear and binary search. [2]
• Further examples of small programming problems. Segment problems (perhaps not maximum segment sum). [2]
• Tail invariants and their uses. Fast exponentiation and modulus computation.[2]
• Longest up-sequence.[1]
• Quicksort or heapsort as examples of efficient sortingalgorithms derived rigorously.[1]
• Specification of systems: modules, abstract datatypes, specification statements.[1]
• Data refinement: datatype invariants and coupling invariants;simple examples.[2]
• Procedures and parameters; call by value and result; recursion and recursion elimination. [2]
• Datatypes using pointers: linked lists and binary trees; pointer algorithms.[3]
• More examples of data refinement: hash tables, binary search trees. [3]

• The language of guarded commands for expressing programs.
• Assertions, invariants, and variant functions.
• Strategies for finding invariants; head and tail invariants.
• General programming techniques for developing efficient programs.
• Examples from sorting and searching problems.
• Procedures and parameter passing.
• Recursion in procedural programs.
• Modules and encapsulation.
• Data refinement.
• Example refinements, including use of hashing and tree structures.
• Pointer algorithms and their development.
• Specification using modules, abstract data types and their operations.

• Anne Kaldewaij, Programming: the derivation of algorithms, Prentice-Hall International, 1990.
• C C Morgan, Programming from specifications,� Prentice-Hall International. (Out of print, but available on web).http://www.comlab.ox.ac.uk/oucl/publications/books/PfS/
• T H Cormen, C E Leiserson, C Stein and R L Rivest, Introduction to algorithms, 2001.