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.
Some Z links: The original de facto manual, outdated but still very useful and readable: http://spivey.oriel.ox.ac.uk/mike/zrm/index.html Jacky's book is excellent, but not free. ISO Spec (note the small print, which contains a link to the free download): http://www.iso.org/iso/iso_catalogue/catalogue_tc/catalogue_detail.htm?csnumb er=21573 Actually the easy way to do this is: http://www.bibsonomy.org/user/mobileink/Z I'm digging around at http://vl.zuser.org/#tools and I find many of the free tools are a) written in Java, and b) GPL licensed. So there's a good OBSD project, implement some Z tools. ;) However, HOL, which is used by some Z tools, is BSD licensed: http://hol.sourceforge.net/ As is the Glasgow Haskell Compiler. Anyway, the main practical benefit of Z for OBSD would probably be e.g. for documenting NICs or the like. Formal specification, validation, etc. for e.g. cryptographic stuff would be great, but also a huge amount of work. Even then, if the implementation language is C, then the code will be beyond formal analysis; you'd have to use an implementation language that supports formal reasoning, like haskell. Not to mention, you'd have to prove that your compiler works correctly. -gregg
