University of Oxford Logo University of OxfordSoftware Engineering - Home
On Facebook
Follow us on twitter
Linked in
Linked in
Google plus
Google plus
Stumble Upon
Stumble Upon

Specification and Design

This course shows how mathematics can be used to structure and reason about real systems. It shows how the Z notation can be used to describe complex pieces of software in a clear and comprehensible fashion. It shows how to check a set of requirements for logical consistency, and how to verify that operations are properly defined.

An essential feature of the course is the workshop, in which students get the chance to develop their own specifications under expert supervision.

Course dates

Future courses yet to be planned.


At the end of the course, students will be able to construct mathematical specifications of real systems. They will be able to check a set of requirements for consistency, and reason about the robustness of a design.


overview of the schema language; patterns and structure; declarations and predicates; schema semantics; bindings and types.
Schema operators:
mechanisms for schema combination; abstract data types; state-based specification; encapsulation of data members; composition of operations.
structuring specifications; compositionality; parallel composition of components; replication; indexing and naming; object references.
checking the consistency of specifications; calculating the applicability of operations; preconditions and data invariants; simplifying requirements.
case studies and exercises, including: file system; bounded buffer; access control; connection-based protocols.


The course assumes a working understanding of the mathematical language of Z, as taught in the Software Engineering Mathematics course. Software engineering mathematics is an ideal preparation.