LOGIC IN COMPUTER SCIENCE Modelling and Reasoning about Systems

英文原版 Preface to the second edition Our motivation for (re)writing this book One of the leitmotifs of writing the first edition of our book was the observation that most logics used in the design, specification and verification of computersystems fundamentally deal with a satisfaction relation M φ where M is some sort of situation or model of a system, and φ is a specification, a formula of that logic, expressing what should be true in situation M. At the heart of this set-up is that one can often specify and implement algorithms for computing . We developed this theme forpr opositional, first-order, temporal, modal, and program logics. Based on the encouraging feedback received from five continents we are pleased to hereby present the second edition of this text which means to preserve and improve on the original intent of the first edition. What’s new and what’s gone Chapter1 now discusses the design, correctness, and complexity of a SAT solver (a marking algorithm similar to St˚almarck’s method [SS90]) for full propositional logic. Chapter 2 now contains basic results from model theory (Compactness Theorem and L¨owenheim–Skolem Theorem); a section on the transitive closure and the expressiveness of existential and universal second-order logic; and a section on the use of the object modelling language Alloy and its analyserforsp ecifying and exploring under-specified first-orderlogic models with respect to properties written in first-order logic with transitive closure. The Alloy language is executable which makes such exploration interactive and formal. Chapter 3 has been completely restructured. It now begins with a discussion of linear-time temporal logic; features the open-source NuSMV modelchecking tool throughout; and includes a discussion on planning problems, more material on the expressiveness of temporal logics, and new modelling examples. Chapter 4 contains more material on total correctness proofs and a new section on the programming-by-contract paradig