Hardware Reference
In-Depth Information
assignment to each variable in V of either
0
or
1
as a value. We can identify the
valuations of V naturally with the power set 2
V
, where U
2
2
V
corresponds to
the valuation that assigns
1
to each element in U and
0
to each element in V
n
U .
Since V
D
A
[
F is a partition, 2
V
!
2
A
defined by .U /
D
U
\
A. In terms of valuations, retains the values assigned
to the regular variables A and forgets the values assigned to the free variables F .
For example, suppose A
Df
a
1
;a
2
g
and F
Df
f
1
;f
2
g
.LetU
Df
a
1
;f
2
g
.Asa
valuation, U assigns a
1
D
1
, a
2
D
0
, f
1
D
0
, f
2
D
1
. Then .U /
Df
a
1
;f
2
g\
A
D
f
a
1
g
. As a valuation, .U / assigns a
1
D
1
, a
2
D
0
, and we simply drop the values
assigned to f
1
and f
2
.
We consider two kinds of traces, reduced and extended. A
reduced trace
is a trace
w
whose letters are valuations of regular variables only:
w
i
D
2
A
2
F
and there is a projection
W
2
V
2
2
A
;i
D
0; 1; : : :.An
extended trace
is a trace W whose letters are valuations of all variables, both regular
and free: W
i
!
2
A
can be applied letter-
wise to define
projection
of an extended trace to a reduced trace. We use the same
notation for this projection of traces: if W is an extended trace, then .W / is the
reduced trace obtained from W by forgetting the values assigned to the free variables
in each letter. In other words, .W /
D
w
iff .W
i
/
D
w
i
for all i
D
0; 1; : : :.
Assertion satisfaction is naturally defined in terms of extended traces, where
all variables that may be referenced by the assertion are included (see Sect.
21.3
).
To define formal semantics for free variables, we need to define assertion satisfac-
tion in terms of reduced traces, which contain regular variables only. The definition
is as follows. Assertion p is
satisfied
on reduced trace
w
, written
w
ˆ
p,iffp is
satisfied in the usual sense on all extended traces W that project to
w
. In other words,
2
2
V
;i
D
0; 1; : : :. The projection
W
2
V
w
ˆ
p
iff
8
W s.t. .W /
D
w
W
W
ˆ
p
This universal quantification over extended traces makes precise the sense in which
free variables are universally quantified over their domains.
23.1.2
Free Variables in Assumptions
What happens if free variables are referenced within assumptions? To keep the
notation clear, we will assume that there is one free variable
v
, two assumptions
q
1
and q
2
and two assertions p
1
and p
2
. We will talk only about the meaning of the
evaluation attempt starting at the beginning of the trace. Property p
1
in the presence
of the assumptions is equivalent to property q
1
^
q
2
!
p
1
. Analogously, p
2
is
equivalent to property q
1
^
q
2
!
p
2
. As we discussed in Sect.
23.1.1
, the values of
v
in formulas q
1
^
q
2
!
p
1
and q
1
^
q
2
!
p
2
are taken independently. In order for
q
1
^
q
2
!
p
j
to hold, it is sufficient to check on a given trace that p
j
holds for all
values of
v
that satisfy both assumptions q
1
and q
2
.
Search WWH ::
Custom Search