Closing Thoughts

Remember that in the last chapter I talked about Blue Collar Formal Methods, my concept of scaling down a formal method to something easier to learn and use that still affords a little rigor, but with little or none of the math.^[12] With just a few simple extensions to Binder's operational relation decision table concept, you have what makes for a decent Blue Collar Model-based Specification of a use case, namely:

^[12] See Chapter 5, the "The Absolute Least You Need to Know: One Fundamental Lesson and Three Simple Rules" section.

• Use of unprimed and primed state variables for operational variables in the style of Figure 6.4 to raise visibility to state change in the use case and allow you to talk about the before and after versions of state variables when describing preconditions, postconditions, and invariants.

• Expansion of the table format in the style of Figure 6.4 to allow a row per use case step's precondition, postcondition, and invariant.

• Dispense with the math and instead describing your preconditions, postconditions and invariants in natural language while following the "one fundamental lesson and three simple rules" from Chapter 5.^[13]

  ^[13] Again, see Chapter 5, the "The Absolute Least You Need to Know: One Fundamental Lesson and Three Simple Rules" section.

The operational relation extended with a few tricks from model-based specification is a winning combination not only for test design, but use case analysis in general.