There are many ways to create software that makes it difficult to verify. If software is hard to test then bugs will inevitably occur. I talk about how to make code more verifiable below.
But before I go on, I should mention TDD (test-driven development). I will probably talk more about TDD in a later post, but I believe one of the main (but never mentioned) advantages of TDD is that it makes code more verifiable.
Testing
Verifiability plays an important part in testing. After all, you can't test something properly if it is difficult to verify that it is correct or, conversely, show that it has no bugs. I give an example of code below that shows how code can be hard to verify and makes bugs far more likely.
In extreme cases, software changes can be impossible to test. For example, I was recently asked to fix up some dialogs that had some spelling mistakes. The problem was that the software was old and nobody even knew how to get the dialogs to display or even if the code that displayed them was reachable. (Some of the dialogs were not even used anywhere in the code as far as I could tell.) It makes no sense to fix something if you cannot verify that it has been fixed!
Debugging
Verifiability is also important in the debugging process. Removing bugs has three phases:
- detecting the presence of a bug
- tracking down the root cause of the bug
- fixing the bug
How Do We Make Software More Verifiable?
Verifiability can be increased in three ways that I can think of:
- external testing tools
- extra facilities built into the software such as assertions and unit tests
- how the application code is actually designed and written
Testing Tools
There are many software tools that can be used to assist software testing. Automated testing tools allow testers to easily run regression tests. This is very useful to ensure that software remains correct after modifications.
One aspect of code that is not often well-tested is error-handling. Test tools, mock objects, debuggers and simulators allow simulation of error conditions that may be difficult to reproduce otherwise. For example, a debug heap library is invaluable in detecting memory allocation errors in C programs.
Debuggers obviously make software more debuggable, but they can also be useful for verifiability. Stepping through code in a debugger is extremely useful for understanding code and finding problems that may not have otherwise been seen.
Assertions
Assertions are an old but crucial way for software to self-diagnose when it has problems. Without assertions bugs can go unnoticed and the software may silently continue in a damaged state (see Defensive Programming).
In my experience, assertions are even more important for debuggability. I have seen problems in C (almost always rogue pointers) that have taken days if not weeks to track down. Careful use of assertions can alert the developer to the problem at its source.
Unit Tests
Unit tests (and TDD) are important for verifiability. If you have proper and complete units tests then you can get a straightforward and obvious indicator whether the code is correct.
In my experience most bugs that creep into released code are due to modifications to the original design. Poor changes are made because the modifier does not fully understand how the code works -- even if the modifier was the original designer, they can still forget! This is further compounded by the fact that the modified code is often less thoroughly tested than the original version.
Mock objects are useful by themselves, for example for testing error-handling code. (When not used with unit tests they may be called simulators, debug libraries, automated test harnesses. etc) Mock objects are particularly useful with unit tests as they allow testing of a module to be isolated from other parts of a system.
I will talk more about verifiability and unit tests in a future post, hopefully soon.
Software Design
Many aspects of good design that improve the maintainability of code are also good for verifiability. For example, decoupling of modules makes the code easier to understand but it also makes the modules much easier to test individually. Testing several simple modules is always simpler than testing a single large module with the same features, even if only because the permutations to be tested increase dramatically as the number of inputs increases. (See SRP and other design principles in Software Design).
Code
Perhaps the simplest way to increase verifiability is simply to write good code. The same principles that a software architect or designer uses also apply at the coding level.
One of the worst programming practices is to use global variables to communicate between modules or functions. This results in poorly understood coupling between different parts of the system. For example, if the behaviour of a function depends on the value of a global variable, it makes it very difficult to verify that the function works correctly, since you can't ensure that some outside influence will change that variable.
Another problem is large functions that do too much (remember SRP). Again the more parameters (or other inputs) to a function, the harder it is to check that all combinations are handled correctly.
Similarly, code with many branches (ie, if statements) is hard to verify since there may be a large number of different paths through the code. Even ensuring that all code is tested (with a code coverage tool) is insufficient. You may need to test every combination of code paths to be sure the code has no bugs.
Code Example
Finally, I will give an example of some C code that is virtually impossible to properly verify due to the way it was written.
Some time ago I worked on some C code for an embedded system. A lot of the code made use of time (and date) values returned from the system. Time was returned as the number of milliseconds since midnight.
One particular function was used to determine if a process had timed out. Like the rest of the code it used this system "time" value. The code was very simple to implement except for the special case where the start time and the end time straddled midnight. (Normally the code below would not be executing in the middle of the night but under unusual circumstances it could.) Here is a simplified version of the code:
/* return 1 if we have already passed end time */
int timed_out(long start, long end)
{
long now = get_time();
if (start == end && end != now)
return 1;
if (end > start)
{
if (now > end || now < start)
return 1;
}
else if (end < start)
{
if (now < start && now > end)
return 1;
}
return 0;
}
int timed_out(long start, long end)
{
long now = get_time();
if (start == end && end != now)
return 1;
if (end > start)
{
if (now > end || now < start)
return 1;
}
else if (end < start)
{
if (now < start && now > end)
return 1;
}
return 0;
}
Do you think the above code always works correctly? It is difficult just looking at it to tell if it is correct. It is virtually impossible for testers to verify that the above code works correctly, even if they were aware that midnight was a special case in the code. Setting up a unit test would be difficult since the software was not permitted to change the system time (though a mock object could have been created to emulate the system time).
You might also notice that the code suffers from poor understandability (and hence poor maintainability) as well as poor verifiability.
A much better way to handle such timing events is to use a type like time_t or clock_t which does not reset at the end of day.
/* return 1 if we have already passed end time */
int timed_out(clock_t end)
{
clock_t now = clock();
assert(now != (clock_t)-1);
return now >= end;
}
int timed_out(clock_t end)
{
clock_t now = clock();
assert(now != (clock_t)-1);
return now >= end;
}
Note that the above code is only for low-resolution timing since the C standard says nothing about the resolution of clock_t – ie, the value of CLOCKS_PER_SEC is implementation-defined. However, in this example 1/10 second was sufficient and CLOCKS_PER_SEC == 1000 for the compiler run-time being used.
This code is more verifiable. First, it is fairly
simple manually verify since anyone reading the code can understand it fairly easily. It is also easy to step through the code in the debugger to make sure it works. Moreover, it does not need special testing for midnight.
Summary
It is important to create software that is easy to test. We talked about using tools and code (such as unit tests) to enhance verifiability, but more important is creating good code. Now that I think about it, verifiability is probably affected more by the data structures that are used (such as the time-of-day format used in the above example). The data structures define the code; get these structures right and the software is likely to be much more verifiable, and consequently less likely to have bugs.
Furthermore, in my experience writing software with testing in mind is more likely to produce better code. This is one of the (many) advantages of unit tests (and even more so with TDD). If you create units tests as you create the code (or even before you create the code in the case of TDD) then you will create code that is not only more verifiable but also better designed in general.
