Further Thoughts: Preconditions, Postconditions, and Invariants in Use Cases

This is a good time to step back and look at some issues associated with preconditions, postconditions, and invariants as they apply to use cases. If you are already familiar with preconditions and postconditions through the use case literature, you have likely already noticed a few differences between that perspective and the model-based perspective presented here; we'll explore these and other issues here.

Preconditions and Postconditions of Individual Operations Versus the Use Case as a Whole

In this chapter, you have been looking at preconditions and postconditions of individual operations or steps that make up a use case. This is a different perspective from that of the use case literature, which generally talks about pre- and postconditions of the use case as a whole. How do these two perspectives relate to one another?

Let's start with postconditions: What is the relationship between postconditions of individual operations and the postconditions of the use case as a whole? The change made by a use case as a whole is the collective change made by the operations that make up the use case, so the postconditions specifying the change of the use case as a whole are the collective postconditions of the operations that make up the use case. If we choose to collect them together into a postcondition section of the use case, that is a matter of style rather than substance. Of course, working at the level of individual operations you'll probably be able to identify more postconditions than you might have had you worked at the use case level only, but that's a matter of thoroughness, not a substantive difference.

A similar argument can be made for preconditions, but with one key difference. The use case literature typically defines preconditions as those conditions that are necessary for the use case to start. But when working at the level of individual operations, the preconditions define those conditions that are necessary for the individual operation to start.^[10] The collection of all preconditions for all operations that form the use case can be divided into two groups:

^[10] This is consistent with the definition used by Rumbaugh et al. (2005).

1. Those preconditions that are satisfied external to the use case and therefore must be satisfied before the use case starts.

2. Those preconditions that will be satisfied after the use case starts by a postcondition of some operation within the same use case.

While the use case community has focused primarily on the first grouplabeling these "use case [as a whole] preconditions"from a failure analysis and test design standpoint this is not sufficient: the second group of preconditions can just as easily be a source of system failure. The failure to satisfy an operation's preconditionwhether it be the fault of something totally outside of the use case or some previous step in the same use casespells potential system failure either way.

Scope of Preconditions and Postconditions: Scenario Versus Whole Use Case

Another difference you may have noticed between the model-based perspective and the "standard" use case perspective is that of scope. In some use case literature, you will read that preconditions and postconditions should apply to all scenarios of a use case (i.e., to all possible paths through a use case). From a model-based perspective, this is usually not true. Because the model-based perspective views preconditions and postconditions as tied to operations performed by the steps of the use case, and because the steps of a use case vary from scenario to scenario, we should expect that their preconditions and postconditions will vary as well.

If this were simply an academic issue, it probably would not matter, but at least from a black-box specification, testing, and failure analysis standpoint, the model-based perspective of preconditions and postconditions is preferred. Preconditions and postconditions are the quintessential tools for black-box specification: saying what a thing does without saying how. If the postconditions of a use case areby definitionso general as to be valid for all possible use case scenarios, they are likely not to be useful as a basis for specifying expected behavior in test design or failure analysis. For example, the outputs and final state of a failed attempt to withdraw cash from an ATM are not the same as a successful withdrawal: if your postconditions reflect this, they too will differ; if your postconditions don't reflect this, you can't use them to specify the expected behavior of tests.

So, in this respect, the model-based perspective of preconditions and postconditions does indeed differ from that commonly presented in the use case literature.

Postconditions Can Have More than One Precondition

It may have been obvious from our chemical tank example, but it's good to be clear; a postcondition can be associated with more than one precondition. Given that a postcondition can potentially wreak havoc on more than one invariant in the use case, it only makes sense that we need separate preconditions for each of the invariants that are to be guarded. We saw just such an example of this in our chemical tank use case. The postcondition

requires this precondition Delta > 0 to guard this invariant InFlow' > OutFlow. But it also requires this precondition OutFlow InFlow' This further reinforces the concept that a specific precondition, postcondition, and invariant are a "team." And the team members can play on more than one team!

Weak and Strong Preconditions

The preconditions calculated with the techniques described in this chapter are often called the weakest preconditions needed to prevent failure of the invariant. These two examples from our chemical tank use case illustrate what this means. In that use case, we computed two preconditions for the chemical tank. First, we found that:

Delta > 0 is the weakest precondition needed to ensure that the invariant does not fail. "Weakest" simply means at the very least Delta must be greater than zero; though, practically speaking, the use case probably requires Delta have some value considerably bigger than zero to refill the tank in a timely manner, for example, Delta = 50 (gallons per minute).

The other example from the chemical tank use case was this:

