specification. A description of what a program, component, or system is supposed
to do. A specification should be a complete description of behavior that describes
328 Glossary
everything the system must do, might do, and must not do. A model program can
act as a specification. Contrast to design.
split action. A pair of actions, the start action and the finish action, associated with
the call and return of a single action method that has a return value and/or out or
byref parameters. Contrast to atomic action.
start action. The first action in a split action, associated with the call of the action
method.
state. The information stored in a system at one point in time. In a model program,
the state is the collection of all state variables and their values.
state filter. A predicate that must be satisfied in the next state of a transition for
that transition to be included in exploration. State filters are a pruning technique.
state grouping. A collection of states that have the same value for a state property.
In exploration, a pruning technique can exclude a state that does not provide a new
value for one of the properties. In testing, an adaptive strategy can select actions
that lead to state groupings that have not yet been visited.
state-independent. A method that does not read or update any state. It only reads
its parameters and returns a value.
Pages:
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424