Skip to Main content Skip to Navigation

XQTC: A Static Type-Checker for XQuery Using Backward Type Inference

Pierre Genevès 1 Nabil Layaïda 1 Christine Vanoirbeek 2
1 WAM - Web, adaptation and multimedia
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : We present a novel technique and a tool for static type-checking of XQuery programs. The tool looks for errors in the program by jointly analyzing the source code of the program, input and output schemas that respectively describe the sets of documents admissible as input and as output of the program. The crux and the novelty of our results reside in the joint use of backward type inference and a two-way logic to represent inferred tree type portions. This allowed us to design and implement a type-checker for XQuery which is more precise and supports a larger XQuery fragment compared to the approaches previously proposed in the literature; in particular compared to the only few actually implemented static type-checkers such as the one in Galax. The whole system uses compilers and a satisfiability solver for deciding containment for two-way regular tree expressions. Our tool takes an XQuery program and two schemas Sin and Sout as input. If the program is found incorrect, then it automatically generates a counter-example valid w.r.t. Sin and such that the program produces an invalid output w.r.t Sout. This counter-example can be used by the programmer to fix the program.
Document type :
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Pierre Genevès Connect in order to contact the contributor
Submitted on : Tuesday, November 27, 2012 - 5:01:20 PM
Last modification on : Tuesday, November 16, 2021 - 5:04:08 PM
Long-term archiving on: : Saturday, December 17, 2016 - 3:30:18 PM


Files produced by the author(s)


  • HAL Id : hal-00757867, version 1


Pierre Genevès, Nabil Layaïda, Christine Vanoirbeek. XQTC: A Static Type-Checker for XQuery Using Backward Type Inference. [Research Report] RR-8149, INRIA. 2012, pp.25. ⟨hal-00757867⟩



Les métriques sont temporairement indisponibles