Can New Software Testing Frameworks Bring Us to Provably Correct Software?

CIO — We can get CPUs that are consistent and reliable, and we can get compilers that work on top of them that are provably correct. Pascal creator Nicholas Wirth described how to write a correct compiler in his book, Compiler Construction, back in 1996. It should be a simple step from there to create "functionally correct" programs that can, for any input, produce the correct output.

The only problem is that no one seems to be able to actually do it.

From Complete Testing to Proofs

Dutch computer scientist Edsger W. Dijkstra is renowned for his contributions to programming languages and for creating the phrase "Go to Considered Harmful."

Within testing circles, he is known for his proof that testing addition for two 32-bit integers a microsecond at a time, would take longer than the known history of the universe. (The problem isn't the 32 bits but that two variables together create 64 bits of combinations.) This leads to Dijktra's famous quotation: "Testing can show the presence of errors, but not their absence."

Edsger Dijkstra proved that complete software testing is impossible.

Most programs are more complex than adding two numbers together. This leads some academics and practitioners to abandon testing and to pursue "proof of correctness" instead. These proofs can demonstrate that a requirements document, probably expressed in symbols, is correctly implemented in code.

Wirth argues that proofs of correctness should be included in programming courses in undergraduate computer science, while C.A.R. Hoare proposes the Floyd-Hoare notation. Sidney L. Hantler and James C. Kind, meanwhile, provide an excellent introduction to proving the correctness of programs, making it clear that the size of the proof will grow much faster than the code itself.

How-to: 7 Sensible Steps to Improve Software Quality

In other words, where the code for a 10-line procedure could be proven in an academic exercise, it's just not feasible for a real, industry computer program. This problem of exploding complexity in code is not new. The NATO Software Engineering Conference identified is as the "software crisis" back in 1968.

Where "proof of correctness" may not be feasible, there have been attempts to move in that direction, to provide more rigor and correctness around a program before it gets to testing. A few of the more popular ways to address this include the transformational specification, model-based testing and Fred Brooks' "Bronze Bullets." Each is discussed below.

Transformational Specification: Impractical for Software Development

If we could define our software in a precise, clear way, it may be possible to take that definition and transform it, over a series of steps, into the actual program. This turns out to be remarkably similar to what a compiler does—and compilers can, in theory, be demonstrated as correct.

Continue Reading