This book describes some basic principles that allow developers of computer programs (computer scientists, software engineers, programmers) to clearly __think__ about the artifacts they deal with in their daily work: data types, programming languages, programs written in these languages that compute from given inputs wanted outputs, and programs that describe continuously executing systems. The core message is that clear thinking about programs can be expressed in a single universal language, the formal language of __logic__. Apart from its universal elegance and expressiveness, this “logical” approach to the formal modeling of and reasoning about computer programs has another advantage: due to advances in computational logic (automated theorem proving, satisfiability solving, model checking), nowadays much of this process can be supported by __software__. This book therefore accompanies its theoretical elaborations by practical demonstrations of various systems and tools that are based on respectively make use of the presented logical underpinnings. Foreword Preface Motivation Content Software Teaching and Further Study Web Page and Exercises Acknowledgments Contents Logic for Programming: A Perspective Logic and Language Logic and Mathematics Logic with Computers Logic for Computer Science Logic and Software Development Further Reading Part IThe Foundations 1 Syntax and Semantics 1.1 Abstract Syntax 1.2 Structural Induction 1.3 Semantics 1.4 Type Systems 1.5 The Semantics of Typed Languages 2 The Language of Logic 2.1 First-Order Logic 2.2 Informal Interpretation 2.3 Well-Formed Terms and Formulas 2.4 Propositional Logic 2.5 Free and Bound Variables 2.6 Formal Semantics 2.7 Validity, Logical Consequence, and Logical Equivalence 3 The Art of Reasoning 3.1 Reasoning and Proofs 3.2 Inference Rules and Proof Trees 3.3 Reasoning in First Order Logic 3.4 Reasoning by Induction 4 Building Models 4.1 Axioms and Definitions 4.2 The Theory of Sets 4.3 Products and Sums 4.4 Set-Theoretic Functions and Relations 4.5 More Type Constructions 4.6 Implicit Definitions and Function Specifications Exercises Further Reading 5 Recursion 5.1 Recursive Definitions 5.2 Primitive Recursion 5.3 Least and Greatest Fixed Points 5.4 Defining Continuous Functions 5.5 Inductive and Coinductive Relation Definitions 5.6 Rule-Oriented Inductive and Coinductive Relation Definitions 5.7 Inductive and Coinductive Function Definitions 5.8 Inductive and Coinductive Proofs Part IIThe Higher Planes 6 Abstract Data Types 6.1 Introduction 6.2 Declarations, Signatures, and Presentations 6.3 Algebras, Homomorphisms, and Abstract Data Types 6.4 Loose Specifications 6.5 Generated and Free Specifications 6.6 Cogenerated and Cofree Specifications 6.7 Specifying in the Large 6.8 Reasoning About Specifications 7 Programming Languages 7.1 Programs and Commands 7.2 A Denotational Semantics 7.3 An Operational Semantics 7.4 The Correctness of Translations 7.5 Procedures Further Reading 8 Computer Programs 8.1 Specifying Problems 8.2 Verifying Programs 8.3 Predicate Transformers and Commands as Relations 8.4 Non-abortion and Termination 8.5 Loop Invariants and Termination Measures 8.6 The Refinement of Commands 8.7 Reasoning About Procedures Further Reading 9 Concurrent Systems 9.1 Labeled Transition Systems 9.2 Modeling Shared Systems 9.3 Modeling Distributed Systems 9.4 Specifying System Properties 9.5 Verifying Invariance 9.6 Verifying Response 9.7 The Refinement of Systems References Index
