Indeholder "Edsger W. Dijkstra: Forword", "Preface", "Part 0. Why Use Logic? Why Prove Programs Correct?", "Part I. Propositions and Predicates", "Chapter 1. Propositions", " 1.1. Fully Parenthesized Propositions", " 1.2. Evaluation of Constant Propositions", " 1.3. Evaluation of Propositions in a State", " 1.4. Precedence Rules for Operators", " 1.5. Tautologies", " 1.6. Propositions as Sets of States", " 1.7. Transforming English to Propositional Form", "Chapter 2. Reasoning using Equivalence Transformations", " 2.1. The Laws of Equivalence", " 2.2. The Rules of Substitution and Transitivity", " 2.3. A Formal System of Axioms and Inference Rules", "Chapter 3. A Natural Deduction System", " 3.1. Introduction to Deductive Proofs", " 3.2. Inference Rules", " 3.3. Proofs and Subproofs", " 3.4. Adding Flexibility to the Natural Deduction System", " 3.5. Developing Natural Deduction System Proofs", "Chapter 4. Predicates", " 4.1. Extending the Range of a State", " 4.2. Quantification", " 4.3. Free and Bound Identifiers", " 4.4. Textual Substitution", " 4.5. Quantification Over Other Ranges", " 4.6. Some Theorems About Textual Substitution and States", "Chapter 5. Notations and Conventions for Arrays", " 5.1. One-dimensional Arrays as Functions", " 5.2. Array Sections and Pictures", " 5.3. Handling Arrays of Arrays of", "Chapter 6. Using Assertions to Document Programs", " 6.1. Program Specifications", " 6.2. Representing Initial and Final Values of Variables", " 6.3. Proof Outlines", "Part II. The Semantics of a Small Language", "Chapter 7. The Predicate Transformer wp", "Chapter 8. The Commands skip, abort and Composition", "Chapter 9. The Assignment Command", " 9.1. Assignment to Simple Variables", " 9.2. Multiple Assignment to Simple Variables", " 9.3. Assignment to an Array Element", " 9.4. The General Multiple Assignment Command", "Chapter 10. The Alternative Command", "Chapter 11. The Iterative Command", "Chapter 12. Procedure Call", " 12.1. Calls with Value and Result Parameters", " 12.2. Two Theorems Concerning Procedure Call", " 12.2. Using Var Parameters", " 12.3. Allowing Value Parameters in the Postcondition", "Part III. The Development of Programs", "Chapter 13. Introduction", "Chapter 14. Programming as a Goal-Oriented Activity", "Chapter 15. Developing Loops from Invariants and Bounds", " 15.1. Developing the Guard First", " 15.2. Making Progress Towards Termination", "Chapter 16. Developing Invariants", " 16.1. The Balloon Theory", " 16.2. Deleting a Conjunct", " 16.3. Replacing a Constant By a Variable", " 16.4. Enlarging the Range of a Variable", " 16.5. Combining Pre-and Postconditions", "Chapter 17. Notes on Bound Functions", "Chapter 18. Using Iteration Instead of Recursion", " 18.1. Solving Simpler Problems First", " 18.2. Divide and Conquer", " 18.3. Traversing Binary Trees", "Chapter 19. Efficiency Considerations", " 19.1. Restricting Nondeterminism", " 19.2. Taking an Assertion out of a Loop", " 19.3. Changing a Representation", "Chapter 20. Two Larger Examples of Program Development", " 20.1. Right-justifying Lines of Text", " 20.2. The Longest Upsequence", "Chapter 21. Inverting Programs", "Chapter 22. Notes on Documentation", " 22.1. Indentation", " 22.2. Definitions and Declarations of Variables", " 22.3. Writing Programs in Other Languages", "Chapter 23. Historical Notes", " 23.1. A Brief History of Programming Methodology", " 23.2. The Problems Used in the Book", "Appendix I. Backus-Naur Form", "Appendix 2. Sets, Sequences, Integers and Real Numbers", "Appendix 3. Relations and Functions", "Appendix 4. Asymptotic Execution Time Properties", "Answers to Exercises", "References", "Index".

I stedet for qwerty programmering skal man tænke på programmer som beviser. Det er godt tænkt, men mon vi har lært ret meget i de forgangne 30 år? ( )