Information Technology Reference
In-Depth Information
APPend Ix A. deTer MInIng Bound S of QuAnTIf Ied VAr IABLeS
Deinition
(Boundedness of variables) A quantified variable
x
of type
T
is
•
Upper bounded,
iff there exists an expression
e
such that
x
≤
e
, where ≤ is a complete ordering
on type
T
;
•
Lower bounded,
iff there exists an expression
e
such that
x
≥
e
;
•
Fully bounded,
iff there exists an expression
e
1
and
e
2
such that
e
1
≤ x ≤
e
2
.
This is a recursive definition because boundedness of a variable may depend on boundedness of
other variables. For example,
x
≤ 1-
y
and
y
≥
0, or
x
≤ 1-
y
and
y
≤
0.
Because we will construct a verification program for the specification, we should know the value
domain that ought to be checked for a variable. Boundedness of variables ensures termination of the
evaluation process.
Bounds of variables are determined based on the following principles:
For clause ∀
x
.
p
, if
TH
├
x
≥
e
→
p
then
e
is an upper bound of
x
; otherwise, if
TH
├
x
≤
e
→
p
then
e
is a lower bound of
x
. Intuitively,
e
is regarded as an upper (lower) bound of
x
if any value greater
than
e
needs not to be checked because ∀
x
.
p
cannot be proved false in the domain that
x
≥
e
(≤
e
).
For clause ∃
x
.
p
, if
TH
├
x
≥
e
→ ¬
p
then
e
is an upper bound of
x
; otherwise, if
TH
├
x
≤
e
→ ¬
p
then
e
is a lower bound of
x
. Intuitively,
e
is regarded as an upper (lower) bound of
x
if any value greater
than
e
needs not to be checked because ∃
x
.
p
cannot be proved true in the domain that
x
≥
e
(≤
e
).
We call
e
the
upper
(
lower
)
bound of x
deduced from
∀
x
.
p
, written
e
= ↑
x
(∀
x.p
) (
e
= ↓
x
(∀
x.p
)) (Pre-
cisely, it should be written as
e
∈ ↑
x
(∀
x.p
) or
e
∈ ↓
x
(∀
x.p
)), or
from
∃
x
.
p
, written
e
= ↑
x
(∃
x.p
) (
e
= ↓
x
(∃
x.p
)), in the above cases. If there is no free occurrence of
x
in
p
, then we write ↑
x
(∀
x.p
) =
irrel
or ↑
x
(∃
x.p
) =
irrel
, which means that ∀
x.p
or ∃
x.p
is irrelevant to the upper bound of
x
. Some rules apply
to the lower bounds.
Search WWH ::
Custom Search