[dsdl-discuss] First draft of Schematron spec (Schematron in one defun)

Finally, I have a rough draft of the Schematron spec at
    http://www.topologi.com/resources/tmp/schematron-is.xml

This draft has an attempt at the basic formal semantics, and
I especially welcome any corrections on these. The key passages
are excerpted below to give you the flavour--hopefully, the
UTF-8 will not have been corrupted in email transit.
(I follow RELAX NG in first removing sugar such as abstract
patterns and abstract rules, which simplified the formal spec.)

The draft is valid against James' schema, except that I need for
<note>s to contain <ul>s and <pre> to allow xml:space="preserve"
(so that Mozilla and IE display <pre> with layout intact.)

If anyone cares to typeset it to PDF and distribute it for initial
comments, please feel free. Alternatively, where are the latest
versions of the schemas and tools please? Is there a package
available?

Cheers
Rick Jelliffe

========================================
Definitions

good schema
    a correct schema with queries which
    terminate, and which does not
    add constraints to those of the natural language
    assertions. Note: it is not always possible to compute
    that a schema is good.

...
========================================
Predicate Logic

This draft uses predicate logic to express the semantics of
Schematron schema. The following functions are defined:

-----------------------------------------------------------
∈
 is member of,
 an infix relation
 
NOTE: The more familiar term "is element of" is not used,
to avoid confusion with XML elements.

 Where y is an element in a simplified schema, x ∈ y
 is defined here as the
 child::x path from context of subject y
 as defined by XSLT.

 Where y is the instance being validated, x ∈ y
 is defined here as all the subjects (information items) in the instance
 that can be accessed by the query language,
 as speficied in the query language binding.

 Where y is the name of the active active-phase,
 one of the following is true:
     x ∈ y is defined here as the path //sch:pattern
     when y has the special value #ALL

     x ∈ y is defined here as the path
     //sch:pattern[@id=/sch:schema/@default-phase]
     when the y has the special value #DEFAULT

     Otherwise x ∈ y is defined here as the path
     ../sch:pattern[@id=//sch:phase[id="y"]/active/@pattern]
     where y is a name.

-----------------------------------------------------------
position( r )
 the XPath function position() of a rule r in its parent pattern

-----------------------------------------------------------
match ( r, s, d )
 a function returning boolean provided by the query language binding:
 it returns true iff the subject s from the document d
 matches the context expression of rule r
  
-----------------------------------------------------------
assert ( a, s, d)
 a function returning boolean
 provided by the query language binding: it returns true
 iff the assertion a is true when applied to
 the subject s from the document d

-----------------------------------------------------------
...
========================================
Schema Semantics

This clause gives the semantics of a good schema
that has been transformed into the simple syntax.

A good schema with no use of keys or variables
satisfies the following predicate:

  ∃ ( instance, schema, active-phase ),
  ∀( subject, pattern, rule, assertion ) :
   subject ∈ instance,
    pattern ∈ schema,
    pattern ∈ active-phase,
    rule ∈ pattern,
    assertion ∈ rule :
      match ( rule, subject, instance )
      ∧ ( ∀(previous-rule ) :
        previous-rule ∈ pattern,
        position (previous-rule ) &lt; position( rule ) :
         ¬ ( match ( previous-rule, subject, instance )))
      ⇒ assert ( assertion, subject, instance ) = true

NOTE: In natural language, that is
"There exists an instance, schema and active-phase combination
where, for each subject, pattern, rule and assertion
(the subject being a member of that instance,
the pattern being a member of that schema,
the pattern being a member of that active-phase,
the rule being a member of that pattern,
the assertion being a member of that rule),
the following is true:
if the subject in an instance
matches the rule, and that subject has not
been matched by a previous rule in the same pattern,
then the particular assertion
evaluates to true when applied to the particular subject
and instance."

--
DSDL members discussion list
To unsubscribe, please send a message with the
command  "unsubscribe" to dsdl-discuss-request@dsdl.org
(mailto:dsdl-discuss-request@dsdl.org?Subject=unsubscribe)