Databases Reference
In-Depth Information
This algorithm uses two helper functions:Get-Incoming-Events(shown
below) andGet-Outgoing-Events(which we leave as an exercise for the
reader; it is quite similar toGet-Incoming-Events).
Get-Incoming-Events(M)
1 Killed =Init-Killed-Variables(M)
2 //Initialize incoming events for each node
3 I = ;
4 for each node n in M
5 for each transition t ingoing into n
6 I[n] = I[n] [t:events
7 //Repeatedly update incoming events for each node
8
repeat
9
for each node n in M
10
for each predecessor p of n in M
11
t = transition from p to n in M
12
for each event e 2 I[p]
13
if var name:e 62 Killed [t]
14
I[n] = I[n] [feg
15
until I does not change anymore
16
return I
TheInit-Killed-Variablesnds variables \killed" by a transition. We will
leave providing an algorithm for this function as an exercise for the reader.
Applying theExtract-Sequential-Constraints algorithm to the
function model shown in Figure 12.3 results in the following sequential con-
straints being extracted:
retval of
Random()
target of
nextInt()
target of
nextInt()
target of
nextInt()
retval of
Stack()
target of
push()
retval of
nextInt()
1st arg of
push()
target of
push()
target of
push()
We call these sequential constraints a sequential constraints abstraction of
the function model they were extracted from. We can apply this algorithm to
function models of all functions of a program and thus arrive at a sequential
constraints abstraction of the program.
12.5 Finding Specifications
In Section 12.1 we said that we can represent specifications as sets of se-
quential constraints, and in the previous section we showed how to automat-
Search WWH ::
Custom Search