The book

Publisted by Springer-Verlag London in 2008 ISBN: 978-1-84800-081-0 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

Top of Page