流年开花De nitionAlabeledgraph(L,E,µL)overthealphabetΣLisa niteanddirectedgraph,whereLisasetofnodes,E L×Lisanedgerelationbetweenthenodes,andµL:L→ΣLisanodelabelingfunction.
AlabeledtreeisalabeledgraphT=(L,E,µL)ifithasasinglerootnoderoot(T)forwhichwehavethefollowing:Foreachnodel∈Lthereexistsexactlyonepathfromtheroottothenode,i.e.exactlyonesequencel0,...,ln,suchthatl0=root(T),ln=l,and(li 1,li)∈E,fori=1,...,n.
Anattributedtree(L,E,µL,µE)overthealphabetsΣLandΣEisalabeledtreewherethereisanadditionallabel-ingfunctionµA:L→ΣA,assigningattributestonodes.Giventwonodesl1andl2ofalabeledtree(L,E,µL),wecalll1theparentofl2andl2thechildif(l1,l2)∈E.Ifthereexistsa(non-empty)pathfroml1tol2,l1iscalledancestorofl2,andl2isadescendantofl1.
AnASTcanbeseenasanattributedtreewherethenodesarelabeledwithprogramstatementsand(sub)expressionswhiletheattributesdescribetheroleofanode’sbranch.E.g.,theconstructinFigure3(a)showspartofanASTforanif-thenbranching.Theattributesdescribewhetherthesubtreeistheif-branch,thecondition,orthenextinstruc-tionofitsparentnode.Thelabelsthendescribethekindofstatementorexpressionoftheconditionorthestatementfollowingtheif-then.
FromtheASTwecanconstructinastraightforwardmannerthecontrol owgraph(CFG).NotethataCFGdoestypicallynotcontainalltheinformationavailableintheAST,onlythecontrolstructuredowntothelevelofstatements,butnotthestructureofexpressions,types,andconstantvalues.
ACFGisagraph,terweaddlabelsmakingitalabeledgraph.WedenotethelabeledCFGofanASTTbyCFGT.Thelabelsrep-resentwhethercertainatomicpropositionsholdinanode.E.g.,ifaparticularvariableisassignedavalue,ifitisusedontheright-handsideofanassignment,orifitisderefer-encedandsoon.
Inourframework,theselabelsareassociatedwithtreepatternsontheAST.Wede nethesyntaxofaquerylan-guagetomatchtreepatternsasfollows:
P::= | |σE|σL|↓|↓ |P/P|P∪P|P[Q]Q::=P|label=σL|attr=σA|Q∧Q|Q∨Q3
3.1
TemporalLogicPropertiesoverPro-grams.
Undertheassumptionthatwecanidentifyatomicpropo-sitionsdeclx,usedxandassignedx,representingprogramlocationswhereavariablexisdeclared,used,orassignedavaluerespectively,wecanspecifythatthisvariableisal-waysinitializedbeforeitisusedasfollowsinCTL:
AGdeclx (A¬usedxWassignedx)
(1)
Thismeanswerequirethatonallprogrampathsifavari-ablexisdeclareditmustnotbeuseduntilithasavalueassignedoritwillnotbeusedatall.Weusetheweakun-tiloperatorWheretoincludethesecondpossibility.Thelattercanalsopointtounusedvariables,whichischeckedseparately.
Inthesamestylewecanexpressotherpropertiesoncor-rectpointerhandling,variableusageormemoryallocationanddeallocation.Moreover,itallowsspecifyingapplicationspeci cpropertiestohandlegeneralprogrammingguide-lines,API-speci crulesorevenhardware/softwareinter-facerulesfordrivers.
Intheremainderofthissectionwedescribehowtomapprogramstotransitionsystemslabeledwithatomicpropo-sitionssuchastheonesaboveandhowtoderivethelabelsthemselvesfromaprogram.
