Slashdot Mirror

← Back to Stories (view on slashdot.org)

Are You Using Z-Notation to Validate Your Software?

Posted by Cliff on from the mathematically-examinating-your-code dept.

ghopson asks: "Many years ago in the early nineties I became aware of a software definition language called Z, which was based on set theory. The idea was that a software system could be defined in 'Z', and then that system could be mathematically proven to be 100% correct (in other words, zero defects).What is the current state of play with 'zero defect' software development? I know Z still exists, that there is a software development method (the B-method) associated with it. Have techniques and advances such as MDA advanced zero-defect software development? Or would a set of robust unit tests suffice?"

3 of 110 comments (clear)

  1. Re:what does this buy me? by Ivan+Raikov · · Score: 3, Interesting

    In other words, I can prove that if my software is 100% bug-free, it's bug-free. Woohoo. This doesn't address the case where my program doesn't fully conform to the Z specification, does it?

    In formal verification, the idea is that you would have a way to prove the equivalence between your Z model (or whatever modeling language you use) and your implementation. Of course, it's a lot more difficult to prove equivalence between a formal model and a C implementation, than if you are using a modern high-level language like Standard ML.

    --
    Bush Lies Watch
  2. Re:Unit tests seem to be the way to go by saden1 · · Score: 3, Interesting

    Someone also needs to tell this crowd that some bugs are result of implementation itself. Out of bounds, errors, looking in non-existent resources, etc. Of course exception handling mechanism should be used where appropriate but that itself is prone to programmatically mistakes.

    Unit Testing is by far the best way to go. You find a problem, you fix it but at the same time make sure you don't introduce new problems. This might seem like a daunting task when dealing with a large system but it sure beats trying to strive for perfection all at once.

    Test, test, test I say.

    --

    -----
    One is born into aristocracy, but mediocrity can only be achieved through hard work.
  3. "Real-world" use of Z for software development by RelentlessWeevilHowl · · Score: 5, Interesting

    Bart Massey and Jamey Sharp of Portland State have written XCB, a reimplementation of Xlib with an eye towards improved tunability (and an improved API). They were having problems coming up with an implementation that worked properly; the multi-threaded connection handling code was up to four designs and two implementations, all of them incorrect.

    Massey and Robert Bauer of Rational ended up writing a Z specification for that portion of the code, and proved it correct. The C implementation of the spec is in the XCB distribution right now.

    Massey and Bauer published a paper describing this effort for USENIX 2002. They conclude with the comment "[t]he sort of lightweight modeling described [above], that isolates a troublesome portion of the system for more detailed study, is especially appropriate[...]".

    XCB Wiki: http://xcb.wiki.cs.pdx.edu/
    XCB/Z Paper: http://xcb.wiki.cs.pdx.edu/pub/XCB/WebHome/usenix- zxcb.pdf