OASIS Mailing List ArchivesView the OASIS mailing list archive below
or browse/search using MarkMail.

 


Help: OASIS Mailing Lists Help | MarkMail Help

relax-ng message

[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [Elist Home]


Subject: Formal Semantics


I've done an inference-rule style formal semantics (like XML Schema Formal
Description) for RELAX NG (this is the approximate equivalent of section 4
of the TREX spec):

http://www.thaiopensource.com/relaxng/proofsystem.html

You can also get the .xml and .xsl files used to generate this. I've used
semantic markup so it will be easy to completely change the notation.

The inference rule notation can look a little daunting if you haven't seen
it before, but it's really quite easy.  An inference rule says that if all
the judgements above the line are true, then the judgment below the line is.
All the variables occurring in the rule are implicitly universally
quantified.

Look at the (choice 1) rule as an example.  Translated into English, this
says:

For any environment E, for any namespace map ns, for any attribute bag a,
for any mixed sequence m, for any pattern p1, for any pattern p2, for any
key bag k, for any key reference bag kr, if, with respect to E and ns, a and
m match p1 generating k and kr, then, with respect to E and ns, a and m
match <choice>p1 p2</choice> generating k and kr.

James







[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [Elist Home]


Powered by eList eXpress LLC