Re: A bit on the formal semantics

Just a caution on making formal semantics normative: The OASIS XACML 2.0 
specification used Haskell to specify the semantics of our higher order 
functions.  When the specification was submitted to the ITU for 
cross-standardization, there was no approved standard for Haskell that 
we could reference.  In order to satisfy ITU requirements, we had to 
make the Haskell description non-normative and the English text 
description the normative version.

Regards,
Anne

Bijan Parsia wrote:

> 
> 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.
> 
> Cheers,
> Bijan.
> 

-- 
Anne H. Anderson               Anne.Anderson@sun.com
Sun Microsystems Labs          1-781-442-0928
Burlington, MA USA

Received on Friday, 15 September 2006 14:43:24 UTC