This 1997 book is a self-contained tutorial on Z for experienced programming professionals, discussing practical ways to apply formal methods in real projects and showing how to implement them in the C programming language, through case studies in safety-critical systems and other examples from computer graphics, word processing, databases, and object-oriented programming.