There is no algorithm or automated method
for deriving a model program ??“ we have to use judgment and intuition. But there
are systematic methods for validating a model program ??“ checking that it behaves
as we intended.
Writing a model program does not mean writing the implementation twice. A
model program should be much smaller and simpler than the implementation. To
achieve this, we usually select just a subset of the implementation??™s features to
model. A large implementation can be covered by several small model programs
that represent different subsets of features.Within each subset, we choose a level of
abstraction where we identify the essential elements in the implementation that must
also appear in the model. Other implementation details can be omitted or greatly
simplified in the model. We can ignore efficiency, writing the simplest model program
that produces the required behaviors, without regard for performance. Thanks
to all this, the model program is much shorter and easier to write than the implementation,
and we can analyze it more thoroughly. ???The size of the specification
and the effort required in its construction is not proportional to the size of the object
being specified. Useful and significant results about large program can be obtained
by analyzing a much smaller artifact: a specification that models an aspect of its
behavior.
Pages:
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30