Publisted by Springer-Verlag London in 2008
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
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
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:
Part II, Material Truth, emphasizes using logic to reason correctly about software execution.
It explains how to use truth tables 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 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:
- 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
- Trace execution of programs forwards and backwards,
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
- 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,
- Test problem specifications for logical equivalence and implication, and
- Reduce redundancy in specifications.