搜索
BI-Hyperdoctrines,Higher-orderSeparationLogic,andAbstraction∗BODILBIERING,LARSBIRKEDAL,andNOAHTORP-SMITHDepartmentofTheoreticalComputerScienceITUniversityofCopenhagenWepresentaprecisecorrespondencebetweenseparationlogicandasimplenotionofpredicateBI,extendingtheearliercorrespondencegivenbetweenpartofseparationlogicandpropositionalBI.Moreover,weintroducethenotionofaBIhyperdoctrineandshowthatitsoundlymodelsclassicalandintuitionisticfirst-andhigher-orderpredicateBI,anduseittoshowthatwemayeasilyextendseparationlogictohigher-order.Wealsodemonstratethatthisextensionisimportantforprogramproving,sinceitprovidessoundreasoningprinciplesfordataabstractioninthepresenceofaliasing.CategoriesandSubjectDescriptors:D.2.7[SoftwareEngineering]:DistributionandMainten-ance—documentation;D.2.8[LogicsandMeaningsofPrograms]:SpecifyingandVerifyingandReasoningaboutPrograms—Assertions,Logicsofprograms,SpecificationtechniquesGeneralTerms:Reliability,Theory,VerificationAdditionalKeyWordsandPhrases:SeparationLogic,Hyperdoctrines,AbstractionContents1Introduction32BIHyperdoctrines52.1Hyperdoctrines..............................52.2BIHyperdoctrines............................73SeparationLogicmodeledbyBI-hyperdoctrines113.1Thepointermodel.............................113.2ThepointermodelasaBIhyperdoctrine................123.3Anintuitionisticmodel..........................143.4Thepermissionsmodel..........................144SomeConsequencesforSeparationLogic144.1FormalizingSeparationLogic......................14∗AnextendedabstractofthepresentpaperappearedintheproceedingsofESOP’05.LarsBirkedal’sandNoahTorp-Smith’sresearchwaspartiallysupportedbyDanishNaturalScienceResearchCouncilGrant51–00–0315andDanishTechnicalResearchCouncilGrant56–00–0309.Permissiontomakedigital/hardcopyofallorpartofthismaterialwithoutfeeforpersonalorclassroomuseprovidedthatthecopiesarenotmadeordistributedforprofitorcommercialadvantage,theACMcopyright/servernotice,thetitleofthepublication,anditsdateappear,andnoticeisgiventhatcopyingisbypermissionoftheACM,Inc.Tocopyotherwise,torepublish,topostonservers,ortoredistributetolistsrequirespriorspecificpermissionand/orafee.c1999ACM0164-0925/99/0100-0111$00.75ACMTransactionsonProgrammingLanguagesandSystems,Vol.TBD,No.TDB,MonthYear2·Biering,Birkedal,Torp-Smith4.2LogicalCharacterizationsofClassesofAssertions...........154.3PredicatesviaFixedPoints.......................175Higher-OrderSeparationLogic175.1ProgramLogicJudgments........................205.2InferenceRules..............................225.3InformalExplanationofRules......................225.4Soundness.................................245.5ADerivedRule..............................276DataAbstractionviaExistentialQuantification276.1ReasoningusingAbstractPriorityQueues...............276.2ImplementationsofPriorityQueues..................297SomeApplicationsofUniversalQuantification297.1PolymorphicTypesviaUniversalQuantification...........297.2Invariance.................................308RelatedandFutureWork30AProofofProposition2.833ACMTransactionsonProgrammingLanguagesandSystems,Vol.TBD,No.TDB,MonthYear.Higher-orderSeparationLogic·31.INTRODUCTIONVariantsoftherecentformalismofseparationlogic[Reynolds2002;IshtiaqandO’Hearn2001]havebeenusedtoprovecorrectmanyinterestingalgorithmsin-volvingpointers,bothinsequentialandconcurrentsettings[O’Hearn2004;Yang2001;Birkedaletal.2004].SeparationlogicisaHoare-styleprogramlogic,anditsmainadvantageovertraditionalprogramlogicsisthatitfacilitatesmodularrea-soning,aka.localreasoning,aboutprogramswithsharedmutabledata.Differentextensionsofcoreseparationlogic[Reynolds2002]havebeenusedtoprovecorrectvariousalgorithms.Forexample,Yang[Yang2001]extendedthecorelogicwithlistsandtreesandin[Birkedaletal.2004]thelogicwasextendedwithfinitesetsandrelations.Thusitisnaturaltoaskwhetheronehastomakeanewextensionofseparationlogicforeveryproofonewantstomake.Thiswouldbeunfortunateforformalverificationofproofsinseparationlogicsinceitwouldmaketheenter-priseofformalverificationburdensomeanddubious.Weargueinthispaperthatthereisanaturalsingleunderlyinglogicinwhichitispossibletodefinethevariousextensionsandprovetheexpectedpropertiesthereof;thisisthenthesinglelogicthatshouldbeemployedforformalverification.Partofthepointermodelofseparationlogic,namelythatgivenbyheaps(butnotstacks,i.e.,localvariables),hasbeenrelatedtopropositionalBI,thelogicofbunchedimplicationsintroducedbyO’HearnandPym[O’HearnandPym1999].Inthispaperweshowhowthecorrespondencemaybeextendedtoaprecisecorre-spondencebetweenallofthepointermodel(includingstacks)andasimplenotionofpredicateBI.WeintroducethenotionofaBIhyperdoctrine,asimpleextensionofLawvere’snotionofhyperdoctrine[Lawvere1969],andshowthatitsoundlymodelspredicateBI.ThenotionofpredicateBIweconsiderisdifferentfromtheonestudiedin[Pym2002;2004],whichhasabunchedstructureonvariablecontexts.However,webelievethatournotionofpredicateBIwithitsclassofBIhyperdoctrinemodelsistherightoneforseparationlogic(Pymaimedtomodelmulitiplicativequanti-fiers;separationlogiconlyusesadditivequantifier