The property vector specification of a multiset iterator

Trace assertion specification methods constrain behaviour at the interface of a module by identifying legal sequences of calls to the module´s access programs. The legality of extending a trace by a call is specified by assertions that ex- press properties that the trace and call must satisfy. Trace specifications can often be simplified by formulating asser- tions about representative normal (or canonical) form traces, but this approach is only useful when convenient forms can be found. This paper: 1) introduces a new trace assertion method, called the Property Vector (PV) method, 2) demonstrates the method by specifying a multiset iterator module previously identified as difficult to specify [Lam90], 3) compares the PV method to other methods. The main new feature of the PV method is the use of a vector of property variables that explicitly represent relevant properties of a trace that influence a module´s future behaviour. It is possible to obtain a simple trace assertion specification for a module even though convenient (legal) normal/canonical form traces are not apparent. Normal/canonical form trace assertion methods are special cases of the PV method where the only relevant property of a trace is its equivalent normal/canonical form.