Verification of tree updates for optimization
| Autor: | Angela Bonifati, Michael Benedikt, Sergio Flesca, Avinash Vyas |
|---|---|
| Předmět: | |
| Zdroj: | Scopus-Elsevier Computer Aided Verification ISBN: 9783540272311 CAV Lecture notes in computer science-(2005). info:cnr-pdr/source/autori:Bonifati Angela, Benedikt Michael, Flesca Sergio, Vyas Avinash/titolo:Verification of Tree Updates for Optimization/doi:/rivista:Lecture notes in computer science/anno:2005/pagina_da:0/pagina_a:0/intervallo_pagine:0/volume |
| Popis: | With the rise of XML as a standard format for representing tree-shaped data, new programming tools have emerged for specifying transformations to tree-like structures. A recent example along this line are the update languages of [16,15,8] which add tree update primitives on top of the declarative query languages XPath and XQuery. These tree update languages use a “snapshot semantics”, in which all querying is performed first, after which a generated sequence of concrete updates is performed in a fixed order determined by query evaluation. In order to gain efficiency, one would prefer to perform updates as soon as they are generated, before further querying. This motivates a specific verification problem: given a tree update program, determine whether generated updates can be performed before all querying is completed. We formalize this notion, which we call “Binding Independence”. We give an algorithm to verify that a tree update program is Binding Independent, and show how this analysis can be used to produce optimized evaluation orderings that significantly reduce processing time. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|