Why Does This Work?


Why Does This Work?!

If you are completely happy to use this technique for calculating preconditions without having to know why it works, feel free to skip this next bit. Trying to explain why the precondition results from the postcondition and invariant is probably harder to do than actually doing it. For an intuitive explanation, let's think back to some things you may remember learning in algebra. Let's take this equation:


You'll recall that given a single equation such as this, there are an infinite number of solutions (values of x and y), and you may remember having to graph equations like this one to visualize all the possible values of x and y that satisfy this equation. Figure 5.3 is a graph for this equation; the line stretches to infinity in both directions.

Figure 5.3. Graph of points satisfying equation.


If we now add a second equation to the first and consider the two simultaneously as a pair, the second equation constrains the values of x and y to be those that not only satisfy the first equation, but also the second:


This is visualized by graphing these two equations together; the two lines intersect at x=4 and y=8, the one solution that simultaneously satisfies both equations (see Figure 5.4).

Figure 5.4. Intersection of lines shows value satisfying both equations.


While graphing simultaneous equations is one way to solve themand it certainly helps to visualize what is going on (i.e., you are looking for the set of values where the two equations overlap)the preferred method is the "algebraic solution." You start with the original equations:


Now take the value of y from the first equation, and substitute it in the second equation:


Then simplify:


You could then substitute the value for x (i.e., 4) into either of the original equations to give you the value of y:


Now let's apply this idea to calculating preconditions. Previously we said the postcondition, precondition, and invariant work together as a unit. We can use our lesson from simultaneous equations to get a feel for the role each plays. Let's start with this postcondition from our example:


For what values of CheckAmount, GiftCardValue, and PriceOfItem is this equation valid? We know from our previous algebra example that it is valid for an infinite number of values, some of which might result in undesired behavior (e.g., when PriceOfItem is negative). So, we decide to constrain the values by adding a second equation, actually an inequality:


This inequalityour invariantwas selected to constrain the values to ones that we felt were safe (i.e., we should never be writing checks for greater than the original gift card's value). So the postcondition and invariant are like simultaneous equations from algebra. And solving simultaneous equationseither graphically or algebraicallyinvolves looking for the set of values that simultaneously satisfy both equations, and that… you guessed it…is what the precondition is: the set of values that simultaneously satisfy both the postcondition and invariant (see Figure 5.5).

Figure 5.5. Venn diagram illustration of precondition as those values which simultaneously satisfy the postcondition and invariant.


So, at least in principle, you learned everything you need to know about computing preconditions from postconditions and invariants in algebra class!



Succeeding with Use Cases. Working Smart to Deliver Quality
Succeeding with Use Cases: Working Smart to Deliver Quality
ISBN: 0321316436
EAN: 2147483647
Year: 2004
Pages: 109

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net