Muhammad Junedi
email: muhammad.junedi@inria.fr

Pierre Genevès
email: pierre.geneves@inria.fr

Nabil Layaïda
email: nabil.layaida@inria.fr

XML Query-Update Independence Analysis Revisited

Keywords: H.2.3 [Database Management]: Languages-Query languages XML, Query, Update, Independence

XML transformations can be resource-costly in particular when applied to very large XML documents and document sets. Those transformations usually involve lots of XPath queries and may not need to be entirely re-executed following an update of the input document. In this context, a given query is said to be independent of a given update if, for any XML document, the results of the query are not affected by the update. We revisit Benedikt and Cheney's framework for query-update independence analysis and show that performance can be drastically enhanced, contradicting their initial claims. The essence of our approach and results resides in the use of an appropriate logic, to which queries and updates are both succinctly translated. Compared to previous approaches, ours is more expressive from a theoretical point of view, equally accurate, and more efficient in practice. We illustrate this through practical experiments and comparative figures.

INTRODUCTION

XQuery is becoming increasingly popular as a transformation and query language for XML documents. XML Update Language extends the syntax and semantics of XQuery to provide update features, i.e. side effects on documents (for example insertion and deletion of nodes).

XML query-update independence analysis consists in statically checking whether the results of a given query are affected by an update. Determining independence has many important applications which makes it an important line of research: avoiding view re-materialization, concurrency control and transaction management optimization, access policy enforcement, query engine optimization, web page consistency and others. The fact that independence detection is undecidable in general for XQuery and XML Update Language raises the challenge of finding a compromise between the accuracy and efficiency of static analysis and trying to support the largest fragments of query and update languages.

The static detection of query-update independence usually follows a two-step approach. As a first step, a common representation of queries and updates should be established in order to analyze them jointly. This operation usually relies on the extraction of path expressions that model both queries and updates. As a second step, once the common representation is obtained, independence can be checked using some intersection testing techniques on these paths. Two aspects are key for the accuracy and efficiency of the whole process:

• the adopted common representation, as its expressiveness (e.g. being able to capture schemas) has a direct effect on the accuracy, and its succinctness has a direct impact on efficiency;

• the chosen intersection testing technique, as its theoretical complexity and algorithmic effectiveness directly affect the performance of the analyzer.

In [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF], Benedikt and Cheney provide a generic framework for independence analysis based on destabilizers and compare different approaches for intersection analysis. The clear separation of concerns in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF] between the representation problem and the problem of intersection analysis provides a good environment for comparison between different independence analysis approaches in addition to the genericity of the framework that can handle any update and query language.

Contribution

In this paper, we revisit query-update independence analysis as proposed by Benedikt and Cheney [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF] under the light of the latest developments in intersection testing through a satisfiability checker for an expressive logic, namely the µ-calculus.

We provide evidence that our approach is more expressive in theory, equally accurate, and provides better performance compared to the various alternatives suggested in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF]. We provide experimental results that back our claims and invalidates Benedikt and Cheney's claims that using such an approach is not competitive.

XML QUERY-UPDATE ANALYSIS

In this section we recall the XML query-update framework introduced by Benedikt and Cheney [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF] that we have reimas a prerequisite for developing our approach. The framework of [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF] relies on a common representation called selection queries for both updates and queries. Specifically, the query is represented as the set of updates that can change the result of that query, which is called the query destabilizer (i.e. the set of nodes that can destabilize the query if they are a target of some update).

Updates are represented by a description of the target nodes that are modified. Then, different intersection analysis techniques can be applied in order to check that none of the target nodes are in the query's destabilizer.

The XML query language supported by [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF] is an XQuery subset called XQ and the supported update language is a part of snapshot semantics-based XQuery Update Facility [START_REF] Chamberlin | XQuery Update Facility. W3C WD[END_REF]. XML documents are considered as tree structures. The reader is referred to [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF] for full details on the syntax and semantics of XQ and XML Updates.

