
Preliminaries
by using an identifier associated with the next program statement. In the
case of programs in assembly language, the location of control can be
specified more precisely by giving the value of the program counter.
Each variable in the program corresponds to one element of this vec-
tor. Obviously, for a large program, such as the Unix OS, the state vec-
tor might have thousands of elements. Execution of program statements
causes the program to move from one state to the next. A sequence of
program states is termed as program behavior.
Example 1.13: Consider a program that inputs two integers into
variables X and Y, compares these values,