Reflections on the Work of C.A.R. Hoare

. . . . . . . 33 SamsonAbramsky 3 OnMereologiesinComputingScience. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 DinesBjorner 4 Roles,Stacks,Histories:ATripleforHoare. . . . . . . . . . . . . . . . . . . . . . . . . . . .... Read more

. . . . . . . 33 SamsonAbramsky 3 OnMereologiesinComputingScience. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 DinesBjorner 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. Less