Guaranteed specs

Action A complex dialog presented with a single overall pre/post or rely/guarantee spec. 

I did manage to band-aid the problem shortly after my arrival at the Singapore-based company I worked for, and they did manage to slip the bad parts into their high volume production, with no future ppm issues either. Though understandably they didn t return to the previous vendor to renew their learnings on what constitutes a guaranteed spec and what is not. 

To write a single complete spec for the action—for example, to define in one contract what the implementor must code, and the caller must be careful of before invocation— both forms are equivalent. The explicit pre/post form makes the client responsibility a bit more visible. The caller is responsible for invoking this operation only when the precondition is true the implementor can assume the precondition is satisfied and must then guarantee the postcondition. 

To define an outcome that must be guaranteed if your precondition holds, regardless of other partial specs, use a ==> b. 

Pre, post, rely, and guarantee conditions are called assertions. Two further assertions appear in a type specification, outside any one action spec inv condition True before and after every action in the model. Effectively anded to each pre- and postcondition. 

A state chart in a component spec refers to the component s behavior (see Figure 5.11). It can focus on one of the component s model types, but again, there is no guarantee that such a class will exist in an implementation, only that the information it represents will be implemented. 

Sometimes, however, you want to write a specification that makes guarantees for certain cases when these cases may overlap with others. In this case you can use an alternative style for writing the spec do not use an explicit precondition but instead describe the case within the postcondition itself. Here we use the same composition mles ... 

The joined spec would make one guarantee for one case and another guarantee for the second case (the two cases happen to be disjoint in this example). 

An implementation of the resulting operation spec is guaranteed to meet the expectation of anyone who expected either T1 or T2. An invocation of m is valid whenever A is hue (because that would make (A or B or C) true) and is guaranteed to result in X (and perhaps also Y, Z depending on whether B or C was also true). 

Typically, however, you want to deal with multiple possible exception outcomes in a more flexible manner. If you place an on-line order, given the preceding spec, what should happen if the credit card number and address are both invalid Which exception should be raised It is best to leave to the implementor the choice of which exception to signal as long as failure indication is guaranteed. This technique helps with composition of specifications, each with its own exception conditions, as is the case of failures in distributed systems. Hence ... 

---