a Practical Theory of Programming 2011.09.27

《a Practical Theory of Programming 2011.09.27》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、aPracticalTheoryofProgramming2011-9-27editionEricC.R.Hehner–5aPracticalTheoryofProgramming2011-9-27editionEricC.R.HehnerDepartmentofComputerScienceUniversityofTorontoTorontoONM5S2E4CanadaThefirsteditionofthisbookwaspublishedbySpringer-VerlagPublishersNewYork1993ISBN0-387-94106-1QA76.6.

2、H428Thecurrenteditionisavailablefreeatwww.cs.utoronto.ca/~hehner/aPToPYoumaycopyfreelyaslongasyouincludealltheinformationonthispage.–4Contents0Preface00.0Introduction00.1CurrentEdition10.2QuickTour10.3Acknowledgements21BasicTheories31.0BooleanTheory31.0.0AxiomsandProofRules51.0.1Expres

3、sionandProofFormat71.0.2MonotonicityandAntimonotonicity91.0.3Context101.0.4Formalization121.1NumberTheory121.2CharacterTheory132BasicDataStructures142.0BunchTheory142.1SetTheory(optional)172.2StringTheory172.3ListTheory202.3.0MultidimensionalStructures223FunctionTheory233.0Functions233

4、.0.0AbbreviatedFunctionNotations253.0.1ScopeandSubstitution253.1Quantifiers263.2FunctionFinePoints(optional)293.2.0FunctionInclusionandEquality(optional)303.2.1Higher-OrderFunctions(optional)303.2.2FunctionComposition(optional)313.3ListasFunction323.4LimitsandReals(optional)334ProgramT

5、heory344.0Specifications344.0.0SpecificationNotations364.0.1SpecificationLaws374.0.2Refinement394.0.3Conditions(optional)404.0.4Programs414.1ProgramDevelopment434.1.0RefinementLaws434.1.1ListSummation434.1.2BinaryExponentiation45–3Contents4.2Time464.2.0RealTime464.2.1RecursiveTime484.2

6、.2Termination504.2.3SoundnessandCompleteness(optional)514.2.4LinearSearch514.2.5BinarySearch534.2.6FastExponentiation574.2.7FibonacciNumbers594.3Space614.3.0MaximumSpace634.3.1AverageSpace645ProgrammingLanguage665.0Scope665.0.0VariableDeclaration665.0.1VariableSuspension675.1DataStruct

7、ures685.1.0Array685.1.1Record695.2ControlStructures695.2.0WhileLoop695.2.1LoopwithExit715.2.2Two-DimensionalSearch725.2.3ForLoop745.2.4GoTo765.3TimeandSpaceDependence765.4Assertions(optional)775.4.0Checking775.4.1Backtracking775.5Subprograms785.5.0ResultExpression785.5.1Function795.5