To illustrate destabilizers, we consider as an example the XPath query Q1 = $doc/C, $doc refers to the document root. The result of Q1 can be affected in different manners:

• the subtree value of the result of Q1 is destabilized if update operations (i.e. insert, delete, replace and rename operations) have a target node in {$doc, $doc/C, $doc/C/descendant-or-self::*}. This set is called the value destabilizer of $doc/C query, which is abbreviated as ∆ v * ($doc/C);

• the boolean result of Q1 can be changed from nonempty to empty if update operations have a target node in {$doc, $doc/C}. This set is called the negative boolean destabilizer and is abbreviated as ∆ b- * ($doc/C);

• the boolean result of Q1 can be changed from empty to nonempty if update operations have a target node in {$doc, $doc/child::*}. This set is called the positive boolean destabilizer and is abbreviated as ∆ b+ * ($doc/C);

• the node structure of the result of Q1 is destabilized if update operations have a target node in {$doc, $doc/ child::*}. This set is called a node destabilizer and is abbreviated as ∆ n * ($doc/C).

The previous example explains the four types of generic destabilizers. To improve accuracy, an update sensitive version of destabilizers is proposed which takes only the update in question into consideration. For example no insert operation can change the results of a query from nonempty to empty. Similarly, no delete operation can change the results of a query from empty to nonempty. Moreover, only a renaming operation on $doc/child::* can destabilize the node structure of Q1, which is an example of a rename sensitive node destabilizer: ∆ n rename ($doc/C) = {$doc/child::*} which is more accurate than including $doc also in node destabilizer set.

These four types of generic and operation sensitive destabilizers are used in the query rewriting algorithm (from an XQ query to a destabilizer) as four mutually recursive functions on the structure of the query. The resulting query belongs to a subset of XQ called SelXQ (Selection Query) that excludes from XQ the rule for output generation. The rewriting algorithm for generic and operation sensitive destabilizers can be found in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF].

While queries are transformed into destabilizers, updates are transformed into the selection query which represents the targets of update operation. The transformation function Targ is defined in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF].

After representing the queries as destabilizers and updates as target queries, a function can translate this unified intermediate representation into a target logical language depending on the chosen intersection testing technique.

INTERSECTION TESTING

Intersection testing uses different static analysis techniques to find the intersection between two structured representations that correspond to a query and an update.

The simplest form of intersection testing for XPath sets is by using heuristics: suffix incompatibility, displacement tests and prefix incompatibility for downward paths [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF]. These techniques have a polynomial time complexity but they work only for a very restricted fragment of downward XPaths.

For downward XPath fragments with child, descendant and wildcard fragments, intersection can be solved in polynomial time by building an automaton for XPath expressions and finding the intersection using product automata and emptiness check [START_REF] Beda | On the intersection of XPath expressions[END_REF]. This solution is accurate but obviously of very limited expressiveness.

To handle more expressive fragments, [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF] proposes to use the Satisfiability Modulo Theory (SMT) approach for intersection analysis using the theory of linear order (N,<). This is done by first transforming selection queries to positive existential first order logic (over trees) formulas. Then these formulas are translated using interval encoding [START_REF] Dehaan | A comprehensive XQuery to SQL translation using dynamic interval encoding[END_REF] and passed to an SMT solver such as Yices [START_REF] Dutertre | The Yices SMT solver[END_REF] to check for independence.

To handle all the fragments of SelXQ queries:

• Selection queries can be transformed into first-order formulas over trees for child, descendant and sibling relations [START_REF] Benedikt | From XQuery to relational logics[END_REF] and intersection analysis reduces to satisfiability which has a non-elementary lower bound for time complexity [START_REF] Vorobyov | An improved lower bound for the elementary theories of trees[END_REF]. These formulas can be checked for disjointness by monadic second order (MSO) satisfiability solvers, like MONA [START_REF] Klarlund | MONA Version 1.4 User Manual[END_REF][START_REF] Genevès | Deciding XPath containment with MSO[END_REF];

