[Bug 6683] New: [FS] Types unsound for nillable element tests (and some minor editorial issues).

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

           Summary: [FS] Types unsound for nillable element tests (and some
                    minor editorial issues).
           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


Consider the following element test:

$axis/self:element(*, myString?)

where myString is a type derived from xs:string
and $axis has static type element(e, xs:string).


Clearly $axis can contain an element with name e and type xs:myString, which
matches the element test, and so the static type of this expression should not
be empty.

Lets look at the rules given in formal semantics (8.2.3.1.2)

The first rule reads:

[ElementTest]sequencetype = ElementType
statEnv |-  Type1 <: ElementType
----------------------------------------------------------
statEnv |-  test ElementTest with element of Type1 : Type1


ElementType is element * nillable of type myString
Type1       is element e of type xs:string

Type1 <: ElementType is false since the content of an element can contain an
xs:string that is not a myString, so this does not apply.


The second rule reads:

[ElementTest]sequencetype = ElementType
statEnv |-  ElementType <: Type1
-----------------------------------------------------------------
statEnv |-  test ElementTest with element of Type1 : ElementType?

ElementType <: Type1 is false since a value of ElementType can be nillable, and
a value of Type1 can not.


The third rule reads:

[ElementTest]sequencetype = element ElementName1 TypeSpecifier1
statEnv |-  TypeSpecifier1 expands to Type1
statEnv |-  TypeSpecifier2 expands to Type2
statEnv |-  Type2 <: Type1
-----------------------------------------------------------------------------
statEnv |-  test ElementTest with element of element TypeSpecifier2 : element
ElementName1 TypeSpecifier2?

The bottom line should probably say "element of element * TypeSpecifier2"), but
this is an editorial issue.

Even if we do apply this for ElementName1 equal to star we get Type1 =
xs:myString? and Type2 = xs:string, so Type2 <: Type1 is false and this rule
does not apply.


The fourth rule reads:

[ElementTest]sequencetype = element TypeSpecifier1
statEnv |-  TypeSpecifier1 expands to Type1
statEnv |-  TypeSpecifier2 expands to Type2
statEnv |-  Type1 <: Type2
------------------------------------------------------------------------------
statEnv |-  test ElementTest with element of element ElementName2
TypeSpecifier2 : element ElementName2 TypeSpecifier1?

Similarly to above the first line should say "element * TypeSpecifier1, but
again this is beside the point of this bug report.

For the same reasons as the previous rule, this rule does not apply.


Finally we reach rule 5:

[ElementTest]sequencetype = element ElementNameOrWildcard1 TypeSpecifier1
statEnv |-  not(element ElementNameOrWildcard1 TypeSpecifier1 <: element
ElementNameOrWildcard2 TypeSpecifier2)
statEnv |-  not(element ElementNameOrWildcard2 TypeSpecifier2 <: element
ElementNameOrWildcard1 TypeSpecifier1)
statEnv |-  TypeSpecifier1 expands to Type1
statEnv |-  TypeSpecifier2 expands to Type2
statEnv |-  not(Type1 <: Type2)
statEnv |-  not(Type2 <: Type1)
statEnv |-  test ElementTest with element of element ElementNameOrWildcard2
TypeSpecifier2 : empty

There is another very minor editorial issue with this rule - there should not
be a space between ElementNameOrWildcard and the subscripted 1 or 2.

This case is indeed the negation of all the previous cases, and so this rule
applies and we obtain static type ().


As stated above, this type is not compatible with run time semantics.

We should have probably inferred the type element(e, myString)?


-- 
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, 11 March 2009 11:22:48 UTC