Re: Example [Was: Two things to strengthen the spec]

[Murata Makoto <mura034@attglobal.net>]

Michael Fitzgerald wrote:

> OK. James and Makoto are the doorkeepers for the spec. I was merely leaning
> on the doorbell. I shall relent.

Oh, please don't give up easily!

I have created an example.  It can be an informative appendix of the specification.
 How do you feel about this?

1) An instance document in the XML syntax

<?xml version="1.0"?>
<foo xmlns=""
 ><pre1:bar1 xmlns:pre1="http://n1"
/><pre2:bar2 xmlns:pre2="http://n2"
/></foo>

Note: The root element has two child elements but has no 
child strings.

3) This instance document in the data model

This document is represented by an element foo
containing two child elements.

The root element e0 is represented by

	element(name("", foo), cx0, {}, {e1, e2}), 

where cx0 is a context {"" -> ""} and e1 (e2) represent the first
(resp., second) child element.

e1

	element(name("http://n1", bar1), cx1, {}, {})

e2
	element(name("http://n2", bar2), cx2, {}, {})

where cx1 and cx2 are contexts {"" -> "", pre1 -> "http://n1"} and
{"" -> "", pre2 -> "http://n2"}, respectively.  (We omit the base 
URI in this example.)

3) schema

This grammar is normalized as defined in Section 5 and satisfies the
restrictions in Section 7.

<grammar ns="" xmlns="http://relaxng.org/ns/structure/0.9">
  <start>
    <ref name="foo"/>
  </start>

<define name="foo">
  <element>
    <name>foo</name>
    <group>
      <ref name="bar1"/>
      <ref name="bar2"/>
    </group>
  </element>
</define>

<define name="bar1">
  <element>
    <name ns="http://n1">bar1</name>
    <empty/>
  </element>
</define>

<define name="bar2">
  <element>
    <name ns="http://n2">bar2</name>
    <empty/>
  </element>
</define>
</grammar>

4) Validation

Let nameclass nc1 = <name ns="http://n1">bar1</name> and 
nameclass nc2 = <name ns="http://n2">bar2</name>.

Then, by the inference rule (name) in 6.1, we have

	name("http://n1", "bar1") in nc1

and 
	name("http://n2", "bar2") in nc2 .

By the inference rule (empty) in 6.2.3, we have

	cx1 |= {};() = <empty/> => {};{}

and 

	cx2 |= {};() = <empty/> => {};{}

Since 

	deref(bar1) = 
	  <element>
	    <name ns="http://n1">bar1</name>
	    <empty/>
	  </element>

we have

	cx0 |-   {}; e1 =~ <ref name="bar1"/> => {}; {}

by applying the inference rule (element) in 6.2.8.   Note that 
we have chosen cx0, since any context is allowed.

Likewise, we have 

	cx0 |-   {}; e2 =~ <ref name="bar2"/>  => {}; {}

By the inference rule (group) in 6.2.1, we have 

	cx0 |-   {}; (e1, e2)
	           =~ <group><ref name="bar1"/><ref name="bar2"/></group>
			=> {}; {}

Since

deref(foo) = <element><name>foo</name>
              <group>
                <ref name="bar1"/>
                <ref name="bar2"/>
              </group>
             </element>
,

we have 

	cx3 |- {}; element(name("", foo), cx0, {}, {e1, e2}) =~ 
                     <ref name="foo"/> => {}; {}

by the the inference rule (element) in 6.2.8 again.  Here
cx3 is an arbitrary context.

Finally, since start() = <ref name="foo"/>, we can apply the 
inference rule (valid) in 6.4 and obtain

	valid(e0)


Cheers,

Makoto
 
Internet: mura034@attglobal.net
Nifty: VEQ00625