• Selection queries can be transformed into a set of XPath expressions which in turn are translated into µ-calculus formulas. The conjunction of these formulas can be checked for satisfiability using a µ-calculus satisfiability solver [START_REF] Genevès | Efficient static analysis of XML paths and types[END_REF][START_REF] Genevès | XML reasoning solver user manual[END_REF].

COMPARATIVE STUDY

We now compare the three mentioned approaches (SMT Solver, MSO Solver and µ-Solver) first from a theoretical perspective, and then from a practical point of view.

Theoretical aspects

Figure 1 illustrates the whole approach and each alternative for performing the intersection test. Vertical arrows correspond to translations which turn a given expression from a source language into an equivalent expression in another target language. The figure also summarizes the theoretical characteristics of each alternative regarding expressivity, accuracy, and complexity. The theoretical complexity of satisfiability on monadic second order formulas is known to be non-elementary whereas it is exponential for simplex based linear arithmetic satisfiability. The complexity of satisfiability on µ-formulas is simple exponential 2 n .

Reduction to Satisfiability modulo order theory requires positive existential first order formulas to be translated into constraints; which is not sufficient to represent negation in qualifiers for example. Mondaic second order logic is equal in expressiveness to µ-logic [START_REF] Genevès | Logics for XML[END_REF].

Practical aspects

We have implemented the destabilizer approach, in Java, to evaluate intersection analysis using the µ-solver. We compared our results with those obtained in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF]. The input to the analysis method consists in an XQuery expression and an XQuery Update Facility update.

The analyzer first transforms the update expression into its corresponding target selection query using Targ method. Then, it transforms queries into query destabilizers using the function ∆ v * which is called on the query expression in the case of a generic destabilizer (or ∪op(∆ v op ) in the case of an operation sensitive destabilizer where op is the set of update operations detected in the input update expression).

Then all XPath expressions are extracted from the query destabilizer and the update target query. Finally, they are passed to the µ-solver that checks the satisfiability of the formula QueryXP aths ∧ U pdateXP aths, where QueryXPaths is the disjunction of the members of the set of XPaths extracted from query destabilizer and UpdateXPaths is the disjunction of the members of the set of XPaths extracted from the update target query.

For example, the following query Q and update U:

Q = for $x in $doc/C return $x/D U = delete $doc/A/B
are independent because none of the extracted path expressions of value destabilizer of Q intersects with the target XPath expressions of U. The following steps denote the whole execution process:

1. The target query is executed on the update U: T arg * (delete $doc/A/B) = ($doc/A/B); On the opposite, Q and U'= delete $doc/C/D/E are not independent because the XPath expression /C/D/E will intersect with /C/D/descendant-or-self::*.

We used the exact same set of 20 Query examples of XMark benchmark [START_REF] Schmidt | XMark: a benchmark for XML data management[END_REF] used by Benedikt and Cheney in their experiments, with the same necessary modifications to fit in the supported query fragments. We automatically generated 4 kinds of updates (rename, insert into, insert before, delete) 1 on the 16 XPath queries (A1-A8, B1-B8) of XPathMark [START_REF] Franceschet | XPathMark: an XPath benchmark for the XMark generated data[END_REF].

We applied this analysis on all the combinations of queries and updates and we compared the mean execution time of the µ-solver with the results found in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF] for the Yices SMT solver.

We used the version of the µ-solver implemented in Java (using JavaBDDs) and shared with Benedikt and Cheney. Experiments are carried out on a laptop with an Intel Processor (3.0 GHz), with 2GB of memory.

Figure 2 compares the running times of the µ-Solver and the SMT-solver. The running times of the SMT-solver (Yices) are taken from [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF]. The running times of the µ-solver carefully followed the method for calculating running times found in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF]. Specifically, each update is tested for independence using the generic analysis with the twenty queries of the XMark benchmark and then the mean time is taken and the results are grouped by the update.

