Lean Software Engineering

In my last post, I proposed the notion of a capability ladder for design specification and verification. The utility of such a ladder is that it allows you to match your capability to the demands of the problem at hand. If you want to improve your design/code quality or reduce rework, then the ladder allows you to set goals, and make a plan to reach them at an appropriate pace for your team. Asking a team to make a sudden leap in capability can be very disruptive. It can be bad for morale and a distraction from delivering business value. It is often better to evolve into a more advanced practice.

Dynamic contracts are something of a hybrid between unit tests and formal specifications. They embody the syntax and semantics of formal specification, but still depend on live execution for verification. Runtime assertion is useful because it can detect error conditions in the field, but somewhat inconvenient because of the neccesity of providing test input in the lab. Wouldn’t it be nice if the computer could figure that out for us?

In fact, a new generation of contract-oriented languages aims to do just that. The SPARK programming language is a formally verifiable subset of Ada, designed for use on safety-critical systems. Spec# from Microsoft Research is an extension to C# that includes an embedded specification language. The improvement over earlier contract languages is the application of static analysis to the contract, which evaluates the program’s possible execution paths without the need for sample input data. In other words, static contract verification makes unit tests redundant, and therefore unnecessary.

Now, this is no slight to the humble unit test. The point here is to illustrate that traditional unit tests exist on a spectrum of verification. The implication of the redundancy of unit tests in the presence of static contracts is that you only need one or the other. Detailed unit tests likewise make detailed design specifications redundant, so which you choose is more a matter of preference and capability. Doing them both leads to duplication, error, and waste, and that’s not lean.

Once we have mastered the static contract, we are at the doorstep of the most advanced design specification method of them all: the formal specification language. The best-known such language is probably the Z specification language. In recent years, the Object Constraint Language has also become somewhat well-known (“popular” would be a considerable overstatement). Specification languages can have a rich syntax tailored for specification and can be validated independently of source code. They can be applied to verification of source code by means of static analysis, or theorem prover. The advantage here is the potential for discovery of design errors at the earliest possible moment, before a single line of code has been written.

Can a software development process that uses a formal specification language be lean? You bet it can. There is no rule that says that such a specification has to be written in one monolithic chunk. The same evolutionary design approach we might use with an Agile process can still be applied, only now we may have the comfort that our design evolutions are provably correct. Improving our specification capability can improve throughput by reducing rework. Does it take a higher level of skill to read and write a formal specification? Of course it does. Continuous and aggressive skill improvement is very much a part of lean thinking. An skillful TDD practitioner should have little difficulty adopting Design by Contract. A skillful DBC practitioner should have little difficulty adopting Z.

The lean principle of perfection helps us to understand that however we might do something today, there’s a way to do it better. If TDD has taken you to 10 defects per KLOC, and you want to get to 1 defect per KLOC, you know that there’s a way to get there, and that way is not “try harder.”