"What Good Are Strong Specifications?"

"I'll go up and find out what they need [this project to actually do], the rest of you stat coding it [right now]" is meant to be humorous, alas I've seen it the Real World far to often. What is our new widgets actually required to do (Validation: Have we built the correct device? Do we meet the customer's requirements)? Which brings us to the subject of this blog, writing software specifications (Verification: Have we built the device correctly? Did we find and remove all of the 'bugs'?) and User Documentation.

What Good Are Strong Specifications? [PDF] by Nadia Polikarpova, Carlo A. Furia, Yu Pei, Yi Wei and Bertrand Meyer Chair of Software Engineering, ETH Zurich, Switzerland.

Abstract:

Experience with lightweight formal methods suggests that programmers are willing to write specification if it brings tangible benefits to their usual development activities. This paper considers stronger specifications and studies whether they can be deployed as an incremental practice that brings additional benefits without being unacceptably expensive. We introduce a methodology that extends Design by Contract to write strong specifications of functional properties in the form of preconditions, postconditions, and invariants. The methodology aims at being palatable to developers who are not fluent in formal techniques but are comfortable with writing simple specifications. We evaluate the cost and the benefits of using strong specifications by applying the methodology to testing data structure implementations written in Eiffel and C#. In our extensive experiments, testing against strong specifications detects twice as many bugs as standard contracts, with a reasonable overhead in terms of annotation burden and runtime performance while testing. In the wide spectrum of formal techniques for software quality, testing against strong specifications lies in a "sweet spot" with a favorable benefit to effort ratio.

- {Trackback}

In a less formal, more practical implementation to the everyday Embedded System Developer, Doxygen is a popular method of generating documentation from source code. Doxygen can be extended with 'alias' to add features, and a thread over at Stack Overflow, Custom tags with Doxygen shows how to add 'Requirement' and 'Requirement Verification' aliases.

While Doxygen excels at Program Documentation, it is often pressed into service to generate User Documentation, which far to often a novel concept to software authors, that is not the domain Doxygen was intended for and often has to be beat into submission. On the other-hand AsciiDoc is written specifically to author User Documentation, and ADExtract.py can be used to extract the User Documentation from the source code files. If you truly want to keep your project on track then write the User Documentation first before any line of code is ever written. Keeping the Source Code, Program Documentation and User Documentation as a single file gives them the best hope of actually being maintained.

Something I always find extremely frustrating is the disconnect between Academia Research into Software Safety, and the Real World of "we must ship 782 Widgets by Friday to meet payroll!". Take for example Net-Centric Software & Systems Consortium's Software Safety Tutorial, that is reproduced below, which seems more like an expedition for finding more funding from industry. How do you actually apply this kind of information in the Real World? The European Network of Excellence of Embedded Systems Design is a bit more in-line with the concept that a product must having shipping it as one of its primary requiremnts...

Alas the problem is not just one of academic discussion as Dave Woll explains the issues of our aging infrastructure impending failure in The coming wave of process safety system migration: Systems changes require rigorous hazards analysis.

If you do like Slid Shows check out CPLD Course Draft International Software Safety Conference 2011: