xml-dev - RE: XML Schema in Z ?

[johns@syscore.com (John F. Schlesinger)]

Robert wrote:
"A suggestion: in parallel with anything else you do, re-express the Schema
spec in a  mathematical specification language such as VDM or Z. Publish a
mathematically annotated  version of the spec."

It is interesting to suggest creating a Z specification of the XML Schema
specification as this would be the first time I'd have seen a Z
specification of a specification.

What a Z specification does is, firstly, to model (mathematically) the state
of a system. Secondly it models the operations against that state. Z ensures
that all operations take the state from a consistent state to another
consistent state. Z also determines the start and end conditions for each
operation and so specifies complete operations (that is, it models all ways
the operation can fail as well as succeed). Finally, Z requires the
specifier to prove that there is an initial state.

I could imagine a Z spec of a validating XML Schema parser, but I'm not sure
what could be done with the specification itself. What is the state? What
are the operations? What would be the initial state?

Yours,
John F Schlesinger
SysCore Solutions
212 619 5200 x 219
917 886 5895 Mobile

-----Original Message-----
From: Robert Worden [mailto:rworden@dial.pipex.com]
Sent: Thursday, July 27, 2000 4:40 AM
To: xml-dev@lists.xml.org
Subject: XML Schema in Z ?


In response to Jonathan Robie's question: what should the Schema WG do
next?

A suggestion: in parallel with anything else you do, re-express the Schema
spec in a  mathematical specification language such as VDM or Z. Publish a
mathematically annotated  version of the spec.

What would Z or VDM do for Schema? They use elementary maths (mainly set
theory) to express  more precisely what you mean. This is the best way I
know to expose any inconsistencies,  ambiguities and gaps in a spec. Better
even than implementing. A spec in Z is never 'just  maths'; it is maths
with explanatory English. Reading it, trying to relate the maths and the
 English, clears the cobwebs faster than anything.

People have noted pieces of 'tortured prose' in the schema spec. Try
turning the tortured  prose into maths. If the maths is simple, we have
learned something, and can probably  re-express the ideas in simpler
English. If the maths is tortured, we have got a problem!  Then leave that
part for release 2 and sort it out first.

Writing a Z spec is a piece of intense work, and reading it is not for
everybody. But   getting the spec right is _much_ cheaper than implementing
and finding problems downstream.  Michael Kay has commented that namespaces
doubled the complexity of implementing SAXON; we  need to be sure there are
no such complexity time-bombs in XML schema. A lot of people will
 implement on top of it for a long time.

W3C needs to be sure it is releasing a quality specification, as Schema
will be so central.  This would be a cost-effective way to do so.

Robert Worden