×

zbMATH — the first resource for mathematics

Satisfiability of constraint specifications on XML documents. (English) Zbl 1321.68352
Martí-Oliet, Narciso (ed.) et al., Logic, rewriting, and concurrency. Essays dedicated to José Meseguer on the occasion of his 65th birthday. Cham: Springer (ISBN 978-3-319-23164-8/pbk; 978-3-319-23165-5/ebook). Lecture Notes in Computer Science 9200, 539-561 (2015).
Summary: Jose Meseguer is one of the earliest contributors in the area of Algebraic Specification. In this paper, which we are happy to dedicate to him on the occasion of his 65th birthday, we use ideas and methods coming from that area with the aim of presenting an approach for the specification of the structure of classes of XML documents and for reasoning about them. More precisely, we specify the structure of documents using sets of constraints that are based on XPath and we present inference rules that are shown to define a sound and complete refutation procedure for checking satisfiability of a given specification using tableaux.
For the entire collection see [Zbl 1319.68011].

MSC:
68Q65 Abstract data types; algebraic specification
03B70 Logic in computer science
68Q42 Grammars and rewriting systems
Software:
XPath; XQuery
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Albors, J., Navarro, M.: SpecSatisfiabilityTool: a tool for testing the satisfiability of specifications on XML documents. In: Proceedings of PROLE 2014, EPTCS, vol. 173, pp. 27–40 (2015) · doi:10.4204/EPTCS.173.3
[2] Alpuente, M., Ballis, D., Falaschi, M.: Automated verification of web sites using partial rewriting. Softw. Tools Technol. Transf. 8, 565–585 (2006) · Zbl 05075118 · doi:10.1007/s10009-006-0009-7
[3] Benedikt, M., Fan, W., Geerts, F.: XPath satisfiability in the presence of DTDs. JACM 55, 2 (2008) · Zbl 1326.68154 · doi:10.1145/1346330.1346333
[4] Benedikt, M., Koch, C.: XPath leashed. ACM Comput. Surv. 41, 1 (2008) · doi:10.1145/1456650.1456653
[5] Bidoit, N., Colazzo D.: Testing XML constraint satisfiability. In: Proceedings of the International Workshop on Hybrid Logic (HyLo 2006), ENTCS, vol. 174(6), pp. 45–61 (2007) · Zbl 1278.68074 · doi:10.1016/j.entcs.2006.11.025
[6] Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. Comput. Sci. 19(2), 245–296 (2009) · Zbl 1168.68022 · doi:10.1017/S0960129508007202
[7] Habel A., Radke H.: Expressiveness of graph conditions with variables. In: International Colloquium on Graph and Model Transformation GraMoT 2010, ECEASST, vol. 30 (2010)
[8] Hähnle, R.: Tableaux and related methods. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 100–178. Elsevier, Amsterdam (2001) · Zbl 1011.68125
[9] Jelliffe, R.: Schematron, Internet Document. http://xml.ascc.net/resource/schematron/
[10] Kilpelainen, P., Mannila, H.: Ordered and unordered tree inclusion. SIAM J. Comput. Arch. 24(2), 340–356 (1995) · Zbl 0827.68050 · doi:10.1137/S0097539791218202
[11] Miklau, G., Suciu, D.: Containment and equivalence for a fragment of XPath. JACM 51(1), 2–45 (2004) · Zbl 1316.68047 · doi:10.1145/962446.962448
[12] Nentwich, C., Emmerich, W., Finkelstein, A., Ellmer, E.: Flexible consistency checking. ACM Trans. Softw. Eng. Methodol. 12(1), 28–63 (2003) · Zbl 05459528 · doi:10.1145/839268.839271
[13] Navarro, M., Orejas, F.: A refutation procedure for proving satisfiability of constraint specifications on XML documents. In: SCSS 2014, EasyChair EPiC series, vol. 30, pp. 47–61 (2014)
[14] Orejas, F.: Symbolic graphs for attributed graph constraints. J. Symb. Comput. 46(3), 294–315 (2011) · Zbl 1298.68121 · doi:10.1016/j.jsc.2010.09.009
[15] Orejas, F., Ehrig, H., Prange, U.: A logic of graph constraints. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 179–198. Springer, Heidelberg (2008) · Zbl 1171.68516 · doi:10.1007/978-3-540-78743-3_14
[16] Orejas, F., Ehrig, H., Prange, U.: Reasoning with graph constraints. Formal Asp. Comput. 22(3–4), 385–422 (2010) · Zbl 1209.68381 · doi:10.1007/s00165-009-0116-9
[17] World WIDE WEB CONSORTIUM: XML path language (XPath) recommendation (1999). http://www.w3c.org/TR/XPath/
[18] World WIDE WEB CONSORTIUM: XSL transformations (XSLT). W3C recommendation version 1.0 (1999). http://www.w3.org/TR/xslt
[19] World WIDE WEB CONSORTIUM: XML schema part 0: Primer. W3C recommendation (2001). http://www.w3c.org/XML/Schema
[20] World WIDE WEB CONSORTIUM: XQuery 1.0 and XPath 2.0 formal semantics. W3C working draft (2002). http://www.w3.org/TR/query-algebra/
[21] WORLD WIDE WEB CONSORTIUM: XML path language (XPath) 2.0 (2007)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.