Recent years have seen the development of powerful tools for verifying hardware and software systems, as companies worldwide realise the need for improved means of validating their products. There is increasing demand for training in basic methods in formal reasoning so that students can gain proficiency in logic-based verification methods. The second edition of this successful textbook addresses both those requirements, by continuing to provide a clear introduction to formal reasoning which is both relevant to the needs of modern computer science and rigorous enough for practical application. Improvements to the first edition have been made throughout, with extra and expanded sections on SAT solvers, existential/universal second-order logic, micro-models, programming by contract and total correctness. The coverage of model-checking has been substantially updated. Further exercises have been added. Internet support for the book includes worked solutions for all exercises for teachers, and model solutions to some exercises for students.

近年来，随着世界各地的公司意识到需要改进验证其产品的手段，用于验证硬件和软件系统的强大工具也得到了发展。人们对形式推理基本方法的培训需求越来越大，以便学生能够熟练掌握基于逻辑的验证方法。这本成功的教科书的第二版满足了这两方面的要求，它继续提供了对形式推理的清晰介绍，既与现代计算机科学的需求相关，又足够严谨，适合实际应用。对第一版进行了全面的改进，增加了关于SAT求解器、存在/普遍二阶逻辑、微模型、契约编程和完全正确性的章节。对模型检查的覆盖面进行了大幅更新。还增加了更多的练习。本书的互联网支持包括为教师提供的所有练习的工作解决方案，以及为学生提供的一些练习的模型解决方案。