Under consideration for publication in J. Function

UnderconsiderationforpublicationinJ.FunctionalProgramming1FromProcessLogictoProgramLogicKoheiHondaQueenMary,LondonDepartmentofComputerScienceQueenMary,LondonAbstractWepresentaprocesslogicfortheπ-calculuswiththelinear/affinetypediscipline(Bergeretal.2001;Bergeretal.2003;HondaandYoshida2002;HondaandYoshida2003;Hondaetal.2004;Yoshidaetal.2001;Yoshidaetal.2002).Builtontheprecedingstudiesonlogicsforprogramsandprocesses,simplesystemsofassertionsaredeveloped,capturingtheclassesofbehavioursrangingfrompurelyfunctionalinteractionstothosewithdestructiveupdate,localstateandgenericity.Acentralfeatureofthelogicisrepresentationofthebehaviourofanenvironmentasthedualofthatofaprocessinanassertion,whichiscrucialforobtainingcompositionalproofsystems.Fromtheprocesslogicwecanderivecompositionalprogramlogicsforvarioushigher-orderprogramminglanguages,whosesoundnessisprovedviatheirembeddingsintotheprocesslogic.Inthispaper,thekeytechnicalframeworkoftheprocesslogicanditsapplicationsispresentedfocussingonpurefunctionalbehaviourandaprototypicalcall-by-valuefunctionallanguage,leavingthefulltechnicaldevelopmentto(Honda2004a;Honda2004b).1IntroductionProgramLogicsofferabstractionofprograms’behaviourscentringonlogicalpredicatesonthem,combinedwithproofsystemsforderivingvalidjudgements.Theyareusefulbothforthedesignofprogramsonarigorousbasis(i.e.specification)andanalysisofexistingprograms(i.e.verification).Infact,thesetwoaspectsaremosteffectivelyintegratedinrealengineeringpractice,wherecodeordesigninproduction,annotatedwithpredicateswhichexpresscrucialsafetyproperties,issubjectedtologicalreasoningandtheresultisreflectedontotheprocessofdesignandcoding.Thisreasoningpartmayevenbehalf-mechanised,sothatprogrammerscangetfeedbackquicklyandreliably.Forallthesepurposestheproofsystemmayaswellbecompositional(i.e.rulesarebuiltfollowingthesyntacticstructureofthelanguage)since,inthisway,wecanreasonaboutalargerprogrambasedonpropertiesderivedforitsconstitutingparts.Somelogicsaremathematicallygeneralforagivenclassofprogramsinthatallmeaningfulobservablepropertiesarepreciselyspecifiable(and,uptoderivabilityofvalidjudgementintheassociateddomain,relativelyprovable)inthesys-tem.Sincetheprogramlogicsofthiskindcanexpresspropertiesofprogramsinageneralandrigorousfashion,andbecausetheassociatedproofsystemoffersafundamentalarticu-lationofsemanticsoflanguageconstructsandtheirinterplay,manyengineeringactivitiesrangingfromstaticanalysestoprogramtestingincreasinglyuseprogramlogicsastheirfoundation.Oneofthewell-knowninstancesofsuchlogics,whichineffectinitiatedthewholefield2K.Hondaofcompositionalprogramlogics,isthespecificationlogicbyTonyHoare(Hoare69),HoareLogic,developedonthebasisofearlierworkbyFloyd(Floyd67)andNaur(Naur66).HoareLogic,originallypresentedforasimpleimperativeprogramminglanguage,ispowerfulfromanengineeringviewpoint:formulaeandrulesaresimpleandintuitive,capturingtheessenceofdynamicsofimperativeprogramsconciselyandelegantly.Anditissatisfyingfromatheoreticalviewpoint;notonlytheproofsystemisbothsoundand(relatively)completewithrespecttoanaturallydefinedmodel,buteachoftheruleshasadecisiveformwhichfollowstheprincipleoffindingaweakestpreconditionforadesiredconclusion.TherehavebeenavastbodyoftheoreticalandpracticalstudiesstartingfromHoare’swork(seevarioussurveysincluding(Apt81;Cousot99)).Thematurityofthetheoreticalunderstandingandpracticaltechniquesisnowreachingthestagewhereonecandevelopconsistentproofrulesforreasoningaboutnon-trivialfragmentsofreal-worldprogramminglanguages,cf.(Oheimb2002;Jacobsetal.98;Poetzsf-HeffterandMuller99;LeavensandBaker99).Compositionalprogramlogicsmakeitpossibletoreasonaboutobservablepropertiesofsoftwarestartingfromtheirconstituentparts.Apieceofsoftware,inprincipleandincreas-inglyinpractice,canconsistofprogramswrittenindifferentlanguages.Evenifaprogramiswritteninasinglelanguage,whenitrunsunderanoperatingsystem,itspropertiesshouldbeconsideredincombinationwiththoseoftheoperatingsystem,whichmaybewritteninadifferentlanguage.Anotherinstantiationofthesameproblemiswhenahigh-levellan-guagecallsnativecode(manylibrariesofahigh-levellanguageareimplementedinthisway).Infact,almostallkindsofsoftwarenowadaysexplicitlyorimplicitlyrelyonthefunctionalitiesofothersoftware.AJavaprogramreliesonitsAPIswhichareimplementedusingnativecodeandOSlibraries,anOSlibraryuseskernelcalls,andevenakernelrelieson,forexample,theproperworkingofthenetworkforcarryingoutitsessentialfunction-alities.Thusreasoningaboutbehaviourofsoftwareacrosslanguageboundaries,butstillonarigorouslogicalbasis,isfundamentalforguaranteeingthesafebehaviourofsoftware.InspiteofmanystudiesonHoareLogicanditsderivatives,itseemsthistopichasnotbeeninvestigatedasextensivelyasthesubjectmaydeserve.Wepresentinthispaperonepossibleapproachtothisproblemdomain.Theideaistodevelopcompositionallogicsforatinyformalismofinteraction,anduseittoderive,analyseandmediate,viaencodingoflanguageconstructsinit,logicsformorecomplexprogramminglanguages.Thistinyformalism—whichisaminimalcoreofaprocesscalculus,theπ-calculus,introducedbyMilner,Parro