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

ThisvolumehasitsoriginsinameetingheldatMicrosoftResearch,Cambridge,in April2009tocelebrateTonyHoare’s75thBirthday(actually11Jan2009). Allthe technicalpapersexceptforthosewrittenbyAbramsky,Jackson,JonesandMeyer arebased–sometimesclosely,sometimesnot–onpresentationsgivenatthatme- ing. TheideaforthemeetingaroseinconversationsbetweenourselvesandAndrew HerbertofMicrosoft,whohostedatrulymemorableandhappyevent. ThemeetingwasorganisedbyourselvesandKenWood,withthe?nancials- portofMicrosoftResearchandFormalSystems(Europe)Ltd,andheldovertwo days. We wouldlike to recordparticularthanksto Angela Still of Microsoftfor makingallthelocalarrangementsatCambridgeandmuchmore:themeetingwould nothavehappenedwithouther. Whilethemajorityofthepapersinthisvolumearetechnical,weaskedauthorsto re?ectonthein?uenceofHoare’sworkontheirown?eldsandtomakeappropriate remarksonit. Allthetechnicalpaperswererefereed. DiscussionswithWayneWheelerofSpringerinspiredthetwoofustowritethe scienti?cbiographyofHoarethatisthe?rstpaperinthisvolume. Thoughwehave bothknownTonywellformanyyears,wewereamazedathowmanydiscoveries abouthimwemadeduringtheprocessofwritingthisarticle. WewouldlikethankWayneandhisassistantSimonReesfortheirhelpinprep- ingthisvolumeaswellastheirpatience. Muchoftheworkingatheringthepapers, ensuringconsistencyofLaTeXstyles,etc. ,wasdonebyLucyLiofOxfordUniv- sityComputingLaboratoryandwethankherwarmly. Tragically,KenWood’swifeLisadiedafteralongillnessinSeptember2009. Wededicatethisvolumetohermemory. January2010 CliffJones BillRoscoe ix Contents 1 Insight,InspirationandCollaboration. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 C. B. JonesandA. W. Roscoe 2 FromCSPtoGameSemantics. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.