[Bug 6625] New: [FS] Type unsoundness of axis expressions involving nillable elements substitutable for non-nillable elements

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

           Summary: [FS] Type unsoundness of axis expressions involving
                    nillable elements substitutable for non-nillable
                    elements
           Product: XPath / XQuery / XSLT
           Version: Candidate Recommendation
          Platform: PC
        OS/Version: Windows NT
            Status: NEW
          Severity: normal
          Priority: P2
         Component: Formal Semantics
        AssignedTo: jmdyck@ibiblio.org
        ReportedBy: oliver@cbcl.co.uk
         QAContact: public-qt-comments@w3.org


Start with the following schema:

<schema targetNamespace="http://www.xqsharp.com/test"
        xmlns:t="http://www.xqsharp.com/test"
        xmlns="http://www.w3.org/2001/XMLSchema">

  <element name="head" type="string" />

  <element name="sub" substitutionGroup="t:head" nillable="true" />

  <element name="root">
    <complexType>
      <sequence>
        <element ref="t:head" />
      </sequence>
    </complexType>
  </element>

</schema>


which looks something like this when translated to the XQuery type system:

define element head of type xs:string;
define element sub substitutes head nillable of type xs:string;
define type fs:anon1 { element head }
define element root of type fs:anon1


now consider the following query:

import schema namespace t="http://www.xqsharp.com/test";

let $root as schema-element(t:root) := (validate{ . })/t:root
return $root/node()


Let us compute the static type of this query.

$root has static type element t:root


According to the revised judgements given in bug 4189, comment 4:

Definition = define type fs:anon1 { element head }
inheritance due to  is empty
element head opt-mixes to element head
type definitions derived from fs:anon1 are empty
------------------------------------------------
union interpretation of define type fs:anon1 { element head } is element head


and again, from bug 4189, comment 4:

fs:anon1 of elem/type expands to fs:anon1
statEnv.typeDefn(fs:anon1) = define type fs:anon1 { element head }
union interpretation of define type fs:anon1 { element head } is element head
element head adjusts to (BuiltInAttributes, element head) &
processing-instruction* & comment*
------------------------------------------------
element head of elem/type expands to (BuiltInAttributes, element head) &
processing-instruction* & comment*

(where I have not bothered to expand out the built in attributes)


thus (from the first rule in FS 8.2.2.1.3):
element root type lookup fs:anon1
fs:anon1 expands to (BuiltInAttributes, element head) & processing-instruction*
& comment*
element head has node content (element head & processing-instruction* &
comment*)
-------------------------------------------
axis child:: of element root : element head & processing-instruction* &
comment*


and finally (FS 8.2.3.1.2):

test node() with PrincipalNodeKind of element head : element head


Skipping the rest of the expansion/judgements we end up with

$root/node() : element head


Now take take the following context document:
<root xmlns="http://www.xqsharp.com/test"
      xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
  <sub xsi:nil="true" />
</root>

The result of the query is the nilled sub element, but this does not match the
static type, since element head is not nillable.


-- 
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 Wednesday, 25 February 2009 17:02:42 UTC