Abstract - lic thesis Artur Wilk
Descriptive Types for XML Query Language Xcerpt
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
back to main page