OASIS Mailing List ArchivesView the OASIS mailing list archive below
or browse/search using MarkMail.


Help: OASIS Mailing Lists Help | MarkMail Help



   RE: [xml-dev] XML CMM and ISO9000 compliance? - was A standard approach

[ Lists Home | Date Index | Thread Index ]

You're right.  For some systems, some proofs are worth paying for.
The question is which ones?  Would it have been more useful for 
NASA to have proven its low level engineers wrong about the 
potential damage to the carbon edges or for the low level 
engineers to have proven such damage is possible?  The first 
set would have been cheaper and answered the more immediate 
question of what is the best course of action next.  The 
second set proves that what was theorized was possible and 
probable.  Nothing more.  Given outcomes, I would have 
preferred the first set of proofs.

For any proof to be meaningful, it must make a difference 
to a choice of value.   It must reduce uncertainty.  
For proofs of XML to be valuable, we should know what choices 
we are making.

It comes back to what is to be proven given the axioms of the 
system and the rules for changing theorems to produce new but consistent 
theorems if we are talking about formal systems.  In fact, XML relies 
heavily on the Draconian rule for rejecting non-well formed strings. 
That's one level.  What is proven?  It doesn't prove XSLT will 
operate as intended because XSLT operates on the infoset.  

Does it prove that a correctly implemented XML parser can construct 
a valid infoset? 

What about operations on strings?  Is XSLT proven to be lossless?
At what level?

One of the interesting issues of formal systems is how long one 
can avoid discussing reality, the isomorphisms where meaningfulness 
is found.  As long as one is only discussing the system that is 
defined by XML 1.0, one can do that virtually forever.  The proofs 
one would look for in your example are in the applications.  Because 
applications such as XSLT, XML Schema, XQuery and XPath are used 
throughout the XML systems, proofs of these should be of interest 
to all.


From: Dave Pawson [mailto:dpawson@nildram.co.uk]

The military do.
  E.g. 'prove' all paths through a program.
  Any stack based language fails on this basis,
hence Z was born as a KISS language,
  to run on risc processors which were sufficiently simple to
  enable 'proof' of this nature.

  Or at least that's what the UK MoD tell us :-)

Mind you, it gets kind of critical when 'proving' the launch software
  for a missile leaving an airplane wing :-)


News | XML in Industry | Calendar | XML Registry
Marketplace | Resources | MyXML.org | Sponsors | Privacy Statement

Copyright 2001 XML.org. This site is hosted by OASIS