Calculating Preconditions from Postconditions

The best way to illustrate this technique is through examples, so let's dive in and work through an example, and then step back and evaluate the process.

Use Case Overview

A new on-line merchant has just introduced gift cards. You can buy a gift card online and have it mailed to a friend. Each card has a unique ID; to buy something you go to the Web site, log in using the ID, and then buy something. If you have change coming, a check for the difference is mailed to you; this is seen as marketing differentiation from competitors that force the customer to spend the full gift card price or more or lose the difference. Figure 5.1 shows the main scenario for the Buy Something With Gift Card use case.

Figure 5.1. Buy Something With Gift Card use case, main scenario.

With a typical use case description in hand, we are ready to think about how the system, as described by this use case, could fail and identify preconditions that would guard against such failure.

Step 1. Find a "Risky" Postcondition: Model as an Equation

First, we identify an operation or step of the use case, the postcondition for which we wish to calculate the precondition. In general, it's not safe to assume that the postconditions provided (if any) are the only postconditions. You'll need to read the body of the use case and look for operations where outputs are produced or state is changed, paying particular attention to ones doing "risky things." Looking at our example, this operation certainly fits the bill, so we'll focus on it:

"System signals accounts payable to mail check for difference between gift card value and price of item"

Next, we write the operation's postcondition in the form of a simple equation:

That was pretty easy. It's important to note that the "=" is not assignment; it is equality, and the equation describes a relationship between the three variables. Use of equality is what allows us to leverage the power of algebra that makes this technique work.^[8]

^[8] Gries and Schneider (1993) provide in-depth coverage of equality, equational logic and leveraging simple algebra-style thinking applied to reasoning about programs.

Step 2. Identify a Potential Failure: State an Invariant

This next step is at the heart of this technique, so a bit of discussion is in order. In a use case, postconditions are where the action is. They describe the output produced and state changed by the use case. And it is precisely when you are generating outputs and changing state that the opportunity for really "screwing things up" occurs; as the old saying goes: "To err is human. To really screw up you need a computer." So how does one judge if the computation described by a postcondition is valid (i.e., isn't going to screw something up)? To do so, we need some statement of what a valid output or valid system state is. These statements of validity are typically called invariants. In the formal methods community, they are variously called data invariants or state invariants: statements that should always be true about the data and system state being described. In the object-oriented community, they are called class invariants: something that should always be true about a class and any object instantiated from it (class invariants were inheritedno pun intendedfrom the formal methods community, so they are quite similar). In the study of program algorithms, there are loop invariants: something that should always be true about the loop being programmed (loop as in "While X do Y"). The word "invariant" simply means something that does not vary; is always true. The common denominator in all these invariants is that they set constraints that postconditions should not "violate."

So as a sanity check for the postconditions of our use case, we introduce the use of invariants. Given these invariants, we can then ask if the computation described by the postcondition preserves them. As it turns out, the answer is usually something like, "Yes, assuming that such and such is true when the computation happens." And that is a precondition: the "such and such" that must be true in order that the postcondition preserves the invariant (i.e., nothing gets "screwed up").

Explanation aside, let's look at the next step. Looking at our postcondition, we ask what bad things could happen with respect to the computation the postcondition is describing? One that comes immediately to mind is cutting a check for more than the gift card was worth; that is literally a money-losing proposition. So an invariant for this postconditionremember, something we always want to be trueis that the refund check amount should never be more than the value of the gift card:

In the field of safety-critical systemssystems where failures pose risk of injury or deaththis process of asking what bad things can happen is called Hazard Identification and Analysis. One identifies the hazards of a system (controller overfills storage tank with toxic chemicals), then analyzes the conditions and failures that would need to occur to cause the hazard to occur (e.g., using techniques such as fault tree analysis). One then formulates safety requirements for the system designed to prevent that combination of conditions and failures. This is a powerful risk-based testing strategy, helping testing to focus on high-impact defects first, and is essentially what we've done in this step.

Step 3. Compute the Precondition

All that remains now is to "turn the crank" to produce a precondition from the postcondition and invariant (see Figure 5.2).

Figure 5.2. Calculating the precondition for invariant CheckAmount < GiftCardValue.

Let's put all the pieces together and see what we have. This postcondition:

…meets this invariant (a property we want to always be true):

…as long as this precondition holds:

The postcondition, precondition, and invariant work together as a unit, as a team. They are like parts of a complete sentence; take away one, and the full meaning is not known.

Your first reaction to the precondition we've just calculated may be something like: "But of course! Everyone assumes that prices are greater than zero!" Right you are. And because everyone assumes it, it's just the type of precondition easily overlooked for error testing. But, in fact, it is a precondition for the successful computation of the refund check, and things do go awry: sign errors in coding, typing mistakes while entering prices in a database, sabotage, and so on.