Z: An Introduction to Formal Methods

by Antoni Diller

Offers a thorough and comprehensive tutorial introduction to Z. Uses standard notation with practical exercises and clear descriptions and explanations. Contains information on how to relate Z specifications to actual program code and is enhanced to reflect the most current language standards.

Genres: Nonfiction

Paperback

First published July 27, 1994

Reviews

[Arthur Ryman · Rating 5 out of 5]

This book is a very thorough introduction to formal software specification using Z notation. It also gives a careful treatment of formal proof and the use of Floyd-Hoare logic for proving properties about programs written in a simple procedural language. The writing style is very clear and easy to follow. The topics are illustrated with simple examples and there are plenty of exercises with solutions included. The book is certainly suitable as a textbook for an introductory undergraduate course on formal methods. I would have liked to see some discussion of tool support for checking correctness and proving properties of Z specifications.