NET. However, this technology is not just for .NET applications. We
can use it to analyze and test programs that run outside .NET, on any computer,
under any operating system. Moreover, the concepts and methods are independent
of this particular technology, so this book should be useful even if you use different
languages and tools.
In the following sections we briefly describe what the technology can do. Explanations
of how it works come later in the book.
1.1 Model programs
We express what we want the program to do ??“ the specification ??“ by writing another
much simpler program that we call a model program. We can also write a model
program to describe a program unit or component ??“ in that case, it expresses part of
the design. The program, component, or system that the model program describes
is called the implementation. A single model program can represent a distributed
system with many computers, a concurrent system where many programs run at the
same time, or a reactive program that responds to events in its environment.
A model program can act as executable documentation. Unlike typical documentation,
it can be executed and analyzed automatically. It can serve as a prototype.
With an analysis tool, it can check whether the specification and design actually
produce the intended behaviors. With a testing tool, it can generate test cases, and
can act as the oracle that checks whether the implemenation passes the tests.
Pages:
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28