Home

A Case for Formal Specification

For once, a story from Kuro5hin.

Formal Specification helps build more robust, more maintainable software with fewer bugs and defects. It has a long history, but it is still a developing field. While it may not be suitable for all software projects, a case can be made that there are many projects not currently using formal specification that stand to benefit from it. As the methods and tools for formal specification develop it is increasingly becoming something that developers and software engineers should learn to use to their advantage.

I haven't had a chance to read it yet, but this story mentions SPARK and CASL, and seems reasonably well-researched.

By Frank Atanassow at 2005-08-02 11:44 | Software Engineering | other blogs | 7161 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Good story

The story itself is pretty good (although the choice of examples is not necessarily the best in terms of showing off the capabilities of formal specs). Unfortunately, the response is pretty much the standard response any time this subject comes up: a few positive comments from people who have actually tried formal specification, and a lot of excuses as to why it won't work from people who have never tried formal spec and don't really understand it.

I do think that the author's mention of the sliding scale of formality, from basic type checking up to full-blown refinement proofs, is useful, and perhaps deserved more emphasis (I think it came out more in his comments). Hopefully he managed to win a few people over.

By Allan McInnes at Tue, 2005-08-02 14:46 | login or register to post comments