Introduction to Specification: 2011-2012
Information
|
Lecturer |
|
|
Degrees |
|
|
Term |
Hilary Term 2012 (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)