1. 9

  2. 4

    Another technique is the use of formal specifications for requirements and/or design. They eliminate ambiguity while providing a bases for correctness checks of the software by automated or semi-automated tooling. Also help human thinking due to being close to the problem description than a machine’s operation. Brief description of some strategies and notations:


    High-assurance field recognize the value long ago as upfront investments into consistency and correctness led to prevention of defects earlier in the lifecycle. It was also shown necessary to be sure systems were correct, reliable, or secure against specific problem categories. Even those one-off programs you mentioned can have a lot of incidental complexity the programmer is juggling in their heads. My favorite example is the one below where the formal requirements take 10 pages to describe. Simple system that we should just code up, right? Look at the piles of refined designs that follow with all the associated states, conditions, and interactions. A fraction of this would be in informal requirements, another in the code, another in developer’s head, and some not at all at some point. And that’s just for 10 pages of requirements. Modern software, esp Internet-connected, is often way more complex.


    So, if high-quality or longevity of software is expected, it’s best to always be clear on the requirements, design, implementation, and how they connect. All assumptions and environmental conditions should be included. That way, once maintenance phase starts, people trying to understand, fix, and/or extend the system won’t be as likely to break it or hold onto crap they don’t need in new circumstances. :)

    1. 4

      The problem with formal specs is that you still rely on humans to parse, interpret and conform to them every time you modify the software. If the adherence to specs can’t be verified by an automated system then you are leaving yourself open to eventual failure.

      1. 3

        If you’re going to produce a complete, formal specification of a software system, you might as well write a compiler and skip the manual translation.

        On the other hand, there’s a lot of good to be found in formalizing parts of a system.

        In particular,

        • Algorithms (e.g. sales forecasts) can have example tables of input/output verified early and are rarely changed
        • Data models can be formalized via e.g. via NORMA or ActiveFacts/CQL; the latter is quite easy for humans to verify.
        1. 1

          That’s a problem with informal specs, too. The only thing that changes is the risk goes down dramatically. Keeping the specs and code close to each other + synced knocks out a lot of the risk. Further, using executable specs that allow code generation… like Esterel’s SCADE or Prolog… eliminates anywhere from most to all of that problem.

      2. 1

        I’d be thrilled if people wrote non-rigorous, informal documents describing the “why"s and "how"s of what they’re going to build, with a clear description of how it benefits the user/customer/client of the system/component. As many people have said (written!) before, writing things down requires a clarity of thought that running to write code doesn’t. It doesn’t need to be a 10 page document, a 1- or 2-pager is a great start and is infinitely greater than nothing at all (though I’d want more than just a “readme”, given how most readme’s fail to elaborate on the "why does this exist”).

        Formal specs, etc., are great, but there’s so much low-hanging fruit that could be grabbed by just writing something down and then having other people read and discuss. This is why written contracts exist: not as an enforcement mechanism (though they are used for that, it’s actually a failure mode), but so everyone is clear on what’s being done (as far as one can be “clear” in a human language).