Contracts provide a basis for deriving test cases based on a simple observation concerning constraints of value ranges expressed in contracts. As a simple example take the following informal contract

// requires (x > 0 & 0 < y & y < 11) | (x < 0 & y == 1)
// ensures Res = 2 * y

Not yet knowing how this is going to implemented, we can predicted which conditions might occur in the implementation. Typically, they are going to based on the components of the properties specified the requires clauses, that is, x > 0, 0 < y, y < 11, x < 0, and y == 1. Of course, there might be more and some components might be ignored. But it’s a good starting point nonetheless. Any implementation of the contract makes some use of it. We consider two techniques that can be used for deriving test cases from specifications:

• Equivalence class partitioning to derive combinations of value ranges
• Boundary value analysis to derive specific values from the value ranges

Taken together, the two techniques permit to exploit contracts for test case generation without considering potential implementations. This can be particularly useful in cases where there is no access to an implementation. Another strength of these techniques is that they also permit to check program behavior outside the defined precondition. This can be relevant for the security of public interfaces, for instance, when a parameter is an array bound or index.

Equivalence Class Partitioning

Assuming all values are integer numbers, in the example

// requires (x > 0 & 0 < y & y < 11) | (x < 0 & y == 1)
// ensures z = 2 * y

each inequality partitions the integer numbers into two sets that can subsequently be intersected. For instance,

1. x > 0 partitions the integer numbers into all those x such that x > 0 and those x such that x <= 0, and
2. x < 0 partitions the integer numbers into all those x such that x < 0 and those x such that x >= 0.

Calculating the intersections of the partitions in 1 and 2, we obtain

Similarly we get the four partitions y <= 0, y == 1, 1 < y & y < 11, and y >= 11 from three three containts on y.

We categorise the product partitions for x and y into «Valid» and «Invalid» partitions

where a product partition is «Valid» if the component partitions imply the precondition in the requires clause. For instance, x < 0 & y == 1 implies (x > 0 & 0 < y & y < 11) | (x < 0 & y == 1). A product partition is «Invalid» if the component partitions imply the negated precondition. For instance, x < 0 & y <= 0 implies (x <= 0 | 0 >= y | y >= 11) & (x >= 0 | y != 1). We are not interested in partitions that do not fall into one of the two categories «Valid» or «Invalid». If a product partition is neither «Valid» or «Invalid», we can either decide to split the component partitions further or discard the product partition.

For non-numeric data types partitions may be based on equality or take into account “special” values. For instance, for the enumerated values Red, Green and Blue of a type Color we may have two partitions x == Red and x != Red. For arrays, we may have a == Array() and a != Array().

Boundary Value Analysis

Equivalence class partitioning does not provide the values for the input of test cases except in the cases where a precondition contains an equation. Boundary value analysis provides the remaining values that are required to specify the input of test cases. It takes the partitions found in equivalence class partitioning and chooses values at the boundaries of the partitions.

Combinations of theses values according to the product partitions are the input values for the test cases.

Test Cases

After performing equivalence class partitioning and boundary value analysis, we have to set up the test cases.

For «Invalid» inputs of a function of a public interface we have to ensure that the function aborts properly. For internal functions we may want to check that such calls do not have harmful side-effects. Testing with «Invalid» inputs and the expected behaviour depends very much on the kind of software being developed. Our development methodology is based on contracts and contract adherence, but a malicious programmer could attempt to produce unindended software behaviour by breaking the contracts. Such considerations are very relevant when dealing with secure software components.

For all «Valid» partitions we can use the postcondition to obtain the expected output for the function. In our example the postcondition is Res = 2 * y, so that we can calculate the result Res from the input value y. In cases where Res is only specified by a relation, say Res >= 2 * y, we can check the result of the function with respect to this relation.