. 33 SamsonAbramsky 3 OnMereologiesinComputingScience. 47 DinesBjørner 4 Roles,Stacks,Histories:ATripleforHoare. 71 Johannes Borgstrom, ¨ Andrew D. Gordon, andRiccardoPucella 5 ForwardwithHoare. 101 MikeGordonandHel ´ene ` Collavizza 6 ProbabilisticProgrammingwithCoordination. 123 HeJifeng 7 TheOperationalPrincipleandProblemFrames. 143 MichaelJackson 8 TheRoleofAuxiliaryVariablesintheFormal DevelopmentofConcurrentPrograms. 167 C. B. Jones 9 AvoidaVoid:TheEradicationofNullDereferencing. 189 BertrandMeyer,AlexanderKogtenkov,andEmmanuelStapf 10 UnfoldingCSP. 213 MikkelBundgaardandRobinMilner xi xii Contents 11 Quicksort:CombiningConcurrency,Recursion, andMutableDataStructures. 229 DavidKitchin,AdrianQuark,andJayadevMisra 12 TheThousand-and-OneCryptographers. 255 A. K. McIverandC. C. Morgan 13 On Process-AlgebraicExtensions of Metric TemporalLogic. 283 ChristophHaase,Joel ¨ Ouaknine,andJamesWorrell 14 FunwithTypeFunctions. 301 OlegKiselyov,SimonPeytonJones,andChung-chiehShan 15 OnCSPandtheAlgebraicTheoryofEffects. 333 RobvanGlabbeekandGordonPlotkin 16 CSPisExpressiveEnoughfor. 371 A. W. Roscoe 17 TheTokeneerExperiments. 405 JimWoodcock,EmineGokc ¨ ¸eAydal,andRodChapman Chapter1 Insight,InspirationandCollaboration C. B. JonesandA. W. Roscoe Abstract TonyHoare’smanycontributionstocomputingsciencearemarkedby insightthatwasgroundedinpracticalprogramming. Manyofhispapershavehada profoundimpactontheevolutionofour?eld;theyhavemoreoverprovidedasource ofinspirationtoseveralgenerationsofresearchers. Weexaminethedevelopmentof hisworkthroughareviewofthedevelopmentofsomeofhismostin?uentialpieces ofworksuchasHoarelogic,CSPandUnifyingTheories. 1. 1 Introduction To many who know Tony Hoare only through his publications, they must often looklikepolishedgemsthatcomefromamindthatrarelymakesfalsesteps,nor evenperhapshastoworkattheircreation. Assooften,thisimpressionisafurther complimenttosomeonewhoactuallyaddstoveryhardworkandmanydiscarded attempts the ?nal polish thatmakes complexideas relatively easy for the reader tocomprehend. Asindicatedonpagexiof[HJ89],hisideastypicallygothrough manyrevisions. ThetwoauthorsofthecurrentpapereachhadthehonourofTonyHoaresuperv- ingtheirdoctoralstudiesinOxford. Theyknowat?rsthandhiskindandgenerous styleandwillcountitasanachievementifthispapercanconveysomethingofthe workingmethodsofsomeonebigenoughtoeschewcompetitionandpointscoring. Indeedit willbe apparentfromthe followingsectionshowoften,havingstarted somenewwayofthinkingorexcitingideas,hehappilyleavestheirexplorationand developmenttoothers. Wehavebothbene?tedpersonallyfromthis. C. B. Jones( ) SchoolofComputingScience,NewcastleUniversity,UK e-mail:cliff. jones@ncl. ac. uk A. W. Roscoe OxfordUniversityComputingLaboratory,UK e-mail:Bill. Roscoe@comlab. ox. ac. uk C. B. Jonesetal. (eds. ),Re?ectionsontheWorkofC. A. R.
Jones / Wood / Roscoe
Reflections on the Work of C.A.R. Hoare jetzt bestellen!
Weitere Infos & Material
Insight, Inspiration and Collaboration.- From CSP to Game Semantics.- On Mereologies in Computing Science.- Roles, Stacks, Histories: A Triple for Hoare.- Forward with Hoare.- Probabilistic Programming with Coordination.- The Operational Principle and Problem Frames.- The Role of Auxiliary Variables in the Formal Development of Concurrent Programs.- Avoid a Void: The Eradication of Null Dereferencing.- Unfolding CSP.- Quicksort: Combining Concurrency, Recursion, and Mutable Data Structures.- The Thousand-and-One Cryptographers.- On Process-Algebraic Extensions of Metric Temporal Logic.- Fun with Type Functions.- On CSP and the Algebraic Theory of Effects.- CSP is Expressive Enough for ?.- The Tokeneer Experiments.