Checking the Satisfiability of XML-Specifications
Harald Hiss · 2008
New developments in databases build on XML-technologies. Concepts of the relations model are transferred to XML. This is not unproblematic, transfer of integrity constraints causes a problem. Some XML-specifications are unsatisfiable. A deductive checker is presented. An extensive formalization developed with Isabelle integrates circular XML-specifications with an inductive method. These XML-specifications are unsatisfiable. The checker generates a representation with F-Logic that is checked with Florid. The correctness is proven. 1 Checking the Satisfiability New developments in databases build on XML [BMP06] technologies. Concepts of the relational [AHV95] model are transferred to XML. This is not unproblematic, transfer of integrity constraints causes a problem. Some XML-specifications are unsatisfiable. A deductive checker for XML-specifications is presented. The complexity of the satisfiability is proven in [FL02]. Implication of relational integrity that is undecidable [CV85] is represented with XML-specifications. A transformation for model checking XML-specifications is presented in [His07]. The transformation generates constraints. A model checker proves the satisfiability of the constraints. An extensive formalization developed with Isabelle [Pau94b] proves the correctness. Circular XML-specifications are integrated with an inductive method [Pau94a]. These XML-specifications are unsatisfiable. A deductive checker is presented based on this development. The checker generates a representation with F-Logic [KLW95] that is checked with Florid [HLS07]. The correctness of the checker is proven. XML-specifications are introduced in the next section with a database of teachers. Section 3 presents a formalization of XML-specifications illustrated with the example. Then section 4 formalizes circular XMLspecifications. Section 5 presents theorems for proving that circular XML-specifications are unsatisfiable in section 6. Then section 7 presents the deductive checker and section 8 concludes the contribution. 2 A Database of Teachers A database of teachers is represented with an XML-specification. Elements (teachers, research, subject) and attributes (name, instructor) are defined with the structural schema in figure 1. Content models form a structure for XML-trees. The root labeled teachers stores content model teacher. XML-trees of the structural schema have a teachers root with teacher children. Figure 2 shows an instance, the next section presents details. Attribute instructor represents a teacher. Integrity represents dependencies of attributes. Keys and inclusion constraints formalize integrity. Key teacher .name → teacher represents teacher with name. Inclusion constraint subject .instructor ⊆ teacher .name represents the dependency of instructor of subject on names. teacher .name → teacher subject .instructor → subject subject .instructor ⊆ teacher .name The XML-tree presented in figure 2 satisfies teacher .name → teacher . The teacher nodes store Dr. Brett and Prof. Crey . The instructors are contained, subject .instructor ⊆ teacher .name is satisfied. several subjects store Dr. Brett , the key subject .instructor → subject isn’t satisfied. The example is unsatisfiable. The subject research teacher teachers