Efficiency. Figures 2 and3 show comparisons between the execution times obtained with the µ-solver with those obtained with the MONA solver and the Yices solver. [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF] finds that Yices is the most efficient in practice, MONA follows and they do not give measurements for the µ-solver whose performance was judged not attractive. Our measurements prove that the µ-solver approach is far more efficient in practice compared to Yices (and obviously to MONA).

An interesting finding was revealed when looking carefully at the time decomposition of the resolution process. This process involves various aspects such as constructing destabilizers, parsing formulas, initializing the BDD library, and the actual resolution time within the solver. It turned out that if we concentrate on the µ-solver time (see Figure 4), leaving aside the other costs, we observe that time spent in the resolution procedure is negligible compared to the overall figures presented in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF]. This gives a clear evidence (somehow counter-intuitive compared to the conclusions of [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF]) that the dominant cost do not necessarily reside in the resolution procedure. We believe that times spent in the resolution procedure better reflect the intrinsic difficulty of each problem instance. Accuracy. Both MONA and the µ-solver approaches can determine exactly whether two selection queries overlap (because they both have the expressivity of MSO, notably encompassing First-Order logic, FO) whereas Positive Existential First-Order logic (EF O + ) can return false negatives (since EF O + is strictly less expressive than FO and thus obviously strictly less expressive than MSO).

Providing MSO expressivity is an unquestionable advantage as this allows capturing regular tree languages (XML schema languages) for which FO expressivity is insufficient.

RELATED WORK

The notion of destabilizers introduced by Benedikt and Cheney [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF] was partly inspired by previous works on XML projection [START_REF] Véronique Benzaken | Type-based XML projection[END_REF], where the goal is to identify nodes that can be deleted without modifying the result of a query (this corresponds to independence problems involving deletion only). As noticed in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF], prior techniques either required a schema [START_REF] Benedikt | Schema-based independence analysis for XML updates[END_REF][START_REF] Véronique Benzaken | Type-based XML projection[END_REF] or apply only to downward fragments of XPath. [START_REF] Ghelli | Commutativity analysis for XML updates[END_REF] proposes a conservative analysis for an XML update language and a theorem that can be used to identify commuting expressions. However a different update language proposal is considered and independence is not addressed.

CONCLUSION

We have revisited the XML query-update independence analysis problem by exploring in depth the approach based on the µ-solver. For that purpose, we have reimplemented a destabilizer's framework for evaluating the relevance of this approach which was neglected in previous studies. We show that performance can be drastically enhanced using the µsolver based approach. Surprisingly, our results show that the best performing approach in practice does not require any loss of precision. This questions systematic search for trade-offs between expressivity and precision.

Figure 1 :

 1 Figure 1: Independence Analysis Framework

2 . 5 .

 25 The Destabilizers rules are applied on the query Q: ∆ v * (for $x in $doc/C return $x/D)= ($doc, $doc/child::*), for $x in $doc/C return ($x/desc-or-self::*, $x/child::*/desc-or-self::*) 3. XPath expressions are extracted from the target query and the result is the set {/child::A/child::B} 4. XPath expressions are extracted from destabilizers and the result is { /self::*, /child::*, /child::C, /child::C/desc-orself::*, /child::C/child::*/desc-or-self::* } The two sets are passed to the µ-solver that indicates the unsatisfiability.

Figure 3 :

 3 Figure 3: µ-solver vs. MONA running times [logarithmic scale].

Figure 4 :

 4 Figure 4: Actual resolution times for the µ-Solver.


Raquel Oliveira
email: raraujo.oliveira@gmail.com

Pierre Genevès
email: pierre.geneves@inria.fr

Nabil Layaïda
email: nabil.layaida@inria.fr

Toward Automated Schema-Directed Code Revision

Keywords: H.2.3 [Database Management]: Languages-Query languages; D.2.4 [Software Engineering]: Software/Program Verification-Validation XML, Schemas, XQuery, Schema evolution 1

