You may consult pages 39-41 in the thesis
"Code Obfuscation and Malware Detection by Abstract Interpretation"
of M. Dalla Preda about formal obfuscation; or sections 4.4 and 4.5 in the orignal paper
"Systematic Design of Program Transformation Frameworks by Abstract
Interpretation"
of Cousot and Cousot.
The theory is formal and requires much more technical details than the following interpretation, but the idea is that:
The "finite trace" semantics of a program P
is defined by the set of all finite traces of P
. A trace is nothing but a finite sequence of states of P
, obtained when running P
, step-by-step over "commands" of P
.
(You may note that, from a state, we can get a set of possible next states, because the command at this state can be nondeterministic: it can receive some value from environment).
To calculate the finite trace semantics of P
, one way (which one is refered in your book) is to use a function F
defined from FinSeqs to FinSeqs:
F : FinSeq -> FinSeq
where FinSeqs
is the set of all "sub-set of finite sequences of states of P
" (you may think that each sub-set is a possible value for the "finite trace" semantics of P
).
This function F
map a sub-set X
to a sub-set X'
so that each trace x'
of X'
has a trace x
of X
as suffix (that is the reason why it is called "backward" in the paper of Cousot and Cousot). Particularly, we have that
x' = sj . x
x = si . x1
and sj
must be able to be a next state of si
. The least fixpoint of the function F
, namely some set Xp
so that
F(Xp) = Xp
is called the trace semantics of P
.