Abstract Types for Correctness of Queries over Semistructured Data

DarioColazzo

GiorgioGhelli

PaoloManghi

CarloSartiani

DipartimentodiInformatica-Universit`adiPisa,CorsoItalia40,Pisa,Italy

e-mail:{colazzo,ghelli,manghi,sartiani}@di.unipi.it

Abstract

operatorssuchasalternativepaths,wildcardmatching,collectionofdescendants.

AtypesystemforaquerylanguageshouldservebothOnepossiblenotionofquerycorrectness,adoptedbythepurposesofverifyingwhetheraqueryiscoherentwithXDucelanguage[4],isthefullcorrespondencebetweenthewhatisknownaboutthestructureofthedatabase(queryalternativepathsinaqueryandallthepossiblecasesofcorrectness)andofgivinginformationaboutthetypeoftheunion-typethatdescribestheinput.Thisapproachthequeryresult(resultanalysis).Currentproposalsforseems,however,toorestrictiveformanySSDspecificpro-typedquerylanguagesforsemistructureddataareusuallygrammingtasks.focusedonresultanalysis,butperformveryfewcontrols,Attheotherextreme,onemayflagasnon-correctonlyornoneatall,ofquerycorrectness.thosequeriesthatarestaticallydeemedtoalwaysreturnThisworkpresentsatypesystemforacoreofXQueryanemptycollection.Thisapproachhasbeensuggestedthatsupportsbothquerycorrectnessandresultanalysis,bytheauthorsofXQuery[1].However,unlessthesystemanddiscussessomeofthedesignissuesandalternatives.isabletoflagthespecificpartsofthequerywherethe

problemarises,thispolicybecomesquiteloose,andnotinformativeenoughforprogrammers.

1IntroductionAnintermediatenotionofcorrectnessistodeemasInconventionalquerylanguages,atypesystemanalyseswrongallandonlythosepathsinthequerythathavequerycorrectnessandtheresulttype.Querycorrectnessnohopetomatchtheinputdata.

Insummary,eachoftheseapproachesisreasonableinisgenerallydefinedasarelationofcompatibilitybetween

thetypeofthequeryinputandthequerytype.Thequerysomespecificapplication,hencenoneofthemcanbere-typerepresentsthetypeofthedatatargetedbythequery,gardedasthegeneralpurposesolution.andiseitherinferredfromthequerystructure,ordirectly

providedbytheprogrammer.Correctnessensures,attheOurcontributionThisworkdescribesatypesystemveryminimum,thatthequeryhassomehopetofindaforµXQuery,anabstractcoreofXQuery.µXQuery’s

typesystemprovidesaformalframeworkwheredifferentmatchindatathatrespectstheinputtype.

Resultanalysisistheprocessofcheckingwhetheranotionsofquerycorrectnesscanbeformalizedandcom-queryeffectivelyreturnsdataofanexpectedoutputtype.pared.Specifically,itsupportsanotionofconformanceofThischeckisperformedbyinferringtheoutputtypeofadatatoatype,ofresultanalysis,andisbasedonathree-levelsdefinitionofquerycorrectness,accordingtowhichqueryandbymatchingitagainsttheexpectedtype.

Bothquerycorrectnessandresultanalysisareusefulaquerycanbeclassifiedas:toolsforthedevelopmentofcomplexdatabaseapplica-•incorrect,ifthestructuralrequirementsofthequerytions,wheredatabasequeriesandhigh-levelprogram-willnotfindamatchagainstanyinstanceoftheminglanguageapplicationsareusuallycombinedforming

databaseschema;acomplexwebofinputandoutputtypedependencies.Inthecontextofsemi-structureddata(SSD)andXML

onlyafewqueryandmanipulationlanguagesexploitstatictypeinformation,giventhepossiblyirregularandunstablenatureofthedata.Currentproposalsmainlyfocusonresultanalysis[3,6,5],butperformveryfewcontrols,ornoneatall,ofquerycorrectness.Actually,thereisnoclearagreement,andneithermuchdiscussion,aboutwhatquerycorrectnessmeansinthiscontext.

ThisisduetothefactthatSSD,especiallyXMLdoc-uments,areusuallyendowedwithratherirregulartypedescriptions,comprisinguniontypes,recursivetypes,andwildcards;coherently,thecorrespondinglanguagesinclude

•weaklycorrect,ifthestructuralrequirementsofthequerywillfindamatchinatleastoneinstanceofthedatabaseschema.

•stronglycorrect,ifthestructuralrequirementswillfindamatchagainstallpossibleinstancesofthedatabaseschema.

Webelievethischaracterisationtobeparticularlysuit-ableinthecontextofSSDBs,asitisbasedonaclearsemanticcharacterizationbutisflexibleenoughtobecom-patiblewiththeneedsofdifferentapplications.

1

2

Querycorrectnessquerylanguages

inXML

Intheabsenceofinputtypedescription,querycorrectnesscannotbechecked.Asaconsequence,programmersmay

interpretanemptyresultasbeingduetoastructuralre-selNumscanbeappliedtotheelementpeopleofd.Thisquirementfailure(fromclause)oraselectionfailure(nofunctionistypecorrect,becauseXDucesupportsano-datasatisfiedthewhereclause).tionofquerycorrectnessaccordingtowhichfunctionsare

correctifandonlyiftheyspecifyamatchingpattern(afunctioncase)forallpossiblepatternsdescribedbythe

inputtype:exhaustivepatternsinfunctiondefinitionsarerequiredtoensurethesoundnessofthetypesystemof

XDuce,asstatedin[4].Indeed,thefunction,

]>

person[name[firstname[String],secondname[n:String]],

phone[p:String]],rest:person*

-->sndname[n],phone[p],selNums(rest)|

()-->()

(XD1)

Figure1:AsampleDTD.

Whenschemasareavailable,instead,somestaticcon-trolscaninprinciplebeperformed.However,theirregularnatureofSSDtypesandquerylanguagesmakesthisaimveryelusive.Infact,onlythelanguageXDucedefinesastandardnotionofquerycorrectness,butXDuceisquitefarfromthestandardstructureofquerylanguages,beingastricterrelativetofunctionallanguagesasML.

Otherapproaches,suchasXQuery’sandSuciu’sap-proach[6],arenotconcernedwiththeautomaticiden-tificationofincorrectqueriesandconcentrateonresultanalysis.Givenaqueryandaschemaforthedatabaseathand,theproblemisthatofcheckingwhethereveryoutputofthequeryconformstoagivenexpectedoutputtype.

Suchsolutionstargetdifferentkindsofapplicationsce-nariosandthereforedifferforanumberofdesignchoices.However,ifwefocusonquerycorrectness,XDuce’sap-proachturnsouttobequiterestrictiveforaquerylan-guage,whiletheotherapproachesareinsteadpoorlyin-formativefortheprogrammer.

XDuceXDuceisatyped,functional,Turingcompleteprogramminglanguage.ItisbasedonanML-likepatternlanguagethatimplementsaone-matchsemantics,i.e.ev-erypattern,insteadofcollectingeverymatchedpieceofdata(asinstandardquerylanguages),onlybindsthefirstmatch.XDuceisnearertoaprogramminglanguagethantoaquerylanguage,butweconsideritheresinceitistheonlyexampleoftypedlanguageforXMLthatexplicitlyprovidesanotionoftypecorrectness.

Forexample,considerthefollowingXDuce’sfunction,whichreturnsthelistofphonenumbersofallpeopleinthedocumentd,whichconformstotheschemainFigure1:

funselNums:person*-->(sndname,phone)*=

person[name[frsname[String],sndname[n:String]],

phone[p:String]],rest:person*

-->sndname[n],phone[p],selNums(rest)|

funselNums:person*-->(sndname,phone)*=

persons[name[frsname[String],sndname[n:String]],

phone[p:String]],rest:person*

-->sndname[n],phone[p],selNums(rest)|

persons[name[firstname[String],secondname[n:String]],

phone[p:String]],rest:person*

-->sndname[n],phone[p],selNums(rest)|

()-->()

(XD2)

isstaticallyjudgedincorrectandneverexecuted,becausethefieldpersonsisnotdefinedintheschema.Thisno-tionofcorrectness,however,istoorestrictiveforXMLqueryingpurposes.Forinstance,thefunction

funselNums:person*-->(sndname,phone)*=

person[name[frsname[String],sndname[n:String]],

phone[p:String]],rest:person*

-->sndname[n],phone[p],selNums(rest)|

()-->()

(XD3)

isconsideredincorrectandneverexecuted,althoughonewouldexpectthequerytoberun,asinstancesofthedatabaseexistthatarematchedbythebodyofthefunc-tion.

XQueryXQuery’stypesysteminferstheoutputtypeofaquerybymatchingthestructuralrequirementsofthequery(querytype)withthetypeofthequeryinput[3].Indoingthis,thetypesystemdoesnotidentifyanddiscardincorrectqueries,butsimplyassignsanemptytypetothosesubpartsofthequerythatcannotfindamatchinanyinstanceofthedata.Coherently,aqueryoveraninstanceofauniontypeisassignedanemptytypeonlywhennoneofthemembersoftheuniontypeisrelevanttothequery.1Giventheexpectedtypeofthequery’soutputdataandtheinferredoutputtypeofthequery,thesystemcanstaticallydetectifthequery’soutputvaluehastheexpectedoutputtype.

Thefunction(XD1)canbeencodedinthefollowingXQuery’squery,

for$pind/person,

$ninop:union($p/name/sndname,

$p/name/secondname),

$phin$p/phone

returndata($n),

$ph

Althoughtheschemaofdcontainsnoagefield,thetypesysteminfersexactlythesameoutputtypeinferredforthequery(XQ1).Thesamehappenswiththefollowingquery,althoughtheschemaofdcontainsnoseconnamefield.

(XQ1)

for$pind/person,

$ninop:union($p/name/sndname,

$p/name/seconname),

$phin$p/phone

returndata($n),

$ph

forwhichthetypesystemstaticallyinfersthefollowingoutputtype,

(elementsndname{xsd:string},elementphone{xsd:string})*

(XQ5)

Suciu’sproposalDanSuciuetal.focusonthedevel-opmentofaformalframeworkforthedefinitionofresultanalysistools[6].Theyviewqueriesastransformationprograms,i.e.applicationstransforminganoriginaldatasourceintoanXMLdatabasethatconformstoagiventype.

Theyexploreabackwardtypeinferencemechanism,whichtakesasinputsthequery,thequeryinputtype,theexpectedoutputtype,andchecksthateverydatabasethatistheresultofthequeryappliedtoaninstanceoftheinputtype,conformstotheoutputtype.Again,themethodologyfullyaddressestheissuesofresultanalysis,buttotallydisregardsanotionofquerycorrectness.

Function(XD3)correspondstothequery,

for$pind/person,

$nin$p/name/sndname,$phin$p/phone

returndata($n),

$ph

(XQ3)

Thetypesysteminfersthesameoutputtypeof(XQ1).Resultanalysisstatesthatboth(XQ1)and(XQ3)arecor-rectastheiroutputtypematches(isasubtypeof)theex-pectedtypeoftheoutput.Thefunction(XD2)becomesinstead,

for$pind/persons,

$ninop:union($p/name/sndname,

$p/name/secondname),

$phin$p/phone

returndata($n),

$ph

3µXQuery

µXQueryisanabstractversionoftheFLWRcoreofXQuery.ThemaindifferencebetweenµXQueryandXQueryisthelackofsupportforfunctiondefinitions,andforif−then−elseandtypeswitchexpression.Moreover,

(XQ2)

µXQueryfeaturesonlycopy-semanticsreturnclauses,

Thetypeinferredforthisqueryistheemptytype().hencediscardingreference-semanticselementconstruc-Thesystempinpointstheerror,astheprogrammerwastion.

ThenoveltyofµXQuery’stypesystemisthatithasexpectingadifferenttype.

Essentially,XQueryprovidesprogrammerswithpower-beenspecificallydesignedforbothresultanalysisandfulresultanalysistools,whichare,insomesituations,alsoquerycorrectnesschecking.Thetypesysteminferstheusefulfordetectingerrorsbeforeexecution.Inparticular,outputtypeofaquery,asinXQuery,butmakesadistinc-theauthorsobservethat,sincequeriesareassignedantionbetweencorrectandincorrectqueries,asinXDuce.emptytypeiftheycannotfindamatchinanyinstanceofInparticular,itsupportsathree-levelsdefinitionofcor-theinputtype,whentheinferredtypeisemptythesystemrectqueries,distinguishingbetweenweaklycorrectandmayautomaticallyreportthequeryasincorrect.Thisisstronglycorrectqueries.Weshallbrieflydiscussthead-generallytrue,unlesstheprogrammerwereexpectinganvantagesofthisapproach.emptytypeasoutput.Thisnotionofincorrectness,how-ever,isratherincomplete,asmanyincorrectqueriesdo3.1Grammarnotnecessarilyreturnanemptytype.Considerforexam-Queriesaredefinedbythefollowinggrammar:

plethefollowingquery:

for$pind/person,

$ninop:union($p/name/sndname,

$p/name/secondname),

$phin$p/phone

returndata($n),

$ph,$p/age

Q

::=

()|vB|󰀂l󰀇Q󰀂/l󰀇|Q,Q|x|Qp

|letx:=QreturnQ|forxinQreturnQ

Dataarerepresentedasorderedforests(f)oftrees(t),asdefinedbythefollowinggrammar:

f

::=

()|t|f,f

t::=

vB|󰀂l󰀇f󰀂/l󰀇

(XQ4)

3

wherevBisaleafvalueoftypeB,‘,’isassociative,and(),f=f,()=f.

Pathsaredefinedbythefollowinggrammar:

pls

::=::=

nil|/ls|//ls|pp|p+p󰀁l|∗

d1=

CarloSartiani

123456d2=

Dario

Colazzo

654321

3.2Querysemantics

AqueryQisevaluatedaccordingtoanenvironmentρwhichassociatesaforestwitheachfreevariableoccur-ringinQ,andtheresultisdenotedby[[Q]]ρ.Informally,[[Q]]ρyieldsthepair󰀄f,S󰀋,wherefistheforestreturnedbyQwithrespecttothesubstitutionρ,andSisasta-tusvariablethatcapturesanotionofcorrectexecution(formaldetailscanbefoundin[2]).Srangesovertheset{C,F},respectivelyrepresentingthecorrectorfaultystatusofexecution.Specifically,󰀄f,C󰀋statesthatfiscorrectlyreturnedbyaquery,while󰀄f,F󰀋statesthatfisfaultilyreturnedbyaquery.

Indetail,aqueryQcorrectlyreturnsaforestfinanenvironmentρ([[Q]]ρ=󰀄f,C󰀋),if,forallpathselectionsQ󰀁pinQ,thepathpfindsamatchwiththeforestre-turnedbyQ󰀁.Inparticular,forpathselectionsoftheformQ󰀁(p1+p2)pitisonlyrequiredthateitherp1porp2pfindsamatchintheforestreturnedbyQ󰀁.AqueryQfaultilyreturnsaforestfinanenvironmentρ([[Q]]ρ=󰀄f,F󰀋),ifthereexistsapathselectionQ󰀁pinQforwhicheitherQ󰀁faultilyreturnsaforestf󰀁orpcannotfindamatchinf󰀁.Becauseofuniontypes,twowell-typedinputvaluesmayexistsuchthatthesamequerymaycorrectlyreturnaresultononeandfaultilyreturnaresultontheotherone.Forthisreason,weadoptathree-levelsclassificationofthesemanticcorrectnessofaquerywithrespecttoaninputtype:stronglycorrectifitcorrectlyreturnsaforestforanywell-typedinput,weaklycorrectifitcorrectlyreturnsaforestforsomewell-typedinput,incorrectifitfaultilyreturnsaforestforanywell-typedinput(Definition3.1).Considerforexamplethedatabasesd1andd2inFig-ure2,whichconformtotheschemainFigure1.Thequery(XQ4)ond1faultilyreturnstheforest:

Sartiani123456

Figure2:Twodb’sconformingtotheDTDinFigure1

overd1,andreturnsthesameforestfabovewithS=C,sinceoneofitsalternativepathsfindsamatchind.(XQ1)isactuallystronglycorrect,since,foranywell-typedcon-tentofthedatabase,atleastoneofitsalternativepathsfindsamatch.Thequery(XQ5),whenappliedtod1,returnsthesameforestas(XQ1),thankstothedisjunct/name/sndname,hencethisexecutioniscorrect,despitethepresenceofthewrongpath/name/seconname.How-ever,(XQ5)isactuallyweaklycorrectsince,overd2,itsexecutionisfaulty.

Hence,oursemanticsdefinesathree-levelnotionofthecorrectnessofaquerywithrespecttoaninputtype.Now,ouraimistodefineatypesystemthatisabletoinfer,foreachquery,areasonableapproximationofitssemanticcorrectnesswithrespecttoagiveninputtype.

3.3Typesystem

InthisSectionweintroduceµXQuery’stypesystem.Wefirstintroducethesyntaxoftypes,thengiveaninformalcharacterisationofthesemanticsoftypes,andgiveachar-acterisationoftypecorrectnessintermsofthesemanticsofqueries.Formaldefinitions,aswellastyperules,canbefoundin[2].3.3.1

Typelanguage

ThetypelanguageweconsiderisessentiallyXDuce’stypelanguage,andisdefinedbythefollowinggrammar.

T

::=

()|B|T,U|T+U|l[T]|X

asthepathselection($p\\age)doesnotmatchthedata;forthesamereason,(XQ4)executionwouldbefaultyoverd2oranydthatconformstothesameschema.Thesameistrueforthequery(XQ2),whichfaultilyreturnstheemptyforestbecausethe/personspathwillnevermatchthedata.Thesequeriesareincorrect.

Ontheotherside,aqueryd/person/name/secondnamewouldfaultilyreturnanemptyforestwhenappliedtod1,sinceitfindsnomatch,butwouldcorrectlyreturnaresultwhenappliedtod2.Hencethisqueryisweaklycorrect.ForpathselectionsQ(p1+p2)p,ournotionofcorrectexecutionisratherpermissive,inthesensethat,aswealreadysaid,matchingisrequiredforatleastonealterna-tive.Thequery(XQ1),forexample,iscorrectlyexecuted

4

whereBrepresentsatomictypes.Theemptytype()onlycontainstheemptyforest().Thetypeconstructorl[T]representsthesetoftreesrootedaslandcontainingaforestoftypeT.ConcatenationT,Urepresentsthesetofforestsf,f󰀁,wherefandf󰀁areforestsinTandUrespectively.TheuntaggeduniontypeconstructorT+UrepresentsthesetofforestsfwhichbelongtoeitherTorU.

TypevariablesaredefinedbyanenvironmentE,whichconsistsofasetofpotentiallymutualrecursivetypedefi-nitionsofthefollowingform:

E::=

()

X=T,Ex:T,Eemptyenvironmenttypevariabledefinitionqueryvariabledeclaration

Notethatenvironmentsalsocontainqueryvariabletypedeclarationsx:T.Theseareusedinthetypingrulesgivenin[2].Moreover,observethatregularexpressionstypes,suchasrepetitionandoptionaltypes,canbedefinedbycombiningrecursiveanduniontypesasfollows:

T∗≡XwithX=()+(T,X)

T?≡()+T

denotesanylabel)andthepathp.

TypeofQ[l[T]+m[U]][l[T]+m[U]][l[T]+m[U]][l[T]+m[U]][l[T]+m[U]][l[T]+m[U]]+n[V]]

WeakYesYesYesYesNoYes

Forinstance,theDTDgiveninFigure1correspondstothefollowingµXQuery’stypeenvironment,

PEOPLE=people[PERSON+]PERSON=person[NAME,PHONE]

NAME=name[(FRSNAME,SNDNAME)+(FIRSTNAME,SECONDNAME)]FRSNAME=frsname[String]SNDNAME=sndname[String]

FIRSTNAME=firstname[String]SECONDNAME=secondname[String]PHONE=phone[String]

/l+/m/l+/m+/n

/l/l+/n/n/l+/o

Table1:Inferredcorrectness.

Asillustratedbytherows1and2,QpisstronglytypecorrectifpfindsamatchineachinstanceofthetypeofQ.Accordingly,whencheckingcorrectnessofapathpwithaninputuniontype,therulesstatethatQpisstronglycorrectonlyifallmembersoftheuniontypearematchedbyp(datacovering).However,wedonotrequireherethepathcoveringproperty,i.e.thateverydisjunctivememberofpismatched(ormaybematched)byapieceofdata,hencerow2isstronglycorrectaswell.Datacoveringandpathcoveringare,inasense,independentissues,bothofthemrelevant,thoughwefocushereonthefirstoneonly;wewillcomebacktothisinSection4.

Whennotallmembersofthetype,butatleastone,arematchedbyp,thequeryisweaklycorrect,asexemplifiedinrows3,4,and6.Inthiscase,programmersmayexploitthisinformation,decidingeithertomaketheirqueriesstronglycorrect,byaddingthemissingalternativesinthepath,orrunthemanywaywhentheyarenotinterestedinqueryingthenon-matchinginstances.Finally,row5ex-emplifiesanincorrectquery,whosepathwillnevermatchanydata.

Therules,givenaqueryQandanenvironmentE,inferapair(T;A),whereTistheoutputtypeofQandAisavariablethatrangesovertheset{s,w,i}.Thecorrectdefinitionoftherulesisfarfromtrivial.Considerthefol-lowingqueryoveradatabaseoftyperoot[a[int]+b[int]],boundtothevariable$y,

{$y/a,$y/b}

WhilequerycorrectnessinXDuceandXQueryisbasedonsubtyping,inµXQueryitisbasedonarelationofcoherencebetweenquerypathsandqueryinputtypes.23.3.2

Semanticsoftypes

Weinterpretatypeasthesetofallforeststhathavethattype.Inthestyleof[4],wedefinethesemanticsoftypesbymeansofasetofdeductionrulesoverjudgementsoftheformE󰀊f:T,whichstatethatfconformstoTwithrespecttoE.Informally,wewrite

[[T]]E={f|E󰀆f:T}.

3.3.3Querycorrectness

TodefinequerycorrectnessinµXQuery,wedenoteas[[Q]]Ethesetofallpossibleresults,i.e.pairs󰀄f,S󰀋,re-turnedbyQ,foreachassignmenttoQ’svariablesthatrespectsthetypedefinitionsinE.

Definition3.1(Correctness)GivenaqueryQandanenvironmentEoftypedefinitionsforfreevariablesinQ,wesaythatQis

stronglycorrectweaklycorrectincorrect

ififif

∀󰀄f,S󰀋∈[[Q]]E.S=C∃󰀄f,S󰀋∈[[Q]]E.S=C∀󰀄f,S󰀋∈[[Q]]E.S=F

In[2]wehavedefinedasetofalgorithmicruleswhichreflectthischaracterisation,byreturningtheinferredcor-E󰀆Q:w,E󰀆Q󰀁:w⇒E󰀆Q,Q󰀁:w

rectnessofaquery(therelationshipbetweenthecorrect-nessasinferredbythetyperulesandtheactualcorrect-doesnotsufficefortheexampleabove,asboth$y/aandnessisdiscussedbelow).Observethatquerycorrectness$y/bareweaklycorrectwithrespecttothetypeof$y.

Similarly,butmoresubtly,thefollowingquery

{$y/a/a,$y/a/b}

Thequeryissemanticallyincorrect,as$yeithermatches/aor/b,butcannotmatchbothofthem.However,astandardinductivetyperulesuchas,

5

where$yisoftyperoot[X]withX=a[X]+b[X]+int,issemanticallyincorrect.Indeed,theproductquery$y/a/a,$y/a/bisincorrectaseachlevelofaunarytreeeithercontainsalabelaoralabelb.

In[2]wegiveasolutiontotheseproblemsbymeansofcomplexalgorithmictyperules,whichkeeptrackofwhichmembersofuniontypesarematchedbythepathsinthequery,andreturnacorrectnessstatuswhichdependsonthisinformation.

Thefollowingpropositionclaimssoundnessofthetyperuleswithrespecttothecharacterisationofquerycor-rectness,althoughtherulesarenotcomplete(astronglycorrectquerymaybeflaggedasw).

Proposition3.2(Soundness)ForeachqueryQandenvironmentE,ifthejudgementE󰀊Q:(T;A)holds,then,

ifA=sthenQisstronglycorrect;

ifA=wthenQisweaklyorstronglycorrect;ifA=ithenQisincorrect;

Observethatthetyperulesalwaysinferanoutputtype.Bydoingso,inthestyleofXQuery,thetypesystemalsoprovidesprogrammerswithresultanalysistools.Forex-ample,forqueries(XQ1)to(XQ4),ourtyperulesinferthesameoutputtypesasXQuery’s.However,wearealsoabletoidentify(XQ1)asstronglycorrect,(XQ3)and(XQ5)asweaklycorrect,and(XQ2)and(XQ4)asincorrect.

wrongpath.Goingbacktoline4ifthetable,thedata-coveringerroris‘branchm[U]inthetypeisnotcovered’,whilethepath-coveringoneis‘subpath/nisirrelevant’.Thesecondmessagehelpstheprogrammerbetter.

Forthesereasons,pathcoverageshouldbeconsid-eredbyacorrectness-checkingtypesystem.How-ever,whilewegaveaprecisesemanticcharacteriza-tionofthecorrectnessofaquerywithrespecttodatacovering,thisisnoteasywhenpathcoveringisconsidered.Asanexample,thepathexpression(/a+/b+/c),(/a+/b+/c),(/a+/b+/c)shouldbeequiva-lenttoitsexpansion/a/a/a+/a/a/b+/a/a/c+/b/a/a....However,thefirstoneshouldprobablybeconsideredwrongonlywhenoneofthenineatoms/xisuseless,whilethesecondoneissuspectassoonasanyoneofthetwenty-sevenaddendsisuseless.

In[2]wediscusssomeconcretenotionsofpath-coveringcorrectnessandtyperules;herewecanonlypointoutthattheproblemisrelevantanddifficult.

5Conclusionsandfutureissues

ThisworkpresentsatypesysteminwhichbothresultanalysisandquerycorrectnessanalysisofXMLqueriescanbeconvenientlyexpressed.Specifically,queriescanbeclassifiedasstronglycorrect,weaklycorrect,orincorrect.Wehaveseenthatsuchclassificationdescribesanintuitivespectrumofquerycorrectnesscharacterisations.

Ourtypesystem,besidebeingthefirsttotrycorrect-nessanalysisforXQuery-likelanguages,alsoprovidesaframeworkinwhichdifferentnotionsofcorrectnesscan4Pathcovering

beformallyidentifiedandstudied,asexemplifiedinthe

Tosimplifythediscussion,imagine,foramoment,thatdiscussionofSection4.Wearecurrentlyworkingontheeveryqueryisjustasumofpaths,andeveryinputtypedesignandcomparisonofsuchalternativenotions.isjustauniontype.Then,thesystemwedescribedupFinally,weplantoaugmentthetypelanguagewithtonowisgearedtowardsthepreventionofproblemsthatothertypeoperators,suchasnon-orderedsequences,IDarise(informally)becauseonebranchoftheinput-dataandIDREFstypes,soastostudyourresultsinthecon-union-typeisnotcoveredbyanypath(lackofstrongcor-textofasystemclosertoXMLSchema.rectness),orevennobranchoftheuniontypeiscoveredbyanypath(lackofweakcorrectness).

Thisisalreadycomplexenough,butonlycapturesthoseReferences

errorsthatshowupas‘toofewpathsinthequery’.Errors[1]D.Chamberlin&J.Clarketal.XQuery1.0:AnXMLmayalsoshowupas‘toomanypaths’,asinrows2,4,andQueryLanguage.Technicalreport,W3C,2001.6,inTable1,orinquery(XQ5),wherewehavepathsthat

[2]D.Colazzo&G.Ghellietal.TypesforCor-arenotcoveredbyanybranchoftheuniontype.

rectnessofQueriesoverSemi-structureddata.

Typicalprogrammingerrors,likepathmisspelling,tendhttp://www.di.unipi.it/~colazzo/tcqssd.ps.togeneratebothpathanddatacoverageproblems,asin

(XQ5)orinrow4,hencesuggestingthatpathcoverage[3]P.Fankhauser&M.Fernandezetal.XQuery1.0formal

semantics.Technicalreport,W3C,2001.

maybeignored.Ontheotherside,considerrow6in

Table1.Heretheprogrammermisspelledan/mintoan[4]H.Hosoya.RegularExpressionTypesforXML.PhDthesis,

TheUniversityofTokyo,Japan,2000./o,wasexpectinga‘weakcorrectness’result,andgets

itfromthetype-checker;hence,themisspellingproblem[5]D.Suciu.TheXMLTypecheckingProblem.SIGMOD

RecordWebEdition,SpecialSectiononDataManagementdoesnotshowupinthetype.

IssuesinElectronicCommerce,2002.Moreover,theerrorsgeneratedbyadata-coveringbased

analysiscanonlybereportedintermsoftype-branches[6]T.Milo&D.Suciu&V.Vianu.Typecheckingfor

XMLTransformers.InACMSymposiumonPrinciplesofthathavenotbeenconsideredbyasubpartofthequery,

DatabaseSystems,2000.whileapath-coveringbasedanalysiswouldpinpointa

6