Using Z. Specification, refinement, and proof Woodcock J., Davies J.

Woodcock J., Davies J.
Количество страниц: 407
Язык: Английский
Формат: PDF / RAR

Формат файла: RAR

This book contains enough material for three courses of study: a course on mathematics for software engineering, a course on formal specification, and a course on refinement. This material can be adapted in a number of ways, to support other courses or as part of a programme of self-paced learning. To make the book easier to use, we have divided it into six parts:
Introduction Chapter 1 explains the use of formal methods, and introduces the Z notation. We discuss the importance of proof and explain what makes a good specification.
Logic Chapters 2 to 4 are an introduction to mathematical logic. We explain both propositional and predicate calculus, and introduce the concepts of equality and definite description.
Relations Chapters 5 to 10 cover sets and relations. We show how to specify objects, and relationships between them, using pieces of mathematics. We show also how the mathematical logic of Chapters 2 to 4 can be used to reason about specifications.
Schemas Chapters 11 to 14 introduce the schema language. We explain how schemas can be used to structure a specification, using logical combinators, sequential composition, and promotion. We present techniques for checking for logical consistency.
Refinement Chapters 16 to 19 are concerned with refinement. We formulate a theory of refinement within the relational calculus, and extend it to cover specifications involving schemas. We then show how a concrete design may be refined to produce executable code.
Case Studies Chapter 15 and Chapters 20 to 23 contain case studies in specification and refinement. These case studies show how the Z notation can be used to produce an abstract specification, a concrete design, and a programming language implementation.
These parts can be combined to provide an appropriate introduction to using Z, whatever the background of the reader.
The material in the book has already been used in a number of taught courses, at both graduate and undergraduate levels. Examples include:
Full-time MSc in Computation (1 year).
Logic and Relations are taught as a core course; Schemas and Case Studies are taught as an optional course.
Part-time Postgraduate Diploma/MSc in Software Engineering (2 years).
Logic and Relations are taught as a single core course, Schemas as another core course, and Refinement as an optional course. Each course is delivered in a week of intensive teaching.
BA in Computer Science (3 years).
Logic and Relations are taught as part of a discrete mathematics course in the first year. Schemas are taught as part of a software engineering course in the second year.
Notice that, by omitting the development of each specification, Case Studies can be used in courses that do not cover Refinement.