OutFlow' < OutFlow + Delta is the weakest precondition needed to ensure the invariant does not fail. But again, practically speaking, the use case probably needs something stronger to ensure the rate of refill stays constant, for instance, the precondition that OutFlow' remains less than or equal to OutFlow throughout the refilling process, to the end of the use case (i.e., OutFlow' These preconditions, Delta = 50 and OutFlow' stronger preconditions because they imply the weaker forms, but not vice versa. What does imply mean? Well, if Delta = 50, then certainly Delta > 0, right? But if Delta > 0, it is not necessarily the case that Delta = 50!

And if OutFlow' OutFlow' < OutFlow + Delta (given that Delta is greater than zero, which we have said is the case). But if OutFlow' < OutFlow + Delta, it is not necessarily the case that OutFlow' That's what we mean by weak and strong preconditions. Strong preconditions imply weak ones, but not vice versa. So, in a use case where we derive a precondition to prevent an invariant from failing, we may decide to strengthen the precondition, and that's perfectly OK; the stronger precondition will still guard the invariant. But we can't weaken the precondition. The one that is calculated is already the weakest form.

As we continue with our chemical tank example in the next chapter, we will keep our calculated, weakest preconditions (i.e., Delta > 0 and OutFlow' < OutFlow + Delta) but know that in "real life" one would probably replace them with stronger, more practical ones.

Types of Invariants in Use Cases

The one thing that all invariants have in common is their role^[11]. The role of an invariant in a model-based specification of a use case is to:

^[11] Gluch et al. (2002) make a distinction between invariants, assertions (which they define as local invariants whose scope is confined to a single point of execution) and constraints (i.e., what is called here a transition constraint). These distinctions are not made here; if it plays the role of an invariant as defined, it will be called an invariant.

1. State a property, as a predicate (is either true or false), whose violation (the predicate is false) may result in system failure.

2. Provide the basis for computing a precondition, in conjunction with some postcondition.

As has already been noted, the role of invariants is very much like safety requirements in safety critical systems. In safety critical systems, hazard identification and analysis involves the identification of hazardous system failures followed by analysis of the combinations of conditions that could cause such failures. The final step is to then formulate safety requirements designed to prevent the identified combination of conditions. These safety requirements, not coincidentally, are often stated as invariant properties of the system, called safety invariants (Storey 1996).

But, though all invariants have the same role, there are different types. As already noted, "invariant" simply means something that is said to be always true. But the scope of what "always" means bears some discussion. The de facto standard is that when the term "invariant" is used, it is generally assumed you mean global invariant. But, in fact, not all invariants are global; some are local invariants. The scope of what "always" means differs between global and local invariants. A common example of a local invariant is a loop invariant (loop as in "While X do Y"). The scope of "always" for a loop invariant is local to a specific loop; it is a statement of truth about that one loop. It is not a statement of truth about, say, all loops. Let's look at examples of these two types of invariants using the examples we've seen thus far.

Global Invariants: Preconditions on Steroids

Global invariants are ones that are true for all states of a system, and as they apply to use cases, they are true for all scenarios of the use case and probably for all use cases of the system.^[12] The most common type of global invariant is the data invariant, which expresses some property that is true about data: inputs, outputs or state variables. They are variously called state invariants when used with state variables and class invariants when used in the context of classes. This type of invariant may be stated in terms of a single variable or a relationship over several variables. These are global data invariants from our examples:

^[12] Because use cases are used in so many waysat various levels of abstraction and granularity, from classes, to sub-systems, to whole products, and for all types of applications, from object-oriented, to relational databases, to hardwaregiving a general rule about the scope of invariants across use cases is tricky. Look at where the invariant is coming from and determine what the scope is there. So, for example, if the invariant is a class invariant, it will be true for any use cases written about that class. If the invariant is an integrity constraint on data in a relational database, it will apply for all use cases that create, read, update or delete that data. If the invariant is some safety requirement associated with a piece of hardware, the invariant will be true for all use cases written about that hardware.

Another common type of data invariant is the domain definition, a statement about the set of all possible values a variable can take on; here are two from the chemical tank example:

Domain definitions are essentially also global data invariants: they make claims about the values of the variables that should always be true.^[13]

^[13] The application of domain definitions as global invariants was illustrated in the "Exploring Boundary Condition Failures" section.

In a model-based specification, global invariants are stated in terms of unprimed state variables: their initial state before they are modified by a postcondition (i.e., the state they are in when the use case begins). It is then understood that the invariant applies to all subsequent primed versions of the state variable as well: their state after they are modified by postconditions. For example:

As this applies to use cases, the invariantboth unprimed and primed formsapplies to all scenarios of the use case; if WidgetsInStock, WidgetsInStock', WidgetsInStock", or WidgetsInStock'" appeared in other scenarios of the use case, it is assumed that they would each be equal to or greater than zero.

This is also true if multiple variables are involved in the invariant:

Global invariants are, in a sense, preconditions on steroids. Whereas a "regular" precondition may only guard one specific postcondition, global invariants act as guards to all postconditions that use the state variables covered in the global invariant. From a failure analysis and testing perspective, it is useful to keep this point in mind because they provide additional ways to validate the correct functioning of the system. A global invariant is a mini test case that can be repeated over and over to reaffirm that property of the system is still holding.

Local Invariants

Local invariants are ones that are not necessarily true for all states of the system, and so may only be true for the scope of a specific scenario. Local invariants are a postcondition-like statement that strengthens another existing postcondition in order to constrain the values that satisfy that postcondition. Here's an example from the chemical tank use case:

The easiest way to spot a local invariant in a model-based spec is that it involves the use of one or more primed variables. A local invariant stated about a primed variable cannot be assumed to apply to all unprimed and primed versions of the invariant. For example:

Transition Constraints: A Special Kind of Local Invariant

There is a particular kind of local invariant that you've seen in the chemical tank example that is used to express properties about state transitions. These are what C.J. Date (2000) calls a transition constraint: they constrain the legal transition of a state variable from one value to another. This is not the same thing as a state invariant. A state invariant describes a valid state or states; a transition constraint describes the allowed transition between states. The easiest way to spot a transition constraint is that it involves the primed and/or unprimed versions of a single state variable. This is a transition constraint from our chemical tank example:

Transition constraints, though local invariants, may sometimes be describing global properties, but just at a local level. Let's say that we have an application that tracks the number of persons that enter a secured area in the morning, and then counts the number that leave that night, allowing for a check that no one has remained in the secure area unauthorized overnight. The normal flow for the use case that tracks entry might be modeled with a postcondition like:

This flow of the use case is executed each time a person enters one of several turnstiles. If we had an alternate flow to the use case that tracked, say, persons entering the area via elevator, we might model it with a postcondition, such as:

The following invariant, though stated locally in terms of primed variables, expresses a property that is true across both use case scenarios, which is to say that the state variable Entered should never decrease but should always advance:

So, though stated as a local invariant, they may in fact be describing a global, cross-scenario property.