Updating XQuery programs in accordance with a change of the input XML schema is known to be a time-consuming and error-prone task. We propose an automatic method aimed at helping developers realign the XQuery program with the new schema. First, we introduce a taxonomy of possible problems induced by a schema change. This allows to differentiate problems according to their severity levels, e.g. errors that require code revision, and semantic changes that should be brought to the developer's attention. Second, we provide the necessary algorithms to detect such problems using a solver that checks satisfiability of XPath expressions.

INTRODUCTION

In document management systems, documents usually encoded in XML are often rendered into output formats (e.g. HTML, SVG, PDF) using transformations, typically written in XSLT or XQuery. 1 XML documents conform to constraints expressed with schemas that continuously change in order to cope with the natural evolution of the entities they describe. However, these changes may break transformations for documents whose structure was described by the original schema.

A frequent scenario consists in an XQuery transformation executed over an XML document (conforming to some schema S in ), generating an XML document that is valid against another schema Sout. For instance, consider a schema describing bibliographical data for a writer (as illustrated in Figure 1a). The schema allows zero or more books, each book having a title of type string and a year of publication of type integer, and some information about its sales. Now consider that this schema S in evolved into a newer version S in (as illustrated in Figure 1b), with three changes: (I) the type of the year is now a string (II) the book is distributed at most once and (III) the city element is removed. against S in , but not valid against S in (because at most one sale is expected in S in ). Instance (b) is allowed by S in whereas it was not allowed by S in , since S in prevented book elements to occur without a least one sale child. The XQuery transformation shown below extracts the sales information for book structures valid against S in . If the book was published in 2012 and was sold in New York, it considers "new" stores (founded in 2010 or later). For other cases, it considers "old" stores too. Finally it returns the sales only for books that were distributed at most once.

¦ ¥

In our scenario, the output document is validated against the schema shown in Figure 3.

Contribution

Our goal is to propose a framework to detect impacts of schema changes on transformations automatically.

TAXONOMY OF ERRORS

We now introduce a taxonomy of impacts on transformations according to various changes brought to a given schema. The taxonomy is divided into two main groups. The first group gathers different errors that can be detected by a joint analysis of the transformations and the input schemas. The second group consists in extending the analysis by taking advantage of the availability of the output schema. Basically, the goal is to check whether the transformation results would still be valid against the output schema. The taxonomy categories are summarized in Table 1. In our setting, the transformation analysis results in one of the two following conclusions: either no problem was detected among the ones we cover in the taxonomy, or a problem is detected, in which case it is properly categorized. We detail each category in the following subsections.

Schema considered

Analysis w.r.t. input schema versions

Type casting problems. Type casting problems can occur in XQuery clauses that bind variables (e.g. for and let clauses). Specifically, a type casting error is detected whenever the schema change results in an assignment of an element with type t1 to a variable with type t2 = t1. For instance, in our motivating example, this problem occurs in the binding between the XPath expression //book/year and the integer variable $y, since the year element is of type string in the new schema S in .

Dead code. A given code portion is dead whenever it is never reached by any execution of the program, for example, the else part of a condition when it is known that the if part always evaluates to true (or the then part whenever the if part is found unsatisfiable). In a XQuery program, there are several places where a dead code can potentially occur, as studied in [START_REF] Genevès | Eliminating dead-code from XQuery programs[END_REF]. We detect errors reported in [START_REF] Genevès | Eliminating dead-code from XQuery programs[END_REF] as well as other categories not covered in [START_REF] Genevès | Eliminating dead-code from XQuery programs[END_REF]. In the motivating example, dead code can be detected in the if expression. Once we detected that this condition always return an empty set (because the city element was removed from the schema), the then part will never be executed.

