10, 3.11, and 3.13. For example,
consider the following sequence of assignment statements (where ???%???
denotes a modulus operator):
S1: r := a % b;
29
Path-Oriented Program Analysis
a := b;
b := r;
r := a % b;
a := b;
b := r;
We cannot simplify this sequence with the previously mentioned
corollaries. Nevertheless, if we perform a symbolic execution of this
sequence of statements with the symbolic values: a ?†? A, b ?†? B, and
r?†?R, the net result will be
r ?†? B%(A%B)
a ?†? A%B
b ?†? B%(A%B)
Some reflection will show that this result can be produced by using
the following sequence of assignment statements:
S2: a := a % b;
b := b % a;
r := b;
That is to say, the previous S1 can be reduced to S2.
30
4
Program Set
Asmentioned before, by inserting a constraint into a program,we shrink
the domain for which it is defined. To reverse this process, we need to
be able to speak of, and make use of, a set of subprograms. To this end,
a new programming construct called a program set is now introduced.
The meaning of a program set, or a set of programs, is identical to the
conventional notion of a set of other objects.As usual, a set of n programs
is denoted by {P1, P2, . . . , Pn}. When used as a programming construct,
it describes the computation prescribed by its elements. Formally, the
semantics of such a set is defined in Axiom 4.
Pages:
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53