Adventures in Formal Methods at W3C: The xquery 0 and xpath 0 Formal Semantics Jerome Simeon, ibm



Yüklə 1,17 Mb.
tarix23.06.2017
ölçüsü1,17 Mb.


Adventures in Formal Methods at W3C: The XQuery 1.0 and XPath 2.0 Formal Semantics

  • Jerome Simeon, IBM


A Formal Semantics is Controversial

  • Famous computer scientist #1:

  • << The XQuery Formal Semantics is unreadable, and you should just use english. >>

  • Famous computer scientist #2:

  • << I couldn’t understand how XQuery works until I read its formal semantics >>



A Formal Semantics is Useful

  • XQuery 1.0 requirements: A language and an algebra

    • Relational algebra was a success: simple core design, basis for optimization, countless research advances over 30 years of history
  • Support for Static Analysis over XQuery 1.0:

    • Static Typing Feature calculate type of expressions at compile time
    • Soundness theorem: every XML data processed by an expression will have the type infered (or a subtype)
  • Deeper understanding of XQuery 1.0 semantics (translation effect):

    • Numerous bugs in english specification found (notably related to types)
    • Exposes unnecessary complexity and opportunities for consolidation
  • Build the language on solid foundations to facilitate future evolutions



XQuery 1.0 and XPath 2.0 Formal Semantics



XQuery Processing Model



English vs. Formal Specification



Formal Specification: One Example



Formal Specification as an Implementation Guide



Lessons Learned

  • A formal specification is a large investment:

  • Important to know what not to formalize:

    • In XQuery: Namespace resolution, validate expression (see XML Schema)…
  • Audience is not everyone:

  • Benefits are numerous, during the specification, and after:




Yüklə 1,17 Mb.

Dostları ilə paylaş:




Verilənlər bazası müəlliflik hüququ ilə müdafiə olunur ©www.azkurs.org 2020
rəhbərliyinə müraciət

    Ana səhifə