On 11/20/07, Andris <[EMAIL PROTECTED]> wrote: > Hi, I have read about formal verification, and it sounds like a > perfect tool to outreach the project goals. I'm pretty sure developers > know about it, so I'd like to read comments or opinions.
You'll want to check out the Z specification language. It's a work of art. The ISO standard is available online, but it would probably be heavy sledding for a newcomer, so you should start with an intro. There are a number of open source tools (dunno about the licensing.) My guess is knowledge of formal methods is quite rare even among the development cognoscenti. It's hard enough to find time to learn functional languages like haskell or ml; formal methods is a whole 'nother area. UML is widely known, but as a formal language, well, let's just say Z makes it look like an amateur hack. Ditto for xml schema. Even without formal (automated) verificiation, proof etc. formal notations are absolutely terrific for documenting specifications. Usually that means system specs, but once upon a time I did quite a bit of work trying to specify a typesetting language in Z - syntax and formal semantics. Never got around to writing it out (too lazy, er, busy), but I could see how it could be done, and Z provided a clarity that allowed me to think about the problems far more rigorously and with far more nuance than would otherwise have been possible. Recently I discovered the W3C tried to use Z to specify one of their languages, but I forget which. -Gregg
