internal action. An action in a model program that has no corresponding action in
the implementation and is not executed by the stepper. Internal actions are typically
used to select among test cases in a test suite.
intersection. A set that contains the elements shared by two sets. Or, the operation
on two sets that returns their intersection. In composition, the allowed traces of
the product belong to the intersection of the traces of the loop extensions of the
individual model programs.
invariant. A predicate that is supposed to be true in every state that is reachable.
Invariants express safety requirements.
invocation. A method call, including the method name and all of its arguments. Or,
the execution of that method call. The invocation of an action method is an action.
isomorphic states. States where there exists a substitution of abstract values that
makes them equal. Isomorphic means ???same shape.??? For example, states are isomorphic
if they store data structures which have the same shape and store the same
values, except for object IDs. Excluding isomorphic states can greatly reduce the
number of states that must be considered during exploration.
Appendices 323
IUT. Implementation Under Test.
lazy. An algorithm that does not compute an element until it is needed. The exploration
algorithm discussed in this book is lazy.
learn. What an adaptive strategy is said to do.
Pages:
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415