[Bug 6160] New: [FS] 7.1.1 The fs:convert-operand function: incorrect type rules

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

           Summary: [FS] 7.1.1 The fs:convert-operand function: incorrect
                    type rules
           Product: XPath / XQuery / XSLT
           Version: Recommendation
          Platform: All
        OS/Version: All
            Status: NEW
          Severity: normal
          Priority: P2
         Component: Formal Semantics
        AssignedTo: jmdyck@ibiblio.org
        ReportedBy: jmdyck@ibiblio.org
         QAContact: public-qt-comments@w3.org


(This bug is extracted from Bug 5915 comment #2, where it's secondary to
that bug's main point.)

Consider the query:

    let $x := if (1) then text{"42"} else 3.14
    return -$x

which normalizes to something like:

    let $x := if (1) then text{"42"} else 3.14
    return fs:unary-minus( fs:convert-operand( fn:data($x), 1.0E0 ) )

We can infer the following static types:

    text{"42"}                        : text?
    3.14                              : xs:decimal
    if (1) then text{"42"} else 3.14  : text? | xs:decimal
    $x                                : text? | xs:decimal
    fn:data($x)                       : (xs:untypedAtomic | xs:decimal)?

The last of these types becomes 'Type1' in the Static Type Analysis rules
for fs:convert-operand (FS 7.1.1). Note that
    Type1 <: xs:untypedAtomic?
does not hold (because of the presence of xs:decimal in Type1), and so
only the first of the four rules applies:

    statEnv |- not(Type1 <: xs:untypedAtomic?)
    ------------------------------------------------------------
    statEnv |- (FS-URI,"convert-operand")( Type1, Type2) : Type1

Thus the static type of the call to fs:convert-operand is also inferred to
be:
    (xs:untypedAtomic | xs:decimal)?

On the other hand, we know that dynamically:
    $x is bound to a text node,
    fn:data($x) yields "42" as an xs:untypedAtomic, and
    fs:convert-operand returns that value cast to xs:double.

Since the value of the call does not belong to the static type for
the call, this is a violation of type soundness. The rules for
fs:convert-operand need to be changed to properly handle such cases.


-- 
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 Monday, 13 October 2008 21:25:08 UTC