XPath Formal Semantics and Beyond: a Coq based approach

Abstract : XPath was introduced as the standard language for addressing parts of XML documents, and has been widely adopted by practioners and theoreticaly studied. We aim at building a logical framework for formal study and analysis of XPath and have to face the combinatorial complexity of formal proofs caused by XPath expressive power. We chose the Coq proof assistant and its powerful inductive constructions to rigorously investigate XPath peculiarities. We focus in this paper on a basic modeling of XPath syntax and semantics, and make two contributions. First, we propose a new formal semantics, which is an interpretation of paths as first order logic propositions that turned out to greatly simplify our formal proofs. Second, we formally prove that this new interpretation is equivalent to previously known XPath denotational semantics, opening perspectives for more ambitious mathematical characterizations. We illustrate our Coq based model through several examples and we develop a formal proof of a simple yet significant XPath property that compares quite favorably to a former informal proof.
Type de document :
Communication dans un congrès
Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logic: TPHOLs 2004, Aug 2004, Utah, United States. University of Utah, pp.181-198, 2004
Liste complète des métadonnées


https://hal.inria.fr/inria-00423372
Contributeur : Vincent Quint <>
Soumis le : vendredi 9 octobre 2009 - 16:19:08
Dernière modification le : vendredi 27 novembre 2009 - 16:18:15
Document(s) archivé(s) le : mercredi 16 juin 2010 - 00:34:17

Fichier

tphols2004.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00423372, version 1

Collections

Citation

Pierre Genevès, Jean-Yves Vion-Dury. XPath Formal Semantics and Beyond: a Coq based approach. Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logic: TPHOLs 2004, Aug 2004, Utah, United States. University of Utah, pp.181-198, 2004. <inria-00423372>

Partager

Métriques

Consultations de
la notice

217

Téléchargements du document

112