MORE INFORMATION ON Predicate_Interpretation.f
In computer programs, each branch point is associated with a predicate which evaluates to true or false. The outcome of the branch
that will be followed is determined by the value of the predicate. The path condition is the compound condition which must be
satisfied by the input data point in order that the control path be executed.
If each program variable appearing in the predicate is replaced by its symbolic value in terms of input variables, we get an equivalent
constraint which we call the predicate interpretation.
In the first predicate of this source, A > B, both A and B are input variables, so there is only one interpretation. The second
predicate, C <= 0, will have two interpretations, depending on which branch was taken in the first IF construct.
For paths on which the THEN C = B + 1 clause is executed, the interpretation is B + 1 <= 0 or, equivalently, B <= -1. When the ELSE
C = B - 1 branch is taken, the interpretation is B - 1 <= 0 or, equivalently, B <= 1. Within the second IF-THEN-ELSE clause,
a nested DO loop appears. The DO loop is executed:
no times if B < 1
The selection of a path will thus require some specification of the number of times that the DO loop is executed, and a corresponding
predicate is applied which selects those input points which will follow that particular path. Even though the third predicate,
D = 2, appears on multiple paths, it only has one interpretation, 2 * A + B = 2, since D is assigned to the value 2 * A + B in the
same statement in each path.
once if 1 <= B < 2
twice if 2 <= B < 3, etc.