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

Soundness is achieved by making sure that every reachable (instrumented)
concrete state istate \ is represented by some reachable abstract state istate,
meaning that for every object o \ 2 L \ there exists a factoid ho; heap-data;hi
in istate that provides a sound representation of o \ . This is a factoid whose
heap-data component fulfills the conditions described in [11], and in addition
h is a sound representation of his \ (o \ ), i.e., Tr(his \ (o \ )) Tr(h). Soundness
of h 0 , the extend transformer, and of the merge operator ensures that the
analysis is sound.

Definition 6.4.5. An abstract extend transformer extend is sound, if
whenever Tr(h \ ) Tr(h) then for every 2 , Tr(extend \ (h \ ;))
Tr(extend(h;)).
Definition 6.4.6. A merge operator F is sound, if for every set of abstract

histories H H, S h2H Tr(h) S h2 F H Tr(h).

Precision. The analysis is precise when it does not introduce additional be-
haviors to those that are permitted by the code base, i.e.,
[

Tr(h \ ) = [
h2H C

Tr(h)

h \ 2H \ C

Remark. In practice, instead of considering the traces represented by all the
abstract histories generated by the analysis, we consider the prefix-closures of
the history automata at the exit points of the program, obtained by setting
F 0 = Q (i.e., all the states are considered accepting). The set of observed
traces is maintained when we restrict ourselves to the prefix-closures of these
automata since all other traces are prefixes of the traces represented by them.

6.4.2.3 History Abstractions

We present a parameterized framework for history abstractions, based on
intuition regarding the structure of API specifications.
Quotient-Based Abstractions. In practice, automata that characterize
API specifications are often simple, and further admit simple characteriza-
tions of their states (e.g., their ingoing or outgoing sequences). Exploiting this
intuition, we introduce abstractions based on quotient structures of the his-
tory automata, which provide a general, simple, and often precise framework
to reason about abstract histories.
Informally, given an equivalence relation R and some merge criterion,
the quotient-based abstraction generalizes histories based on their quotient
structures w.r.t. R. The merge criterion is used to determine which abstract
histories are merged by the merge operator. More precisely, we define the
quotient-based abstraction of R as follows.
The abstraction h 0 of the empty-sequence history is Quo R (h \ 0 ) = h 0 ,
i.e., the empty-sequence history.