I like formal languages for formal verification, but they are not necessarily good for giving directions to protocol implementers. IETF, for example, uses textual descriptive language to describe algorithms used in protocols. While interoperability problems do arise, I doubt that use of a formal language that few implementers understand would reduce the interoperability problems. Let's not try to push the world into understanding OCL; our job is to push the world into understanding XACML.

I continue to vote for use of "standard" procedural language syntax, with a little descriptive comment.

Anne