Correctness
There is a problem with the above strategy for testing. Although we can be sure that our code works ok we can not guarantee it will work in all situations. We can not prove that the software will do a given job in all situations. The process of proving software will work is known as proving the correctness of the code. This is a major area of research of computer science and is not something which you would normally encounter till you get to the third year of your degree.
But why is proving correctness so hard? The answer is in the number of states software can be in. Consider a Boolean variable, x. It can have two values 1 or 0.
X |
1 |
0 |
Above shows all the possible states of X. In order to prove code is correct for this one variable we must use both possible values. That is we need to test both of the state s of the system. Consider adding a second and third Boolean variable, Y and Z.
X |
Added Y, produces 4 states. Y |
1 |
0 |
0 |
0 |
1 |
1 |
0 |
1 |
X |
Y |
Z |
1 |
0 |
0 |
0 |
0 |
Added Z, produces 8 states. 0 |
1 |
1 |
0 |
0 |
1 |
0 |
1 |
0 |
1 |
0 |
0 |
1 |
1 |
1 |
1 |
0 |
1 |
1 |
Every time we add a Boolean variable we double the amount of possible states. The number of states, if you have N number of Boolean variables, is –
2^N
If we have 10 variables we would end up with 1024 states. Imagine having to write 1024 tests! The situation gets much worse when we bring integers into the equation. Each variable could then have between 256 and 4294967296 states per variable. Imagine having four 32 bit variables. That would give us 3.403 * 10 38 . Writing that out would be –
34,0300,0000,0000,0000,0000,0000,0000,0000,0000,0000
How many programs have you wrote which only use four integer variables? Most programs will use thousands of variables. The more complicated the program is the more variables it will use which, in turn, results in more states being possible. Looking at this you may think it is impossible to prove code is correct. In a lot of ways you would be correct which would explain why a lot of programs have bugs in them. However consider safety critical systems such as air traffic control. Is this answer good enough?
There are tools to test software with large number of states. It uses logical deduction to try and prove the correctness of a given algorithm. The process has been used, to some success, to help find previously unnoticed bugs in major software. The most notable is its use to help identify problems in the TCP/IP protocol stack.. The interested user may wish to look up automatic verification in your favourite search engine. Most of the pages will be from university pages as it has not really moved too far away from the research stage.
