Science of Programming

Part - 0: Why Use Logic? Why Prove Programs Correct? Part - 1: Propositions and Practices Propositions Reasoning Using Equivalence Transformations A Natural Deduction System Predicates Notations and Conventions for Arrays Using Assertions to Document Programs Part - 2: The Semantics of a Small Language The Predicate Transformer The Commands Skip Abort and Composition The Assignment Command The Alternative Command Procedure Call The Iterative Command Procedure Call Part - 3: The Development of Programs Introduction Programming as a Goal Oriented Activity Developing Loops from Invariants and Bounds Developing Invariants Notes on Bound Functions Using Iteration Instead of Recursion Efficiency Considerations Two Larger Examples of Program Development Inverting Programs Notes on Documentation Historical Notes Appendix - 1: 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 References Index