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

Yüklə 1,17 Mb.
ö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 © 2020
rəhbərliyinə müraciət

    Ana səhifə