S1
S2
/\B;
/\?¬B;
if B then S1 else S2
A loop formed by an edge associated with programming construct
S is used to represent a program set whose elements are all possible
concatenations of S.
50
Pathwise Decomposition
S
S*
To be more specific, S* is defined as
S??— ?‡” {?», S, S;S, S; S; S, S; S; S; S, . . .}
?‡” ???U
n=0
Sn
where Sn denotes a concatenation of n S??™s, and ?» (= S0) is the identity
under the operation of concatenation, i.e., a special programming construct
having the property that ?»;S?‡”S;?»?‡”S for any S. It corresponds
to a null statement or a NO-OP operation in a machine code.
A loop construct of the form while B do S can thus be represented by
the program graph in the following figure,
/\?¬B;
/\B;S
while B do S
and by expression (/ \B;S)*;/ \?¬B in the language of regular expressions.
For example, consider the following program:
read(a, b, c);
w := b ??“ a;
while (w > e)
begin
p := a + w / 3;
u := f(p);
q := b ??“ w / 3;
v := f(q);
if (u < v)
a := p;
51
Path-Oriented Program Analysis
else
b := q;
w := b ??“ a
end;
max := (a + b) / 2;
print (max);
According to the graphic representation scheme just described, this program
can be represented by the following program graph:
?±
??
?? ??
?µ
?·
where ?±: read (a, b, c);
w := b ??“ a;
??: / \ w > e;
p := a + w / 3;
u := f(p);
q := b ??“ w / 3;
v := f(q);
??: / \ u ?‰? v;
b := q;
??: / \ u < v;
a := p;
: w:= b ??“ a;
?·: / \ w ?‰¤ e;
max := (a + b) / 2;
print(max);
52
Pathwise Decomposition
Because the paths in a graph can be described by a regular expression
over the symbols assigned to each edge, we can now speak of the trace
subprograms ?±?????·, ?±?????·, ?±?????????·, and so on.
Pages:
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73