Now that formal methods are seen as a necessary and beneficial theoretical tool for systems designers and programmers, this book offers a thorough and comprehensive tutorial introduction to Z taking as its starting point the practical use of this formal specification language. Case studies are used to illustrate all aspects of Z and are introduced early on in order to motivate the mathematical notations that have to be covered. Standard notation is used throughout. Many proofs are included and they are presented using the commonest format for natural deduction proofs. With exercises given and clear descriptions and explanations provided, this book is required reading for students and post-experience software engineers learning Z. Enhancements to this edition are more exercises, information on how to relate Z specifications to actual program code, and amendments so that the book is in line with the current language standards.

How many hours have you spent trying to get LATEX to do what You want? If the answer is ‘too many’, then you need LATEX Line by Line. Written for LATEX novices, this book starts from the very basics providing clear explanations and realistic examples. The book is designed to help you find solutions to specific tasks, such as indexing, setting complicated mathematics and producing simple line diagrams. It also aims to guide you through the process of creating documents as simple as letters and articles or as complex as books—all to a professional presentational quality. The glossary provides guidance on every standard command—and a few non-standard ones too. Although the book provides a comprehensive introduction to the latest version of LATEX, namely LATEX 2_ε, an appendix clearly explains the differences between LATEX 2_ε and the original version of LATEX. In this way, the book can profitably be used by people who still have the older version. Many of the examples of typesetting that are given in the book are coded as templates and are available on the accompanying Website. They can be used as recipes or skeletons which can be customized by making minor adjustments to the commands. Full explanations of how these documents have been constructed are given for those wanting to better understand the inner workings of this flexible and powerful package.