Every program or system starts up in an initial state. The initial state is usually
an empty or idle state. Behavior continues until the system reaches an accepting
state. An accepting state is usually a state where the program??™s goals have been
achieved, where some unit of work has been completed. The system may stop in
an accepting state; alternatively, it may continue, starting new work. A sequence of
actions beginning in the initial state and ending in an accepting state is called a run
or a trace. A run must not end in a state that is not an accepting state (if the model
program does not identify any accepting states, a run may end in any state). The
runs of a model program are sequences of method calls (and returns).
The behavior of a program or system is the complete collection of all the runs
that it can execute. A contract model program is a specification that describes
all of the allowed behavior of its implementation: it describes everything that its
implementation must do, might do, and must not do. Every run that a contract
model program can execute represents a run that its implementation must be able to
execute. A contract model program cannot execute any run that its implementation is
forbidden to execute. A contract model program often has a large collection of runs;
1 This is a simplification; the relation between actions in the implementation and methods in the
model program is not always one-to-one.
Pages:
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99