Formal Specification and Documentation using Z: A Case Study Approach

Presents a pragmatic view of the use of formal methods, that it can still be beneficial (and is much more cost effective in general) than attempting proofs in many cases.

**Tag(s):**
Formal Methods

**Publication date**: 01 Feb 1996

**ISBN-10**:
1850322309

**ISBN-13**:
9781850322306

**Paperback**:
315 pages

**Views**: 22,783

Formal Specification and Documentation using Z: A Case Study Approach

Presents a pragmatic view of the use of formal methods, that it can still be beneficial (and is much more cost effective in general) than attempting proofs in many cases.

:santagrin: This book was suggested by jpbowen

Book excerpts:

Formal methods are becoming more accepted in both academia and industry as one possible way in which to help improve the quality of both software and hardware systems. It should be remembered however that they are not a panacea, but rather one more weapon in the armoury against making design mistakes. Thus one should not expect too much from formal methods, but rather use them to advantage where appropriate.

This book presents an even more pragmatic view of the use of formal methods than that held by some academics: that is that formal specification alone can still be beneficial (and is much more cost effective in general) than attempting proofs in many cases. While the cost of proving a system correct may be justified in safety-critical systems where lives are at risk, many systems are less critical, but could still benefit from formalization earlier on in the design process than is normally the case in much industrial practice.

This book presents the use of one notation in the accumulation of available mathematical techniques to help ensure the correctness of computer-based systems, namely the Z notation (pronounced 'zed'), intended for the specification of such systems. The formal notation Z is based on set theory and predicate calculus, and has been developed at the Oxford University Computing Laboratory since the late 1970?s.

The use of a formal notation early on in the design process helps to remove many errors that would not otherwise be discovered until a later stage. The book includes specification of a number of digital systems in a variety of areas to help demonstrate the scope of the notation. Most of the specifications are of real systems that have been built, either commercially or experimentally. It is hoped that the variety of examples in this book will encourage more developers to attempt to specify their systems in a more formal manner before they attempt the development or programming stage.

It is hoped that the specifications presented here will help students and industrial practitioners alike to produce better specifications of their designs, be they large or small. Even if no proofs or refinement of a system are attempted, mere formalization early on in the design process will help to clarify a designer?s thoughts (especially when undertaken as part of a team) and remove many errors before they become implemented, and therefore much more difficult and expensive to rectify.

Book excerpts:

Formal methods are becoming more accepted in both academia and industry as one possible way in which to help improve the quality of both software and hardware systems. It should be remembered however that they are not a panacea, but rather one more weapon in the armoury against making design mistakes. Thus one should not expect too much from formal methods, but rather use them to advantage where appropriate.

This book presents an even more pragmatic view of the use of formal methods than that held by some academics: that is that formal specification alone can still be beneficial (and is much more cost effective in general) than attempting proofs in many cases. While the cost of proving a system correct may be justified in safety-critical systems where lives are at risk, many systems are less critical, but could still benefit from formalization earlier on in the design process than is normally the case in much industrial practice.

This book presents the use of one notation in the accumulation of available mathematical techniques to help ensure the correctness of computer-based systems, namely the Z notation (pronounced 'zed'), intended for the specification of such systems. The formal notation Z is based on set theory and predicate calculus, and has been developed at the Oxford University Computing Laboratory since the late 1970?s.

The use of a formal notation early on in the design process helps to remove many errors that would not otherwise be discovered until a later stage. The book includes specification of a number of digital systems in a variety of areas to help demonstrate the scope of the notation. Most of the specifications are of real systems that have been built, either commercially or experimentally. It is hoped that the variety of examples in this book will encourage more developers to attempt to specify their systems in a more formal manner before they attempt the development or programming stage.

It is hoped that the specifications presented here will help students and industrial practitioners alike to produce better specifications of their designs, be they large or small. Even if no proofs or refinement of a system are attempted, mere formalization early on in the design process will help to clarify a designer?s thoughts (especially when undertaken as part of a team) and remove many errors before they become implemented, and therefore much more difficult and expensive to rectify.

Tweet

About The Author(s)

Jonathan Bowen, FBCS FRSA, is Chairman of Museophile Limited (founded in 2002) and an Emeritus Professor at London South Bank University, where he established and headed the Centre for Applied Formal Methods in 2000.

He has been involved with the field of computing in both industry (including Marconi Instruments, Logica, Silicon Graphics Inc., and Praxis) and academia since 1977. His interests have ranged from formal methods, safety-critical systems, the Z notation, provably correct systems, rapid prototyping using logic programming, decompilation, hardware compilation, software/hardware co-design, linking semantics, and software testing, to the history of computing, on-line museums, and virtual communities.

He has been involved with the field of computing in both industry (including Marconi Instruments, Logica, Silicon Graphics Inc., and Praxis) and academia since 1977. His interests have ranged from formal methods, safety-critical systems, the Z notation, provably correct systems, rapid prototyping using logic programming, decompilation, hardware compilation, software/hardware co-design, linking semantics, and software testing, to the history of computing, on-line museums, and virtual communities.

Book Categories

Computer Science
Introduction to Computer Science
Introduction to Computer Programming
Algorithms and Data Structures
Artificial Intelligence
Computer Vision
Machine Learning
Neural Networks
Game Development and Multimedia
Data Communication and Networks
Coding Theory
Computer Security
Information Security
Cryptography
Information Theory
Computer Organization and Architecture
Operating Systems
Image Processing
Parallel Computing
Concurrent Programming
Relational Database
Document-oriented Database
Data Mining
Big Data
Data Science
Digital Libraries
Compiler Design and Construction
Functional Programming
Logic Programming
Object Oriented Programming
Formal Methods
Software Engineering
Agile Software Development
Information Systems
Geographic Information System (GIS)

Mathematics
Mathematics
Algebra
Abstract Algebra
Linear Algebra
Number Theory
Numerical Methods
Precalculus
Calculus
Differential Equations
Category Theory
Proofs
Discrete Mathematics
Theory of Computation
Graph Theory
Real Analysis
Complex Analysis
Probability
Statistics
Game Theory
Queueing Theory
Operations Research
Computer Aided Mathematics

Supporting Fields
Web Design and Development
Mobile App Design and Development
System Administration
Cloud Computing
Electric Circuits
Embedded System
Signal Processing
Integration and Automation
Network Science
Project Management

Operating System
Programming/Scripting
Ada
Assembly
C / C++
Common Lisp
Forth
Java
JavaScript
Lua
Microsoft .NET
Rexx
Perl
PHP
Python
R
Rebol
Ruby
Scheme
Tcl/Tk

Miscellaneous
Sponsors