Proving behavioural theorems with standard first-o

ProvingBehaviouralTheoremswithStandardFirst-OrderLogicMichelBidoit1andRolfHennicker21LIENS,C.N.R.S.U.R.A.1327&EcoleNormaleSupérieure45,Rued’Ulm,F-75230ParisCedex05,France2InstitutfürInformatik,Ludwig-Maximilians-UniversitätMünchenLeopoldstr.11B,D-80802München,GermanyAbstract.Behaviourallogicisageneralizationoffirst-orderlogicwheretheequalitypredicateisinterpretedbyabehaviouralequalityofobjects(andnotbytheiridentity).Weestablishsimpleandgeneralsufficientconditionsunderwhichthebehaviouralvalidityofsomefirst-orderfor-mulawithrespecttoagivenfirst-orderspecificationisequivalenttothestandardvalidityofthesameformulainasuitablyenrichedspecification.Asaconsequenceanyproofsystemforfirst-orderlogiccanbeusedtoprovethebehaviouralvalidityoffirst-orderformulas.1IntroductionObservabilityplaysaprominentroleinformalsoftwaredevelopment,sinceitpro-videsasuitablebasisfordefiningadequatecorrectnessconcepts.Forinstance,forprovingthecorrectnessofaprogramwithrespecttoagivenspecification,manyexamplesshowthatitisessentialtoabstractfrominternalimplementationdetailsandtorelyonlyontheobservablebehaviouroftheprogram.Asimilarsituationisthenotionofequivalencebetweenconcurrentprocessesandtheab-stractionfromsinglesteptransitionstoinput-outputoperationalsemantics.Behaviouralcorrectnessconceptscanbeformalizedbyusingabehaviourallogic,wheretheusualsatisfactionrelationoffirst-orderlogicwithequalityisgeneralizedtoabehaviouralsatisfactionrelation(cf.e.g.[14,12]).Thekeyideaistointerprettheequalitypredicatesymbolbyabehaviouralequality,wheretwoobjectsarebehaviourallyequaliftheycannotbedistinguishedbyexperimentswithobservableresults.Hencetoprovethebehaviouralvalidityofaformulawehavetoconsideringeneralinfinitelymanyobservableexperimentswhichareformallyrepresentedbyaninfinitesetof“observablecontexts”.Theproblemconsideredinthispaperishowtoprovethebehaviouralvalidityofsomefirst-orderformulaφwithrespecttoagivenfirst-orderspecificationSP.Weprovethat,whenthe(first-order)specificationSPsatisfiessomegeneralandsimpleproperty(calledthe“ObservabilityKernelassumption”),thebehaviouralvalidityofthefirst-orderformulaφ(w.r.t.SP)isequivalenttothestandardva-lidityofthesameformulaφwithrespecttothespecificationSPenrichedbyanadequatefinitaryfirst-orderformulathatrepresentstheinfinitesetofallobservableexperiments.Tothisend,weuseageneralcharacterizationofbe-haviouraltheoriesthatweestablishedin[5],andweshowthatthebehaviouralfirst-ordertheoryofSPisequaltothestandardfirst-ordertheoryoftheclassofthefullyabstract(standard)modelsofSP.Thenweprovideaninfinitaryaxiom-atizationoffullabstractness,andfinallyweshowthat,underthe“ObservabilityKernelassumption”,thisinfinitaryaxiomatizationisequivalenttoafinitaryone.Themainsignificanceofourresultisthatanyavailabletheoremproverforstandardfirst-orderlogicwithequalitycanbeused,firsttodischargethe“Ob-servabilityKernelassumption”,andthentoprovethebehaviouralvalidityoffirst-orderformulas.Thesoundnessandcompletenessofbehaviouralproofsonlyrelyonthesoundnessandcompletenessoftheactuallyusedstandardproofsys-tem.Ourresultisfairlygeneralsincewedonotneedanyrestrictionneitheronthefirst-orderspecificationSPnoronthefirst-orderformulaφtobeproved.Intheliteratureseveralapproachesformalizebehaviouralcorrectnesscon-ceptsbyintroducingsomekindofbehaviouralsemantics(cf.e.g.[8],[14],[12],[15],[2],[13]).Themaindrawbackoftheseapproachesisthattheyeitherdonotprovideaproof-theoreticalframeworkorsuggesttechnicallycomplicatedprooftechniqueswhichareonlyoflimitedinterestforpracticalapplications(cf.thecontextinductionprinciplein[10]orthecorrespondancerelationin[16]).[4]canbeconsideredasapreliminaryresult,butrestrictedtothebehaviouralproofofequationsw.r.t.equationalspecifications,withonlyonenonobservablesort.Thispaperisorganizedasfollows.InSection2webrieflysummarizethebasicnotionsofalgebraicspecificationsthatwillbeusedlateron.InSection3wedefinethebehaviouralequalityandtheassociatedbehaviouralsatisfactionrelation,weexplainhowallusualnotionscanbegeneralizedinabehaviouralframeworkandwepointoutthecrucialroleoffullyabstractalgebras.InSection4westudysufficientconditions(the“ObservabilityKernel”assumption)underwhichitisenoughtoconsiderafinitenumberofobservableexperiments.InSection5weshowhowthe“ObservabilityKernel”assumptionleadstoageneralmethodtoprovebehaviouraltheoremsusinganytheoremproverforstandardfirst-orderlogic.2BasicNotionsWeassumethatthereaderisfamiliarwithalgebraicspecifications[9,6].Thebasicconceptsandnotationsthatwillbeusedhereafterarebrieflysummarizedinthissection.A(manysorted)signatureΣisapair(S,F)whereSisasetofsortsandFisasetoffunctionsymbols.3Toeachfunctionsymbolf∈Fisassociatedanarity3InthispaperweassumethatbothSandFarefinite.s1...sn→swiths,s1,...,sn∈S.Ifn=0thenfiscalledconstantofsorts.AtotalΣ-algebraA=((As)s∈S,(fA)f∈F)overasignatureΣ=(S,F)consistsofafamilyofcarriersets(As)s∈Sandafamilyoffunctions(fA)f∈Fsuchthat,iffhasaritys1...sn→s,thenfAisa(total)functionfromAs1×...×AsntoAs(ifn=0thenfAdenotesaconstantobjectofAs).Σ-morphismsaredefinedasusual.ThecategoryofallΣ-algebrasisdenotedbyAlg(Σ).Throughoutthispaper,givenasignatur