[Bug 10065] New: [XPath] Rules for matching substitution groups differ from those in formal semantics

http://www.w3.org/Bugs/Public/show_bug.cgi?id=10065

           Summary: [XPath] Rules for matching substitution groups differ
                    from those in formal semantics
           Product: XPath / XQuery / XSLT
           Version: 2nd Edition Recommendation
          Platform: PC
        OS/Version: Windows NT
            Status: NEW
          Severity: normal
          Priority: P2
         Component: XPath
        AssignedTo: jonathan.robie@redhat.com
        ReportedBy: oliver@cbcl.co.uk
         QAContact: public-qt-comments@w3.org


Note that this could either be considered a bug against XPath, or a bug against
Formal Semantics, depending on the resolution.

XPath 2.0 SE and FS 1.0 SE seem to give conflicting definitions for matching
schema elements.


To summarize the differences between the definitions:

Formal Semantics says that an element X matches schema-element(E) if its name,
type and nillability of X match those of an element S which substitutes for E.

XQuery says that an element X matches schema-element(E) if its name matches the
name of an element S which substitutes for E, and if its type and nillability
match those of E.



In particular I am concerned with the following case

define element foo of type xs:anyAtomicType
define element bar substitutes for foo of type xs:integer

and consider the following query:

validate lax { <bar xsi:type="xs:decimal">123</bar> } instance of
schema-element(foo)



Quoting the rules for matching schema types from XPath 2.0 (2.5.4.4):


A SchemaElementTest matches a candidate element node if all three of the
following conditions are satisfied:

1. The name of the candidate node matches the specified ElementName or matches
the name of an element in a substitution group headed by an element named
ElementName.

2. derives-from(AT, ET) is true, where AT is the type annotation of the
candidate node and ET is the schema type declared for element ElementName in
the in-scope element declarations.

3. If the element declaration for ElementName in the in-scope element
declarations is not nillable, then the nilled property of the candidate node is
false.


In this case all 3 conditions are satisfied - bar substitutes for foo, the type
of bar (xs:decimal) is a subtype of the type of foo (xs:anyAtomicType) and
neither element is nilled.  Thus the test should match.


However, I do not believe that formal semantics correctly reflects condition 2.




Consider the dynamic semantics specified by FS.

Firstly, look at the name-lookup judgement  (FS 8.1.3):

statEnv |- ElementName1 substitutes for ElementName2
statEnv |-  ElementName1 of elem/type expands to expanded-QName1
statEnv.elemDecl(expanded-QName1) = define element ElementName1 OptSubstitution
OptNillable TypeReference
-------------------------------------------------------------
statEnv |- ElementName1 name lookup element ElementName2 yields OptNillable
TypeReference

Substituting in our types, I believe

statEnv |- bar name lookup element foo yields xs:integer

And thus taking the rule for matches (FS 8.3.1):

statEnv |- ElementName name lookup ElementType yields OptNillable of type
BaseTypeName
statEnv |- TypeName derives from BaseTypeName
Value1 filter @xsi:nil => SimpleValue
SimpleValue in { (), false }
--------------------------------------------------
statEnv |- element ElementName of type TypeName { Value } matches ElementType

Substitute in our element (replace ElementName with bar, TypeName with
xs:decimal) and ElementType with element foo.

The first line restricts BaseTypeName to xs:integer (as bar name lookup element
foo yields xs:integer)
The second line then does not hold (as xs:decimal derives from xs:integer is
false).

And so formal semantics yields false for the judgement.



The static semantics are also different according to FS, as they use this same
matches judgment.

I believe the type inferred for 

let $node := validate lax { <bar xsi:type="xs:decimal" /> } as node()
return $node/self::schema-element(foo)

is computed as:

(element(foo, xs:anyAtomicType) | element(bar, xs:integer))?

which does not match the type of the value returned when using the rules in
XQuery (element(bar, xs:decimal)).  When using the rules specified in formal
semantics, this produces the empty sequence though, and I believe the rules to
be sound in this respect.




In order to fix these problems we can either move XPath in line with Formal
semantics, or move formal semantics in line with XPath.  Whilst the obvious
answer is "FS is no longer normative", both these specifications were written
to be normative and since both these definitions are consistent with themselves
I see no reason why one should hold more merit that the other.  I know that at
least one implementation implements the rules as stated in FS (XQSharp) and at
least one implementation implements the rules as stated in XPath (Saxon).



To make XPath behave as the Formal Semantics describes, we need to change
2.5.4.4 from


A SchemaElementTest matches a candidate element node if all three of the
following conditions are satisfied:

1. The name of the candidate node matches the specified ElementName or matches
the name of an element in a substitution group headed by an element named
ElementName.

2. derives-from(AT, ET) is true, where AT is the type annotation of the
candidate node and ET is the schema type declared for element ElementName in
the in-scope element declarations.

3. If the element declaration for ElementName in the in-scope element
declarations is not nillable, then the nilled property of the candidate node is
false.


to


A SchemaElementTest matches a candidate element node if all three of the
following conditions are satisfied:

1. The name of the candidate node matches the specified ElementName or matches
the name of an element in a substitution group headed by an element named
ElementName.  Call this element the substituted element.

2. derives-from(AT, ET) is true, where AT is the type annotation of the
candidate node and ET is the schema type declared for the substituted element
in the in-scope element declarations.

3. If the substituted element is not nillable, then the nilled property of the
candidate node is false.




To bring FS in line with XPath I believe the following changes need to be made:

In FS 8.1.3, change the judgement

statEnv |- ElementName1 substitutes for ElementName2
statEnv |-  ElementName1 of elem/type expands to expanded-QName1
statEnv.elemDecl(expanded-QName1) = define element ElementName1 OptSubstitution
OptNillable TypeReference
-------------------------------------------------------------
statEnv |- ElementName1 name lookup element ElementName2 yields OptNillable
TypeReference

to

statEnv |- ElementName1 substitutes for ElementName2
statEnv |-  ElementName2 of elem/type expands to expanded-QName2
statEnv.elemDecl(expanded-QName2) = define element ElementName2 OptSubstitution
OptNillable TypeReference
-------------------------------------------------------------
statEnv |- ElementName1 name lookup element ElementName2 yields OptNillable
TypeReference

Significant changes would also have to be made to the text describing these
judgements.



Personally, I find the FS rules far more intuitive.

-- 
Configure bugmail: http://www.w3.org/Bugs/Public/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are the QA contact for the bug.

Received on Friday, 2 July 2010 11:22:31 UTC