提出尝试以数学方式证明可靠性的非正式方法，以确保我们的计算机程序能够可靠运行。 即使没有严格的手续，也显示了该方法的好处。ContentsForewordPrefaceⅹ1111 Introduction1.1 How do you know a program does what you want it to?1.2 Why bother1.3 What did you want your program to do?4 Local versus global behaviour1.5 Reasoned programs1. 6 Reasoned programming111234567Modules1.8 Programming in the large1. 9 Logical notation1. 10 The leed for forinlalit101.11 Can programs be proved correct1.12 Summary12I Programming2 Functions and expressions2.1上 unctions152.2 Describing functions162. 3 Some properties of functions2.4 Using a functional language evaluator2.5 Evaluation of expressions222.6 Notations for functions24vi contents2.7 Meaning of expressions252.8 Summary262.9 Exercises3 Specilications273.1 Specification as contract273.2 Formalizing specifications3.3 Defensive specifications what happens if the input is3.4 How to use specilicationS: fourthroot.5 Proof that fourthroot satisfies its specification313.6 A little unpleasantness: error tolerances343. 7 Other changes to the contract353.8 A careless slip: positive square roots363.9 Another example, min373.10 Summary3.11 Exercises384 Functional programming in Miranda404.1 Data types- bool, num and char404.2 Built in functions over basic types414. 3 User-defined functions444.4 more constructions474.5 Summary4.6上 Xercises)25 Recursion and induction531 Rorecursion35.2 Evaluation strategy of miranda45.3 Euclids algorithm5.4 Recursion variants575.5 Mathenatical induction605.6 Double induction- Euclid's algorithm without division635.7 Summary655.8 Exercises656 Lists686.1 Introduction6.2 The list aggregate type6.3 Recursive functions over lists726.4 Trapping errors6.5 An example - insertion sort766.6 Another exampsorted merge6.7 List induction82limma.Ty86Contents vii6.9 Exercises877 Types7.1 Tuple917. 2 More on pattern matching937. 3 Curr ving947. 4 Types7.5 Enumerated typcs7.6 User defined constructors7.7 Recursively defined types7.8 Structural induction1067.9Summary1117.10 Exercises1128 Higher-order functions117Higher-order programming1178.2 The higheer-orderfunction map1178.3 The higher-order function fold4 Applications8.5 Implementing fold--foldr1228.6 Summary1238. 7 Exercises1249 Specification for Modula-2 programs1299.1 Writing specifications for Modula-2 procedures9.2 Mid-conditions1319.3 Calling proccdurcs1339.4 Recursion1359.5 Examples1369.6 Ca ling procedures in general9.7 Keeping the reasoning simple1:99. 8 Summary1399.9Exercises10 Loops1410.1 The coffee tin game14110.2 Mid-conditiois iI lOopS14410.3 Termination14510.4 An example14510.5 Loop invariants as a programming technique10.6 FOR loops14910.7 Summar510. 8 Exercises151viii Contents11 Binary chop15411.1 a tclcphonc directory15411. 2 Specification15511. 3 The algorithm11. 4 The prograIll15811. 5 Some detailed checks15911. 6 Checking for the presence of an element16011.7 Summa16111. 8 exercises16212 Quick sort16412.1 Quick sort16412.2 Quick sort- functional version16412. 3 Arrays as list12. 4 Quick sort in Modula-216712.5 Dutch national flag16912.6 Partitions by the Dutch national fag algorithm17212. 7 Summary17412.8 Exercises17413 Warshall's algorithm17613.1 Transitive closure17613.2 First algorithm13.3 Warshall s algorithm18113.41 Summary18413.5 Exercises18414 Tail recursion18611.1 Tail recursion18614.2 Example: gcd14. 3 General scheine14.4 Example: fact orial19014.5 Summary19)214.6 Exercises193ogIc19515 An introduction to logic19715.1 Logic19715. 2 The propositional language15. 3 Meanings of the connectives20015.4 The quantifier language20315.5 Translation from english205Contents ix15.6 Introducing equivalence20815.7 Somc uscful predicate cquivalcnccs20915.8 Summary21015.9 Exercises21116 Natural deduction21416.1 Arguments21416.2 The natural deduction rules16.3 Examples16. 4 Summary16.5 Exercises7 Natural deduction for predicate logic23717.1 V-elimination(vE)and 3-introduction (3I) rules23717.2 V-introduction(VI) and 3-climination (8) rulcs24217. 3 Equality24717.4 Substitution of equality24917.5 Suirmlary2:))17.6 Exercises1 8 Models26018.1 Validity of a rguments18.2 Disproving arguments26418.3 Intended structures26718.4 Equivalences26818.5 Soundness and completeness of natural deduction27118.6 Proof of the soundness of natural deduct ion27318.7 Proof of the completeness of natural deduction27518.8 Summary2791 8.9 Exercises280a Well-founded induction282A1 ExercisesB Summary of equivalences288c Summary of natural deduction rules289Further reading3ForewordHow do you describe what a computer program does without getting boggeddown in how it does it? If the program hasnt been written yet, we can askthe same question using a different tense and slightly different wording: Howdo you specify what a program should do without determining exactly how itshould do it? Then we can add the question: When the program is writtenhow do you judge that it satisfies its specificficationIn civil engineering, one can ask a very similar pair of questions: How canyouspecify what a bridge should do without determining its design? Andwhen it has been designed, how can you judge whether it does indeed dowhat it should?This book is about these questions for software engineering and its answerscall usefully be compared with what happens inl civil engineering. First, aspecification is a different kind of thing from a design; the specification of abridge may talk about load bearing capacity, deflection under high winds andresistance of piers to water erosion. while the design talks a bout quite differentthings such as structural components and their assembly. For soft ware, toospecifications talk about external matters and programs talk about internalmattersThe second of the two questions is about judging that one thing satisfiesanothcr. The main mcssagc of the book, and a vitally important onc, is thatjudgement relies upon under standing. This is obviously true in the case of thebridge; the judgement that the bridge can bear the specified load rests onstructural properties of components, enshrined in engineering principles. whichin turn rest upon the science of materials. Thus the judgement rests upon atower of understandingThis tower is well-established for the older engineering disciplines: forsoftware engineering, it is still being built.(We may call it"software science.The authors have undertaken to tell students in their first or second yearabout the tower as it now stands, rather than dictate principles to them. This