W3C home > Mailing lists > Public > public-ws-policy@w3.org > September 2006

A bit on the formal semantics

From: Bijan Parsia <bparsia@cs.man.ac.uk>
Date: Fri, 15 Sep 2006 10:38:10 +0100
Message-Id: <81D91A19-8254-4ECF-B0A0-210B8AAB650D@cs.man.ac.uk>
To: public-ws-policy@w3.org

Just to clarify a few issues that I was too tired to bring up last  
night and didn't want to burn f2f time on given the lack of interest.  
This message is purely informative and in no way is intended to  
reraise the issues closed by the working group last night.

The reason I've not raised any issues on what were, imho, ambiguities  
is that the formalization we did before was on a much earlier version  
and I've not (yet) gone through the current spec to verify things. I  
was sorta waiting on this issue :)

With regard to David Orchard's remark about it being a trade off  
between methods of achieving clarity in the spec, I must strongly  
disagree. The other technique he brought up were test cases. But in  
no W3C spec that I know of are test cases *specifying*, i.e.,  
*normative*. The test suites produced by the W3C are systematically  
inadequate as conformance suites (they are specifically intended  
*not* to be, in my experience), and, of course, they can only test  
what you thought to test. This is partly why I worry about the high  
use of examples in the current text...it runs us perilously close to  
specification by example. Finally, as test suites get more useful for  
nailing down behavior, they get larger. Much larger. It becomes very  
difficult to determine whether the test are mutual coherent.

This is not to denigrate tests or examples. They can be very useful,  
indeed essential. But I don't see that they are candidates for a  
*specification* technique.

Finally, at the moment, I think WS-Policy is juuuust simple enough to  
make moving to a formal semantics rather easy, and, in fact, would  
considerable simplify the text. Having formal semantics from the  
start makes it easier to add features which are formalizable. This  
is, of course, a *constraint*. Some features aren't so easy to fit  
in. So it does limit the freedom (or agility) of the WG to add  
features. So there is an apparent tradeoff. However, in point of  
fact, you do need to verify, for example, that a new feature doesn't  
conflict with the commutivity of <all/> --- and that's easier to do  
than one might expect.

Of course, just because we're not using a formal semantics to  
specify, doesn't mean we can use it as a tool. I stand ready to chat  
or assist with such things.

Received on Friday, 15 September 2006 09:38:13 UTC

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 19:33:15 UTC