0 What can we learn from a cake?. - 0. 0 Introduction. - 0. 1 What can we learn from a cake?. - 1 Preliminary notions notations and terminology. - 1. 0 Introduction. - 1. 1 The shapes of our calculations. - 1. 2 Laws and so on. - 1. 3 On avoiding parentheses. - 1. 4 On carrying out calculations. - 1. 5 Three new arithmetic operators. - 1. 6 The problem with the three dots. - 1. 7 What are the natural numbers?. - 1. 8 A bit about function application. - 1. 9 What next?. - 2 Predicates A Boolean operators. - 2. 0 Introduction. - 2. 1 The equivalence. - 2. 2 The disjunction. - 2. 3 Intermezzo on some interesting formulae. - 2. 4 The conjunction. - 2. 5 The implication. - 2. 6 The consequence. - 2. 7 The negation. - 2. 8 The discrepancy. - 2. 9 Summary of binding powers. - 2. 10 Final comments. - 2. 11 Exercises. - 3 Predicates B Quantified expressions. - 3. 0 How to write quantified expressions. - 3. 1 Laws for quantified expressions. - 3. 2 Universal quantification. - 3. 3 Existential quantification. - 3. 4 Some arithmetic quantifications. - 3. 5 Other quantified expressions. - 3. 6 Additional exercises. - 4 Specifications. - 4. 0 Introduction. - 4. 1 Assigning meaning to our predicates. - 4. 2 Towards writing specifications. - 4. 3 Examples of specifications. - 4. 4 Intermezzo on the array. - 4. 5 More examples of specifications. - 4. 6 Intermezzo on ascending functions. - 4. 7 Even more examples of specifications. - 4. 8 Other notations for functional specifications. - 4. 9 Comments on specifications. - 5 The shapes of programs. - 5. 0 Introduction. - 5. 1 The shapes of programs. - 5. 2 When is a program correct?. - 5. 3 A bit about wp. S. - 5. 4 Defining wp. S for all programs S. - 6 Intermezzo on calculations. - 7 Developing loopless programs. - 7. 0 Introduction. - 7. 1 Calculating expressions in assignments. - 7. 2 Developing IFs. - 8 Developing loops anintroduction. - 9 Loops A On deleting a conjunct. - 9. 0 Introduction. - 9. 1 An example Integer-division. - 9. 2 An example The linear search (and its billions of uses). - 9. 3 An example 3-tuple sort (and avoiding avoidable case-analyses). - 9. 4 An example Integer-division improved (and postponing design decisions). - 10 Loops B On replacing constants by fresh variables. - 10. 0 Introduction. - 10. 1 An example Evaluating a polynomial. - 10. 2 An example The minimum value. - 10. 3 An example Determining the multiple. - 10. 4 An example A table of cubes. - 10. 5 An example The maximum section sum. - 10. 6 An example The binary search (and its numerous applications). - 10. 7 An example Rearranging an array. - 10. 8 An example The bounded linear search. - 11 Mainly on recursion. - 11. 0 Introduction. - 11. 1 The general solution. - 11. 2 An example The sum of digits. - 11. 3 An example Exponentiation. - 11. 4 Introducing four new types. - 11. 5 An example Reversing a sequence (and the importance of good notation). - 11. 6 An example The post-order of a binary tree. - 11. 7 An example The depth of a binary tree. - 11. 8 Exercises. - 12 Back to scratch. - 12. 0 Introduction. - 12. 1 An example Evaluating a polynomial (and the discovery of nice specifications). - 12. 2 An example Greatest common divisors (and the discovery of useful properties). - 12. 3 An example All shortest paths (and the specification as logical firewall). - 12. 4 A final example Shiloach's algorithm. - 12. 5 Additional exercises. - 13 Where to go from here. - 13. 0 On what we have learned. - 13. 1 Where to go from here. - 13. 2 Be a little discriminating. - 13. 3 Inspirations and acknowledgements. - 13. 4 Selected references. - 13. 5 If you find a nice example. Language: English