XQTC: A Static Type-Checker for XQuery Using Backward Type Inference - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2012

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

(1) , (1) , (2)
1
2

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.
Nous présentons une technique nouvelle et un outil pour le contrôle de type statique des programmes XQuery. L'outil recherche les erreurs dans le programme en analysant à la fois le code source du programme et les schémas d'entrée et de sortie qui décrivent respectivement les ensembles de documents admissibles en entrée et en sortie. L'originalité de nos résultats réside dans l'utilisation conjointe de l'inférence de type arrière et d'une logique avec programmes inverses pour représenter des fragments de types d'arbre. Cela nous a permis de concevoir et de réaliser un contrôleur de type pour XQuery qui est plus précis et supporte un fragment de XQuery plus large que les approches proposées précédemment dans la littérature, en particulier si on se réfère aux quelques contrôleurs de type statiques effectivement réalisés, tel que celui de Galax. L'ensemble du système utilise des compilateurs et un solveur pour décider de l'inclusion des expressions d'arbres régulières bi-directionnelles. Notre outil prend en entrée un programme XQuery et deux schémas Sin et Sout. Si le programme est reconnu incorrect, l'outil engendre automatiquement un contre-exemple valide vis-à-vis de Sin et tel que le programme produise un résultat invalide vis-à-vis de Sout. Ce contre-exemple peut alors être utilisé par le programmeur pour corriger son programme.
Fichier principal
Vignette du fichier
RR-8149.pdf (1.06 Mo) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00757867 , version 1 (27-11-2012)

Identifiers

  • HAL Id : hal-00757867 , version 1

Cite

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⟩
233 View
102 Download

Share

Gmail Facebook Twitter LinkedIn More