Modeling State Change

Frequently, a use case involves change to the state of a system. In such instances, in order to calculate preconditions, we need a way to model the system's before and after state. Again, a simple example is the best way to illustrate. In the following example, WidgetsInStock is a state variable; a set of state variables such as WidgetsInStock are what define the state of, say, an inventory control system. We can represent the after version of a state variable with the postfix prime ( ' ). This equation describes the expected results of one step in a use case, that of shipping widgets. It describes the relationship between the number of widgets that were in stock when the use case started (no prime) versus the number of widgets in stock after some number were shipped (primed):

Again, keep in mind that "=" is equality, not assignment: the equation describes a relationship between the variables.^[9]

^[9] The convention used here of decorating state variables with prime follows that of the model-based specification languages Z and VDM. In Eiffel, the prefix old is used.

WidgetsInStock = old WidgetsInStock WidgetsShipped. See Meyer (1988). In UML's Object Constraint Language (OCL) the postfix @pre is used:

WidgetsInStock = WidgetsInStock@pre WidgetsShipped. See Warmer and Kleppe (1999).

Having before and after versions of state variables allows us to talk about invariants that involve both. The state variable WidgetsInStock is subject to the invariant that it should always be greater than or equal to zero, and this should be true before and after the postcondition completes. Here is this invariant stated for the after version of the state variable, i.e., this use case should never ship more widgets than are in stock (that's the failure to be avoided):

Turning the crank, we get the precondition that ensures the postcondition meets this invariant (see Figure 5.6).

Figure 5.6. Calculating precondition for invariant WidgetsInStock' 0.

Working through simple examples such as this allows you to gain confidence that the technique yields results you intuitively know are true.