Lecturer	Geraint Jones
Degrees	Schedule A — MSc in Advanced Computer Science
Term	Michaelmas Term 2013  (16 lectures)

Overview

Many programs are so complex that they can be properly understood and designed only by raising the level of abstraction at which they are analysed way beyond what is expressible in a programming language.

A specification language and its logic are the tools we need in order to give a clear specification of the intended behaviour and functionality of a program, and to design and prove correct a plan for its implementation. The language is used to express decisions about the behaviour and functionality of a program; the logic is a collection of rules which govern the way in which we can construct mathematical proofs of its properties.

The purpose of this course is to teach a methodology for the modelling and analysis of discrete systems at varying and appropriate levels of abstraction using the specification language Z. The Z notation enables a model to be expressed, and reasoned about, mathematically. Consequently, the notations, concepts and reasoning methods of mathematics taught in this course can be applied to the specification and design of programs.

The emphasis in this course is on learning to use mathematics as a tool to support communication between humans: designers and clients, designers and programmers, programmers and other programmers. Our initial presentation of the basic notations and reasoning methods will therefore be informal and intuitive -- based for the most part on case studies.

Learning outcomes

At the end of the course, students will:

• be familiar with the discrete mathematics required for Software Engineering;
• be familiar with the core of the specification language Z;
• be capable of understanding Z specifications of some real programs;
• be capable of writing a Z specification of a reasonably complex program or discrete system, at an appropriate level of abstraction;
• be capable of proving some of the consequences of the design decisions expressed in a specification.

Prerequisites

The course is intended for graduate students with some programming experience and a basic understanding of set notation and concepts.

Synopsis

• Introduction to formal specification; preview case study
• Levels of abstraction; information structures vs. data structures; systems as objects
• Propositional logic: propositions; logical connectives; deductive reasoning; laws; methods of proof
• Predicate logic: quantification; substitution; assumptions; laws
• Equality: definite description; the one-point rule; uniqueness and quantity
• Sets: membership; set comprehension; power sets; Cartesian product; types
• Definitions: declarations; abbreviations; axioms; generics
• Relations: information content; relational inverse; relational composition; closure; domain and range; relational operations; laws
• Functions: partial functions; lambda notation; overriding; finite sets
• Sequences: sequence notation; sequences as functions; structural induction; bags
• Free types: constants and constructor functions; structural induction
• Schemas: inclusion; bindings, renaming; decoration; composition
• Systems: using schemas to define state and operations
• Case studies

Syllabus

• The use of mathematical abstraction and formal methods for specifying and reasoning about programs and discrete state systems
• Data refinement and operation refinement
• The Z specification language
• Methods of reasoning about a system specification
• Case studies in specification of dynamic systems, such as a bank account or Wikipedia

Reading list

Primary text

• J M Spivey, The Z Notation: A Reference Manual, 2nd edition, Prentice-Hall, 1992 (available on the course website).

Additional reading

• J C P Woodcock and J Davies, Using Z : Specification, Refinement, and Proof, Prentice Hall, 1996.
• I Hayes, Specification Case Studies, Prentice Hall, 1993.
• M Huth and M Ryan, Logic in Computer Science : Modelling and Reasoning about Systems, Cambridge University Press, 2004.

Recommended pre-course reading

The following is recommended as pre-course reading for those unfamiliar with the standard algebraic notations used for set operations and logic.

• Seymour Lipschutz, Discrete Mathematics. Schaum's Outline Series.
  • Chapter 1 (Set Theory: up to 1.8)
  • Chapter 2 (Relations: up to 2.6)
  • Chapter 4 (Logic and Propositional Calculus)

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.