Introduction to Specification

Aims

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

A specification language and its logic are the intellectual 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 behaviour and functionality of a program; the logic is a collection of rules which govern the way in which we can construct credible and understandable proofs of its properties.

This course introduces the specification language Z. Together with its companion course ``System Design and Refinement'' and the module ``Formal Program Design'' it is intended to show you how to use the notations, concepts and reasoning methods of mathematics in the specification, design and detailed implementation 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.

The course is intended for graduate students with a little experience in programming and a rudimentary (or better) understanding of the the very simplest ideas and notations of set theory.

Learning Outcomes

At the end of the course, students will:

• 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 at an appropriate level of abstraction.
• be capable of proving some of the consequences of the design decisions expressed in a specification.