Acknowledgements

This book is based upon our experience in teaching and using formal methods at the Programming Research Group, Oxford, and elsewhere. The courses that we teach draw their inspiration from the work of others: Jean-Raymond Abrial, Paul Gardiner, Ian Hayes, He Jifeng, Tony Hoare, Cliff Jones, Carroll Morgan, Jeff Sanders, Ib Holm Sorensen, Mike Spivey, and Bernard Sufrin.

We are grateful to many others for their help: John Axford, Rosalind Barden, Stephen Brien, Neil Brock, Tim Clement, David Cooper, Will Harwood, Jonathan Hoare, Fleur Howles, Roger Jones, Steve King, Peter Lupton, Andrew Martin, Colin O'Halloran, Steve Schneider, Roger Shaw, Jane Sinclair, Susan Stepney, Pete Verey, Geoff Winn, John Wordsworth, and Maureen York.

We are grateful also to the students who have attended our lectures over the years: at the Programming Research Group; at Royal Holloway, University of London; at the University of Reading; at the University of Klagenfurt; on industrial courses and summer schools in Europe, North America, and Africa. Their comments and suggestions are much appreciated.

The file system and save area case studies are based upon work carried out by Ian Hayes and Ib Sorensen; the better examples of simulation were suggested by Carroll Morgan and Paul Gardiner; the better examples of refinement owe much to the work of Cliff Jones. The diagrams in the introduction were supplied by the London Transport Museum.

Jackie Harbor, Helen Martin, and Derek Moseley of Prentice Hall were professional but sympathetic at every turn. The last two years would have been less enjoyable if it had not been for their good humour, gentle tolerance, and quiet efficiency.

We would also like to thank our families, without whose love and support this book could not have been completed. This book is dedicated to them.

We would like to acknowledge the significant contribution made by the following institutions and organisations to the development of the material presented in this book:

• British Telecom;
• Defence Research Agency, Malvern;
• Department of Computer Science, Reading;
• Department of Continuing Education, Oxford;
• Engineering and Physical Sciences Research Council;
• Formal Systems (Europe) Ltd;
• IBM UK Laboratories;
• Kellogg College, Oxford;
• Logica Cambridge;
• Nortel;
• Pembroke College, Oxford;
• Programming Research Group, Oxford;
• Rutherford-Appleton Laboratory.