Descriptive Types for XML Query Language Xcerpt
2006 (English)Licentiate thesis, monograph (Other academic)
The thesis presents a type system for a substantial fragment of XML query language Xcerpt. The system is descriptive; the types associated with Xcerpt constructs are sets of data terms and approximate the semantics of the constructs.
A formalism of Type Definitions, related to XML schema languages, is adopted to specify such sets. The type system is presented as typing rules which provide a basis for type inference and type checking algorithms, used in a prototype implementation. Correctness of the type system wrt. the formal semantics of Xcerpt is proved and exactness of the result types inferred by the system is discussed.
The usefulness of the approach is illustrated by example runs of the prototype on Xcerpt programs.
Given a non-recursive Xcerpt program and types of data to be queried, the type system is able to infer a type of results of the program. If additionally a type specification of program results is given, the system is able to prove type correctness of a (possibly recursive) program. Type correctness means that the program produces results of the given type whenever it is applied to data of the given type. Non existence of a correctness proof suggests that the program may be incorrect. Under certain conditions (on the program and on the type specification), the program is actually incorrect whenever the proof attempt fails.
Place, publisher, year, edition, pages
Institutionen för datavetenskap , 2006. , 108 p.
Linköping Studies in Science and Technology. Thesis, ISSN 0280-7971 ; 1228
ype system, XML querying, Xcerpt, type inference, type definitions
IdentifiersURN: urn:nbn:se:liu:diva-7542ISBN: 91-85497-10-XOAI: oai:DiVA.org:liu-7542DiVA: diva2:22550
2006-01-27, Alan Turing, House E, Campus Valla, Campus Valla, Linköpings universitet, Linköping, 13:15 (English)
Fischer Nilsson, Jørgen, Professor
Report code: LiU-TEK-LIC-2006:92006-10-092006-10-092009-06-08