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

defined in a standard way as follows:
L \ 2 2 objects \
v \ 2 Val = objects \ [fnullg
\ 2 Env = VarId ! Val
\ 2 Heap = objects \ FieldId ! Val
state \ = hL \ ; \ ; \ i 2 States = 2 objects \ Env Heap
where objects \ is an unbounded set of dynamically allocated objects, VarId is
a set of local variable identifiers, and FieldId is a set of field identifiers.
A program state keeps track of the set L \ of allocated objects, an environ-
ment \ mapping local variables to values, and a mapping \ from fields of
allocated objects to values.
In our instrumented semantics, each concrete object is mapped to a \con-
crete history" that records the sequence of events that has occurred for that
object. Technically, we define the notion of a history which captures a regular
language of event sequences.
Denition 6.4.1. A history h is a nite automaton (;Q; init;;F), where
F 6= ;. F is also called the set of current states. We dene the traces repre-
sented by h, Tr(h), to be the language L(h).
A concrete history h \ is a special case of a history that encodes a single
finite trace of events, that is, where Tr(h \ ) consists of a single finite trace of
events. In Section 6.4.2 we will use the general notion of a history to describe
a regular language of event sequences. We refer to a history that possibly
describes more than a single trace of events as an abstract history.
Example 6.4.2. Figure 6.3 shows examples of concrete histories occurring
for a SocketChannel object of the example program at various points of the
program. Figure 6.6 and Figure 6.7 show examples of abstract histories de-
scribing regular languages of events. In all figures, current states are depicted
as double circles. Note that the automaton corresponding to an abstract history
may be non-deterministic (e.g., as shown in Figure 6.7).
We denote the set of all concrete histories by H \ . We augment every con-
crete state hL \ ; \ ; \ i with an additional mapping his \ : L \ * H \ that maps
an allocated object of the tracked type to its concrete history. A state of the
instrumented concrete semantics is therefore a tuple hL \ ; \ ; \ ;his \ i.
Given a state hL \ ; \ ; \ ;his \ i, the semantics generates a new state
hL \ 0 ; \ 0 ; \ 0 ;his \ 0 i when evaluating each statement. We assume a standard
interpretation for program statements updating L \ , \ , and \ . The his \ com-
ponent changes when encountering object allocations and observable events:
Object Allocation: For a statement x=newT() allocating an object of
the tracked type, a new (fresh) object l new 2 objects \ nL \ is allocated,
and his \ 0 (l new ) = h \ 0 , where h \ 0 = (;finitg; init; 0 ;finitg) and 0 is