Redundant code. A code portion is redundant if its execution does not affect the result of the program. It can be safely removed from the program, like a condition that is always evaluated to true. The relevance of the detection of this problem resides on the possibility to propose query rewriting, with the purpose of optimization and/or size reduction of a program. In our motivating example, the XPath qualifier in the return clause becomes redundant following the schema change. In the new schema, the sales element can now occur at most once in the document. As a result, the condition of the qualifier is always true under this schema, making it removable.

Invalid query. We identify as invalid the XPath expressions that are unsatisfiable under the considered schema. Using the satisfiability algorithm proposed in [START_REF] Genevès | Efficient static analysis of XML paths and types[END_REF], we check statically (at compile time) whether an XPath is satisfiable against schema S in . Otherwise, we deduce that the XPath (and subsequently the expression that uses it) is invalid. The XPath used in the if condition of the motivating example is invalid. It is never satisfied given that the city element was removed from the schema.

Different query results. In this category, we are interested in highlighting to the user at compile time the fact that, due to the schema evolution, the result of the query will change unexpectedly. The query will not raise type casting problems, does not contain neither dead nor redundant code, but it will select unexpectedly more (or less) nodes in the input XML document, due to, for example, insertion (or removal) of elements in the XML schema, or changes in the constraints of the elements, or in its content model. In our motivating example, once we remove the city element from the schema, the content model of the store element changes (it is somehow "decreased"). Since store is part of the content model of the element that will be returned, we can conclude that the result of this XQuery is affected by the schema change (knowing that the return clause creates a document consisting of the selected element of the XPath and its content model).

Analysis w.r.t. the output schema

Invalid query results. When the output schema is available (Sout), we can go further and detect at compile time that the changes in the input schema will produce an invalid document with respect to the output schema Sout. First, we review the validation process of the output document before considering the input schema changes. The XQuery of our example returns the sales information of books which were sold at most once. This XQuery is launched on instances of the schema S in of Figure 1a. This schema allows instances of books with at least one sale (< + > constraint at the element sales). When the transformation is executed, only books with exactly one sale will be returned, which is a valid result considering Sout (< + > constraint at the element sales). Now consider the input schema change (II): the book will be distributed at most once (sales? ). Now this schema allows instances of books with no sale. When we run the XQuery transformation, the condition of the return clause will also allow such kind of documents. When considering the output schema of Figure 3 we observe that each book should have at least one sale (< + > constraint at the element sales). So, the XQuery transformation of our example may generate invalid results against Sout.

ERROR DETECTION

We present the analysis technique for detecting errors for each taxonomy category. For this purpose, we develop inference rules as a detection mechanism for a fragment of XQuery defined below.

Considered XQuery fragment

Specifically, we consider the fragment of XQuery whose syntax is defined in Table 2, that uses XPath expressions whose syntax is described in Table 3. In these grammars, n stands for any integer number, v for any variable's name, tag for any string corresponding to the name of a tag and cst for any constant value. For FLWOR expressions, we consider for, let, where and return clauses. The considered fragment captures the most important features for extracting and generating information.

Inference Rules

For each category of the taxonomy, we develop a set of inference rules that are applied recursively. Specifically, we design one inference rule per construct of our XQuery fragment shown on Table 2. A given rule tests for the presence of an error by invoking logical predicates in the premises. A logical predicate corresponds to a property involving XPath queries, schemas and more generally constraints over XML document trees. The truth status of these logical predicates is evaluated using calls to an external XML reasoner such as the one proposed in [START_REF] Genevès | Efficient static analysis of XML paths and types[END_REF]. Depending on the truth status of the properties described in the premises, the conclusion of a rule attaches the detected error to the corresponding XQuery subexpression. We only detail rules for cases where an error is detected, other obvious cases are omitted.

Type casting problems. In order to detect type casting errors in variable bindings of the for and let clauses, we use an environment Γ that keeps track of the type of variable $v. This rule invokes the predicate has different type, that checks if an element selected by an XPath is of type t in the considered schema. This predicate formulates the property that the type of an element returned by the XPath is different from the one expected by the schema.

