Types for path correctness of XML queries

被引:19
作者
Colazzo, D [1 ]
Ghelli, G [1 ]
Manghi, P [1 ]
Sartiani, C [1 ]
机构
[1] Univ Pisa, Dipartimento Informat, Pisa, Italy
关键词
languages; theory; algorithms; verification; type correctness; XML queries; XML types;
D O I
10.1145/1016848.1016869
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
If a subexpression in a query will never contribute data to the query answer, this should be regarded as an error. This principle has been recently accepted into mainstream XML query languages, but was still waiting for a complete treatment. We provide here a precise definition for this class of errors, and define a type system that is sound and complete, in its search for such errors, for a core language, under mild restrictions on the use of recursion in type definitions. In the process, we describe a dichotomy among existential and universal type systems, which is useful to understand some unusual features of our type system.
引用
收藏
页码:126 / 137
页数:12
相关论文
共 18 条
[11]  
DRAPER D, 2003, XQUERY 1 0 XPATH 2 0
[12]  
Fernandez M., 1997, SIGMOD Record, V26, P4, DOI 10.1145/262762.262763
[13]  
HOSOYA H, 1999, XDUCE XML PROCESSING
[14]  
Jacquemard Florent, 1997, Tree automata techniques and applications
[15]  
LEE D, 2000, REASONING XML SCHEMA
[16]  
MILO T, 2000, P 19 ACM S PRINC DAT, P11, DOI DOI 10.1145/335168.335171
[17]  
THOMPSON HS, 2002, XML SCHEMA 1
[18]  
YERGEAU F, 2004, EXTENSIBLE MARKUP LA