
Publisted by SpringerVerlag London in 2008
ISBN: 9781848000810
Link to Springer
The purpose of this book is to help software developers make better quality
longer lasting software by learning more about using elementary logic to
communicate about software, to reduce, detect, and remove software errors,
to simplify software, to verify correctness of programs, and to read software
development literature that presumes knowledge of elementary logic.
Its primary audiences are working software developers and students in any
area of computing. No previous knowledge of logic is assumed. Some knowledge
of software development is assumed. Since pseudocode is used for programming
examples, no knowledge of any particular programming language is needed.
Applications of logic to software development are emphasized throughout.
Numerous examples and solved exercises help make the book suitable for self
study and for use in college level courses. Its content has been tested in
classes and by independent readers.

Brief Contents below
Click here for detailed contents.
Click here to report errors in book
Preface
Part I Language and Logical form
 Ch01 Atomic Statements
 Ch02 Compound Statements
 Ch03 Quantified Statements
 Ch04 Expressing Arguments
 Ch05 Defining Data Structures
 Ch06 Expressing Problem Specifications
 Ch07 Expressing Program Designs
Part II Material Truth
 Ch08 Truth for Statements with At Most One Connective
 Ch09 Truth for Statements with Multiple Connectives
 Ch10 Tracing Program Execution
Part III Logical Truth
 Ch11 Truth Functional Forms
 Ch12 Truth Functional Properties of Program Designs
 Ch13 Quantified Forms
 Ch14 Logical Equivalence
 Ch15 Logical Implication and Validity
 Ch16 Rules of Inference
 Ch17 Proof
 Ch18 Algorithmic Unsolvability Proofs
 Ch19 Program Correctness Proofs
 Ch20 Above and Beyond This Book
Solutions to Selected Exercises
Sources and Bibliography
Index

Part I, Language and Logical Form, emphasizes using logic to communicate more effectively. It
explains how to find and represent the logical forms of statements and conditions and how to use
this knowledge to:
 Express and clarify problem specifications, data structure definitions, and program designs,
 Find and eliminate vagueness, ambiguity, and other defects in problem specifications,
 Translate algorithms expressed in English into pseudocode, and
 Understand software development literature that presumes knowledge of logic notation.
Part II, Material Truth, emphasizes using logic to reason correctly about software execution.
It explains how to use truth tables to:
 Understand the effect of short cut evaluation of "and" and "or" in programs,
 Calculate and use bitwise extensions of "not", "and", "or", and "xor" to make masks and
simple codes,
 Trace execution of programs forwards and backwards,
Part III, Logical Truth, emphasizes reasoning correctly about software error, simplification,
and verification. Early chapters show how to test statements for logical equivalence, logical
implication, and logical redundancy, and how to test arguments for validity and soundness.
They then describe how to apply these concepts to problem specifications. specifically how to:
 Translate program designs expressed in English into equivalent program designs expressed
as decision tables,
 Simplify decision tables,
 Analyze program designs expressed as decision tables for consistency, completeness,
and redundancy.
 Test problem specifications for logical equivalence and implication, and
 Reduce redundancy in specifications.
Later chapters explain how to use rules of inference to make proofs about software. This is
followed by a proof that no computer program can be written that solves the halting problem,
i.e. the problem of determining whether any arbitrarily selected program will halt with any arbitrarily
selected input. That bad news is followed by the good news that it is possible, though difficult,
to prove that a program is correct relative to a problem specification, without doing any testing.
Examples showing how to do this in simple cases are given. The last chapter briefly discusses
some topics not covered in the book, e.g. logic testing and quantum computing. It includes
pointers to additional sources of information about those topics