Redundant code. For checking redundant code, we introduce the predicate removable qualifier. It successively removes qualifiers from the XPath expression one by one and checks for the equivalence with the original one (meaning that such a qualifier is redundant). To check for equivalence, we use the predicate non equivalence(xpath1, xpath2) that is satisfiable iff there exists an element which is selected by one of the XPaths and not by the other one. Invalid query. The rules for detecting invalid queries are based on satisfiability tests for each XPath, directly available in any XML reasoner, that we denote here through the predicates select and type. The rule concludes that a given XQuery expression is invalid with respect to an input schema iff it contains XPath expressions that are unsatisfiable in the presence of the schema (i.e. always empty).

INVQUERY xpath S in ,S in ,Γ ¬select(xpath,type(S in )) S in ,S in ,Γ xpath→ IN V QU ERY
Different query results. For this category, the rules expressed in the table bellow focus on analyzing parts of XQuery expressions that, combined with elements and document constructors, generate content dynamically. For example, in a < if e1 then e2 else e3 > expression, only e2 and e3 are evaluated, since they can generate new content depending on the boolean condition. In the inference rules, we use the predicates new regions and new contents introduced in [START_REF] Genevès | Impact of XML schema evolution[END_REF]. The first one returns true when an XPath selects nodes that were already present in the old schema, but that now appear in different regions of the document, due to the schema changes. The second predicate returns true when the XPath selects elements that already occurred in the old schema, but whose content model has changed. Invalid query results. To detect invalid query results, it is necessary to statically analyze whether the document produced by the transformation validates against the output schema Sout. We know that the structure of the output document is influenced by changes brought to input schema. For example, assume that we launch our XQuery on some document that follows S in of Figure 1a. In this case, the output document will follow the structure described by Sout of the Figure 3.

In order to check if the generated document remains valid against Sout whenever S in changes, we proceed in two steps. First, we abstract over the structure generated by the XQuery transformation using a set of XPath expressions that describe the location of nodes created in the output document. We introduce the predicate selected node that takes an XPath as argument and returns the selected node name (for example, selected node(/a/b/c)=c). Consider the return clause of our motivating example:

return <book>{$s[count(sales)<=1]/sales}</book>
The XPath that abstracts over the generated structure for this return clause would be: /book/sales. In the inference rules above, the construction of an XPath p from the XQuery expression e is denoted as e → p (see table INVRES).

RELATED WORK

Impacts of schema evolutions have been recently investigated in the literature by several authors [START_REF] Velegrakis | Mapping adaptation under evolving schemas[END_REF][START_REF] Necaský | Five-level multi -application schema evolution[END_REF][START_REF] Boukottaya | Schema matching for transforming structured documents[END_REF][START_REF] Curino | Graceful database schema evolution: the PRISM workbench[END_REF][START_REF] Guerrini | Impact of XML schema evolution on valid documents[END_REF][START_REF] Genevès | Impact of XML schema evolution[END_REF].

In [START_REF] Velegrakis | Mapping adaptation under evolving schemas[END_REF] the authors address the problem of schema evolution assuming that a mapping between schemas is provided. In [START_REF] Necaský | Five-level multi -application schema evolution[END_REF] the authors propose a five-level framework (called XCase) to manage XML evolution, but they do not deal with propagation of schema changes at query level. [START_REF] Boukottaya | Schema matching for transforming structured documents[END_REF] is concerned with a structural similarity measure as a step for the automatic inference of a transformation from one schema to another. However the approach is approximate and does not deal with XQuery. The work found in [START_REF] Curino | Graceful database schema evolution: the PRISM workbench[END_REF] addresses evolution in schemas but the process is not fully automatic in the sense that the user must indicate which queries are potentially affected by schema changes. The work found in [START_REF] Guerrini | Impact of XML schema evolution on valid documents[END_REF] deals with revalidation of documents whenever their schema evolves but does not deal with queries. Finally, the present work extends our previous results on evolution restricted to XPath expressions and schemas analysis [START_REF] Genevès | Impact of XML schema evolution[END_REF]. The extension consists in considering a transformation language such as XQuery that can not only select nodes in input documents but also generate output documents. In addition, we analyze the impact of input schema changes over the output generated by the transformation.

