Lecturer	Geraint Jones
Degrees	Schedule S1(3rd years) — Computer Science Schedule B1 — Computer Science Schedule B1(M&CS) — Mathematics and Computer Science
Term	Michaelmas Term 2011  (24 lectures)

Overview

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 and recursive procedures 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.

Learning outcomes

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

Synopsis

• 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]

Syllabus

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.

Reading list

• 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 at 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; various editions.

Feedback

Students are formally asked for feedback at the end of the course. Students can also submit feedback at any point here. Feedback received here will go to the Head of Academic Administration, and will be dealt with confidentially when being passed on further. All feedback is welcome.

Taking our courses

This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses

Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.