On 13/05/11 05:52, Milind Bhandarkar wrote:
Ok, my mistake. They have only asked for documented specifications. I may
have been influenced by all the specifications I have read. All of them
were in English, which is characterized as a natural language.
But then, if you are proposing a specification in a non-natural-language,
isn't that called a test suite ? Or is there a middle ground ?
There's formal specifications in languages like Z, We don't really want
to go there if we can help it, as all it lets you do is prove
correctness if you're a mathematician, and I haven't found the
mathematician plugin for Jenkins yet.
There's also languages like Extended ML, from Sanella et al, who may be
familiar to Doug from his time in the frozen lands of the north
(edinburgh):
http://homepages.inf.ed.ac.uk/dts/eml/
Some of the bits of spec in this language can be executed, as long as
you don't start declaring things about state over time. Again, though,
it's hard work, unless your target language is, say ML or Haskell, as
there you can jump from Specification to Implementation fairly rapidly
Where the formal stuff is good for is things like consistency protocols,
so I'd hope someone did get out the proofs for Zookeeper, so the rest of
us can rely on it working.
-Steve
