62Proving behavioural theorems with standard first

ProvingBehaviouralTheoremswithStandardFirst-OrderLogicM.BIDOITR.HENNICKERLaboratoired’Informatique,URA1327duCNRSDepartementdeMathematiquesetd’InformatiqueEcoleNormaleSuperieureInstitutfurInformatikLudwig-Maximilians-UniversitatMunchenLIENS-94-11September1994ProvingBehaviouralTheoremswithStandardFirst-OrderLogicMichelBidoit1andRolfHennicker21LIENS,C.N.R.S.U.R.A.1327&EcoleNormaleSuperieure45,Rued’Ulm,F-75230ParisCedex05,France2InstitutfurInformatik,Ludwig-Maximilians-UniversitatMunchenLeopoldstr.11B,D-80802Munchen,GermanyAbstract.Behaviourallogicisageneralizationofrst-orderlogicwheretheequalitypredicateisinterpretedbyabehaviouralequalityofobjects(andnotbytheiridentity).Weestablishsimpleandgeneralsucientconditionsunderwhichthebehaviouralvalidityofsomerst-orderfor-mulawithrespecttoagivenrst-orderspecicationisequivalenttothestandardvalidityofthesameformulainasuitablyenrichedspecica-tion.Asaconsequenceanyproofsystemforrst-orderlogiccanbeusedtoprovethebehaviouralvalidityofrst-orderformulas.1IntroductionObservabilityplaysaprominentroleinformalsoftwaredevelopment,sinceitpro-videsasuitablebasisfordeningadequatecorrectnessconcepts.Forinstance,forprovingthecorrectnessofaprogramwithrespecttoagivenspecication,manyexamplesshowthatitisessentialtoabstractfrominternalimplementationdetailsandtorelyonlyontheobservablebehaviouroftheprogram.Asimilarsituationisthenotionofequivalencebetweenconcurrentprocessesandtheab-stractionfromsinglesteptransitionstoinput-outputoperationalsemantics.Behaviouralcorrectnessconceptscanbeformalizedbyusingabehaviourallogic,wheretheusualsatisfactionrelationofrst-orderlogicwithequalityisgeneralizedtoabehaviouralsatisfactionrelation(cf.e.g.[14,12]).Thekeyideaistointerprettheequalitypredicatesymbolbyabehaviouralequality,wheretwoobjectsarebehaviourallyequaliftheycannotbedistinguishedbyexperimentswithobservableresults.Hencetoprovethebehaviouralvalidityofaformulawehavetoconsideringeneralinnitelymanyobservableexperimentswhichareformallyrepresentedbyaninnitesetof\observablecontexts.Theproblemconsideredinthispaperishowtoprovethebehaviouralvalidityofsomerst-orderformulawithrespecttoagivenrst-orderspecicationSP.Weprovethat,whenthe(rst-order)specicationSPsatisessomegeneralandsimpleproperty(calledthe\ObservabilityKernelassumption),thebehaviouralvalidityoftherst-orderformula(w.r.t.SP)isequivalenttothestandardva-lidityofthesameformulawithrespecttothespecicationSPenrichedbyanadequatenitaryrst-orderformulathatrepresentstheinnitesetofallobservableexperiments.Tothisend,weuseageneralcharacterizationofbe-haviouraltheoriesthatweestablishedin[5],andweshowthatthebehaviouralrst-ordertheoryofSPisequaltothestandardrst-ordertheoryoftheclassofthefullyabstract(standard)modelsofSP.Thenweprovideaninnitaryaxiom-atizationoffullabstractness,andnallyweshowthat,underthe\ObservabilityKernelassumption,thisinnitaryaxiomatizationisequivalenttoanitaryone.Themainsignicanceofourresultisthatanyavailabletheoremproverforstandardrst-orderlogicwithequalitycanbeused,rsttodischargethe\Ob-servabilityKernelassumption,andthentoprovethebehaviouralvalidityofrst-orderformulas.Thesoundnessandcompletenessofbehaviouralproofsonlyrelyonthesoundnessandcompletenessoftheactuallyusedstandardproofsys-tem.Ourresultisfairlygeneralsincewedonotneedanyrestrictionneitherontherst-orderspecicationSPnorontherst-orderformulatobeproved.Intheliteratureseveralapproachesformalizebehaviouralcorrectnesscon-ceptsbyintroducingsomekindofbehaviouralsemantics(cf.e.g.[8],[14],[12],[15],[2],[13]).Themaindrawbackoftheseapproachesisthattheyeitherdonotprovideaproof-theoreticalframeworkorsuggesttechnicallycomplicatedprooftechniqueswhichareonlyoflimitedinterestforpracticalapplications(cf.thecontextinductionprinciplein[10]orthecorrespondancerelationin[16]).[4]canbeconsideredasapreliminaryresult,butrestrictedtothebehaviouralproofofequationsw.r.t.equationalspecications,withonlyonenonobservablesort.Thispaperisorganizedasfollows.InSection2webrieysummarizethebasicnotionsofalgebraicspecicationsthatwillbeusedlateron.InSection3wedenethebehaviouralequalityandtheassociatedbehaviouralsatisfactionrelation,weexplainhowallusualnotionscanbegeneralizedinabehaviouralframeworkandwepointoutthecrucialroleoffullyabstractalgebras.InSection4westudysucientconditions(the\ObservabilityKernelassumption)underwhichitisenoughtoconsideranitenumberofobservableexperiments.InSection5weshowhowthe\ObservabilityKernelassumptionleadstoageneralmethodtoprovebehaviouraltheoremsusinganytheoremproverforstandardrst-orderlogic.2BasicNotionsWeassumethatthereaderisfamiliarwithalgebraicspecications[9,6].Thebasicconceptsandnotationsthatwillbeusedhereafterarebrieysummarizedinthissection.A(manysorted)signatureisapair(S;F)whereSisasetofsortsandFisasetoffunctionsymbols.3Toeachfunctionsymbolf2Fisassociatedanarity3InthispaperweassumethatbothSandFarenite.s1:::sn!swiths;s1;:::;sn2S.Ifn=0thenfiscalledconstantofsorts.Atotal-algebraA=((As)s2S;(fA)f2F)overasignature=(S;F)consistsofafamilyo