## Authors' 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 computer systems fundamentally deal with a *satisfaction relation*** **M
|= phi where M is some sort of *situation *or *model* of a system, and
phi 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 for
propositional, 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**

Chapter 1 now discusses the design, correctness, and complexity of a SAT
solver (a marking algorithm similar to Stalmarck's method for full propositional
logic.

Chapter 2 now contains basic results from model theory (Compactness Theorem
and Loewenheim-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 analyzer for specifying and exploring under-specified first-order logic
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 re-structured. It now begins with a discussion
of linear-time temporal logic; features the open-source NuSMV
model-checking 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 paradigm of verifying program
correctness.

Chapters 5 and 6 have also been revised, with many small alterations and
corrections.

Back to main index.