CONCLUSION

We highlighted various consequences that schema changes may have on transformations. We presented a new taxonomy of possible problems induced by schema changes. We proposed automated static analysis techniques to detect each category. The analyses are presented through inference rules that operate on a core fragment of XQuery. We believe this is a step toward automated schema-directed code revision techniques for modern document management systems.

Figure 2

 2 gives two document instances. Instance (a) is valid S in =evolved schema

Figure 1 :

 1 Figure 1: Example of a schema evolution.

  instance valid against S in

Figure 2 :

 2 Figure 2: Instances of documents

Figure 3 :

 3 Figure 3: Output schema Sout

e

  ::= () | $v | xpath | $v/xpath | e,e | <tag> e < /tag> | element{e}{e} | if e then e else e | let $v as t := e (where e)? return e | for $v (as t)? in e (where e)? return e t ::= xs:integer | xs:string | xs:boolean Table 2: Syntax of XQuery Programs xpath ::= step | xpath/xpath | xpath[qualifier ] step ::= axis::nameTest qualifier ::= xpath | xpath op cst | count(xpath) op n op ::= < | > | ≤ | ≥ | = | ! = | eq|ne|lt|le|gt|ge axis ::= self | child | parent | descendant | ancestor | following | preceding | following-sibling | preceding-sibling nameTest ::= tag | *

  REDUNDCODE xpath S in ,S in ,Γ removable qualif ier(xpath) S in ,S in ,Γ xpath→ REDU N DCODE

  §

	for $s in doc (" bib . xml ")// book
	let $y as xs : integer := xs : integer ( $s / year )
	where
	if (( $s / sales / store / city = " New York ")
	and ( $y = 2012)) then
	$s / sales / store / foundation >= 2010
	else
	$s / sales / store / foundation >= 1960
	return
	< book >{ $s [ count ( sales ) <=1]/ sales } </ book >

Table 1 :

 1 Summary of the taxonomy

		Acronym	Category
		TYPECAST	Type casting
	Input Schemas	DEADCODE REDUNDCODE Redundant code Dead code
		INVQUERY	Invalid query
		DIFFRES	Different results
	Output Schema	INVRES	Invalid results

Table 3 :

 3 Syntax of XPath Expressions

  The main rule is shown in the table below.

		TYPECAST
	f or	S in ,S in ,Γ,Γ ∪(t,$v) S in ,S in ,Γ,Γ f or $v as t in xpath return e 3 → T Y P ECAST has dif f erent type(xpath,S in ,t)

  The main rules are shown in the table below.

			DIFFRES
	xpath	S in ,S in ,Γ S in ,S in ,Γ	new regions(xpath,S in ,S in ) xpath→ DIF F RES
	xpath	S in ,S in ,Γ S in ,S in ,Γ new contents(xpath,S in ,S in ) xpath→ DIF F RES
	f or	S in ,S in ,Γ	S in ,S in ,Γ∪($v,e 1 ) f or $v in e 1 where e 2 return e 3 → DIF F RES e 3 → DIF F RES

Those XPath expressions are collected during the application of the inference rules. As a second step, we check whether these XPath expressions are unsatisfiable against the output schema (using the "select" predicate), in which case we raise the INVQUERY error.INVRESxpath Γ xpath → /selected node(xpath) seq Γ e 1 → p Γ e 2 → p Γ e 1 ,e 2 → p/f ollowing simbling:: * [p ] tag Γ e → p Γ <tag>e</tag> → /tag/p elem Γ e 1 → p Γ e 2 → p Γ element{e 1 }{e 2 } → /p/p