This computer science book is split into two parts: the first part is about the process of implementing an abstract data type and proving that your implementation is correct. There are a number of methods for doing this and the second part of the book analyses these methods and shows that fundamentally they are all instances of the same two concepts.

This book is intended for people familiar with formal methods such as VDM and Z who wish to prove that their refinements are correct, and also for logicians who are interested in the comparison of the soundness and correctness properties of these various methods and approaches. The treatment is both extensive and rigorous. It is, however, not an introductory text and the writing style is rather dry requiring a certain investment from the reader wishing to understand the underlying concepts. Practitionerswishing to increase their knowledge in this area would be better advised to read some of the introductions to VDM or Z by authors such as Jones or Woodcock and Davies instead.