This is an archived snapshot of W3C's public bugzilla bug tracker, decommissioned in April 2019. Please see the home page for more details.

Bug 5254 - [FS] Validate has inconsistent static and dynamic types
Summary: [FS] Validate has inconsistent static and dynamic types
Status: CLOSED FIXED
Alias: None
Product: XPath / XQuery / XSLT
Classification: Unclassified
Component: Formal Semantics 1.0 (show other bugs)
Version: Recommendation
Hardware: PC Windows XP
: P2 normal
Target Milestone: ---
Assignee: Michael Dyck
QA Contact: Mailing list for public feedback on specs from XSL and XML Query WGs
URL:
Whiteboard:
Keywords:
Depends on:
Blocks:
 
Reported: 2007-11-06 10:48 UTC by Nick Jones
Modified: 2009-02-16 07:42 UTC (History)
0 users

See Also:


Attachments

Description Nick Jones 2007-11-06 10:48:15 UTC
In FS 4.13 the static type analysis for validate expressions can only ever be a union of element types.

But in FS 4.13.2 the validate expression can yield a document rather than an element.

I think the fix would be to split the static type analysis rule into two. One for elements, the other for documents.

statEnv |-  Expr : Type
statEnv |-  Type <: (element)
statEnv |-  prime(Type) = ElementType1 | ... | ElementTypen
.
(same as current rule)
.
statEnv |-  validate ValidationMode { Expr } : Type1


statEnv |-  Expr : Type
statEnv |-  Type <: (document {ElementType})
statEnv |-  prime(ElementType) = ElementType1 | ... | ElementTypen
.
(same as current rule)
.
statEnv |-  validate ValidationMode { Expr } : document {Type1}
Comment 1 Michael Dyck 2008-01-18 06:54:31 UTC
I agree that there's a problem, and I agree with your approach to a solution.
However, the original rule has some additional bugs that also need to be fixed:

1. The type 'element' should be 'element *'. (See Bug 3269.)

2. The earlier and later occurrences of ElementTypei should be distinct.

3. Requiring Type <: document { ElementType } is too restrictive, because
   ElementType cannot be bound to a type involving
   (a) processing-instruction or comment types, or
   (b) a union of element types.

Points 1, 2, and 3a are all easy to fix, but I'm not sure what to do about 3b.
Comment 2 Nick Jones 2008-01-22 13:06:21 UTC
> 3. Requiring Type <: document { ElementType } is too restrictive, because
>    ElementType cannot be bound to a type involving
>    (a) processing-instruction or comment types, or
>    (b) a union of element types.
> 
I think "ElementType" isn't actually an ElementType, it was just an unfortunately chosen name. If it is changed to "Type_Element" or something then I think the rule is valid.

The prime(Type_Element) = ElementType1 | .... | ElementTypen should cover the union case.
Comment 3 Michael Dyck 2008-01-22 18:02:02 UTC
(In reply to comment #2)
> I think "ElementType" isn't actually an ElementType, it was just an
> unfortunately chosen name.

That could be, though I somewhat doubt it.

> If it is changed to "Type_Element" or something then I think
> the rule is valid.
> 
> The prime(Type_Element) = ElementType1 | .... | ElementTypen should cover the
> union case.

But then:
1) It incorrectly allows multiple elements in the document content.
2) It doesn't allow processing-instructions or comments.
3) Given a binding for Type_Element that satisfies the rule, there are (infinitely?) many supertypes of it (and possibly some subtypes of it) that also satisfy the rule, and that lead to different types for the validate expression.
Comment 4 Michael Dyck 2009-02-01 00:31:14 UTC
It occurred to me that splitting FS 4.13 / STA / rule 1 into a rule for
    Type <: element
and a rule for
    Type <: document { ... }
woldn't allow for a Type that was a union of (subtypes of) those two
possibilities.  After some thought, I'm instead proposing to replace that
rule with the following set of rules (leaving out "statEnv |-" here for
brevity), which I think handle all problems raised above.

    Expr : Type
    Type <: element * |
            document { element * & (processing-instruction * | comment)* }
    Type with mode ValidationMode unites to TypeU
    ----------------------------------------------------
    validate ValidationMode { Expr } : TypeU


    prime( Type ) = FormalItemType1 | ... | FormalItemTypen
    FormalItemType1 with mode ValidationMode resolves to FormalItemType1'
    ...
    FormalItemTypen with mode ValidationMode resolves to FormalItemTypen'
    FormalItemType1' | ... | FormalItemTypen' = TypeU
    ----------------------------------------------
    Type with mode ValidationMode unites to TypeU


    DocumentType = document { Type }
    Type with mode ValidationMode unites to TypeU
    ----------------------------------------------------
    DocumentType with mode ValidationMode resolves to document { TypeU }


    ElementType = element ElementNameOrWildcard OptTypeSpecifier
    ElementNameOrWildcard with mode ValidationMode resolves to ElementType'
    ----------------------------------------------------
    ElementType with mode ValidationMode resolves to ElementType'


    ----------------------------------------------------
    ProcessingInstructionType with mode ValidationMode resolves to none


    ----------------------------------------------------
    comment with mode ValidationMode resolves to none

Comment 5 Nick Jones 2009-02-02 11:06:19 UTC
That looks good to me, so I'm happy to close if no one else has a problem with it.
Comment 6 Michael Dyck 2009-02-02 18:58:23 UTC
Well, it would need to be approved by the WG first.
Comment 7 Michael Dyck 2009-02-04 06:44:32 UTC
At their joint meeting this morning, the XQuery and XSL WGs approved the proposal in comment #4. Consequently I'm marking this issue resolved-FIXED. Since you have already expressed your approval of the proposal, I will also take the liberty of closing the issue.
Comment 8 Michael Dyck 2009-02-16 07:42:50 UTC
This issue has been entered as FS erratum E058, and the proposed fixes have
been committed to the source files for the next edition of the FS document.
(Mind you, I made some editorial changes to the new judgment forms, to
reduce confusion with the judgment defined in 8.6.1.)