Manually finding defects in a program's output is difficult if failures occur rarely. Manual debugging is simply a task at which humans are not proficient. Hence, the use of automated testing oracles (or what throughout this report we simply term ``oracles'') is valuable when testing software in which failures are rare. The software is of good enough quality such that failures are rare.
Building automated test oracles requires that the oracle knows what is correct (with respect to the specification) and what is not. Fortunately, oracles can be designed directly from formal specifications (that describe exactly what the software is supposed to do without also describing the implementation details of the system) [11]. An executable specification is a formal specification can be executed (like a program) to see if the behavior it defines satisfies the higher level requirements of the system. Executable specifications typically produce output, but do not check this output. In theory, the output from an executable specification can be given to the oracle so that the oracle can learn what output is correct.
Run-time assertion checking is a ``programming for better validation'' trick that helps ensure that a program state satisfies certain logical constraints. Unlike executable specifications, run-time assertions do check for the correctness of the output. Run-time assertions (or simply ``assertions'') are based on either the requirements or the specification. Some of the earliest writing concerning assertions can be traced to [6,9], and more recent research into giving programs the ability to check themselves during execution can be found in [12,13,2,15]. Further, Bieman and Yin recently discussed using assertions to increase fault detectability [1]; however our contribution furthers the idea of run-time assertions by providing methods for placing assertions where assertions are more desperately needed. Our method decides what portion of the software's state really needs to be checked, and where that check needs to be placed. We term our assertion placement scheme strategic run-time assertion checking.
Our goal is to embed assertions in a manner that engenders testing with greater defect revealing ability. The conjecture that has motivated this work follows:
Why place assertions on program states if it is known a priori that if these states are in error, failure of the software is nearly guaranteed to occur. Instead, place assertions on program states when it is likely that incorrectness in those portions of the state will not be observable in the software's output.Our strategic run-time assertion checking presents the opportunity to thwart defect hiding at a more reasonable cost than ad hoc assertion placement, which is the usual heuristic for deciding where to put assertions.
Software assertions can be very complicated in terms of the information that they produce, but for simplicity, we will assume that software assertions are Boolean functions that only evaluate to TRUE when a program state satisfies some semantic condition, and FALSE otherwise. If an assertion evaluates to FALSE, we will consider it the same as if the execution of the program resulted in failure, even if the output for that execution is correct. Because a program that did not have assertions is truly a different program after assertions are added, it is necessary for us to redefine what we consider a program failure: a program failure will be said to have occurred if the program output is incorrect or if an assertion evaluates to FALSE. This not only modifies what is considered failure, but it also modifies what is considered output, because there is now one more bit of output each time that an assertion statement fails.
Whenever the amount of output increases (e.g., outputting 2 64-bit floating point values as opposed to one), more of the internal (intermediate) calculations can be observed. Observability has long been a metric used in hardware design that describes the degree (or ability) of a chip to detect problems in the inner logic of a chip at the output of the chip. When observability is poor, hardware probes are often placed in circuits to increase the observability of the circuit during testing. Similarly, assertions increase software's observability by increasing the dimensionality and/or cardinality of the software's output space, which is precisely what is desired if the of testing is to catch defects. (This is discussed in more detail later.) In our work, we consider software observability to be an informal measure of the tester's ability to ascertain what is occurring internally inside of the states created at run-time.
Correctness proofs can be thought of as a formal assertion checking system. Correctness proofs statically test to ensure that the entire program satisfies certain logical constraints for all inputs, whereas an executable specification, like a program, can be run on a per test case basis. Software assertions perform a slightly different function than correctness proofs; they semantically test internal program states that are created at run-time and that may not be observable as stand-alone entities. For example, given a known range of legal values for some intermediate computation in a program, a software assertion can test the correctness of the program state at the instant when the state is created. Since assertions are able to check intermediate data state values, they can reveal when the program has entered into an undesirable state. This is vital, because the undesirable state might not propagate into a program failure.
Figure 1: One-dimensional output.
An important measure of the fault-hiding ability of a program is contained in the dimensionality and cardinality of the program. Dimensionality is the number of different output variables produced by the program, and cardinality is the total number of unique output values. So for example, if a program has 100 different variables, and only one variable's value is output, then the dimensionality is one. If 20 variables have their values output, the dimensionality would be 20. If there are 1,000,000 million unique input values to the program, then the cardinality of the program is less than or equal to 1,000,000.
The effect of assertions on the dimensionality and cardinality of a program can be best explained through examples. Figure 1 illustrates a program that reads in an integer and outputs an integer; in this example, an input value of 5 produces 100, 6 produces 200, and 7 produces 300. Thus, the dimensionality of the output space in Figure 1 is one.
Figure 2: Two-dimensional output from added Assertion
In Figure 2, the conditional branch in the code causes only certain inputs to execute the assertion. The assertion essentially acts as another output statement whose result will be checked by the oracle. Thus, for some inputs, the dimensionality of the output actually increases to two. In Figure 2, the inputs 5 and 6 execute the assertion and will therefore have outputs with a dimensionality of two, whereas an input value of 7 will have a dimensionality of one.
Now imagine a slightly different example where two unique input cases resulted in the same output value, and assume this value is of dimension n. By adding an assertion to the code that both input cases execute, it is possible that the variable asserted on now has different values, and hence each input case can be thought of as producing a unique output value of dimension n+1. This is shown in Figure 3. In this example, we see how an assertion can increase the cardinality of the output space.
Figure 3: Assertions increase the cardinality of the
output space.
Assertions have an interesting ability that is similar to the ability of oracles. When an assertion evaluates to FALSE, it has the ability to not only warn of a problem at this point in the code, but also to warn of problems at totally different places in the code. This requires reversing the execution trace back to the preceding computations in order to localize the problem. It is this ability to warn of problems originating from various statements that increases the fault detectability provided by assertions.