<p>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.</p><p>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.</p><p>The usefulness of the approach is illustrated by example runs of the prototype on Xcerpt programs.</p><p>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.</p> / Report code: LiU-TEK-LIC-2006:9
| Identifer | oai:union.ndltd.org:UPSALLA/oai:DiVA.org:liu-7542 |
| Date | January 2006 |
| Creators | Wilk, Artur |
| Publisher | Linköping University, Linköping University, TCSLAB - Theoretical Computer Science Laboratory, Institutionen för datavetenskap |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | English |
| Type | Licentiate thesis, monograph, text |
| Relation | Linköping Studies in Science and Technology. Thesis, 0280-7971 ; 1228, ; |
Page generated in 0.002 seconds