Static Specification Mining Using Automata-Based Abstractions* - Mining Software Specifications: Methodologies and Applications - page 176

After merge

rd

fin

fin fin rd fin wrt 3 rd

fin

cfg cnc

fin

End of for
iteration

0 1 2 5

cfg cnc fin

cfg cnc fin rd cfg cnc fin wrt

0 1 2 5 fin

0 1 2 3 5 0 1 2 4 5

4 wrt

wrt

rd

6 rd

cnc

fin

3

fin
fin

cnc

cfg

No change

sc.connect(2)

0 1 2

4

fin

wrt wrt

FIGURE 6.7: Abstract interpretation with future abstraction (exterior
merge).

fg for every state q. As a result, R[k; 0] collapses to a relation that considers
ingoing sequences of length k. We refer to it as R k past , and to the abstraction as
the k-past abstraction. Similarly, R[0;k] refers to outgoing sequences of length
k, in which case we also refer to it as R k future . We refer to the corresponding
abstraction as the k-future abstraction. Intuitively, analysis using the k-past
abstraction will distinguish patterns based only on their recent past behavior,
and the k-future abstraction will distinguish patterns based only on their near
future behavior. These abstractions will be effective if the recent past (near
future) suces to identify a particular sequence.
Merge Criteria. Having defined equivalence relations, we now consider
merge criteria to define quotient-based abstractions. A merge criterion will
determine when the analysis should collapse abstract program states, thus
potentially losing precision, but accelerating convergence.
We consider the following merge schemes.
None: Each history comprises a singleton set in the partition. This
scheme is most precise, but is impractical, as it results in an exponential
blowup.
Total: The partition consists of a single set that contains all histories,
i.e., all histories are merged into one.
Exterior: The histories are partitioned into subsets in which all the
histories have compatible initial states and compatible current states.
Namely, histories h 1 and h 2 are merged only if (a) (init 1 ; init 2 ) 2 R;
and (b) for every q 1 2F 1 there exists q 2 2F 2 s.t. (q 1 ;q 2 ) 2R, and vice
versa.
Intuitively, the total criterion forces the analysis to track exactly one ab-
stract history for each \context" (i.e., alias context, instance key, and program
point).
The exterior criterion provides a less aggressive alternative, based on the
intuition that the distinguishing features of a history can be encapsulated
by the features of its initial and current states, which we refer to as the
\exterior" of the history. The thinking follows that if history states dier only