![](https://csdnimg.cn/release/download_crawler_static/88626862/bg4.jpg)
M. Elder
等人
/
理论计算机科学电子笔记
267
(
2010
)
43
如果
x*x >= 4,则
(
a)
x = x+1
(
b)
assert(x*x> 0)(c)
图二. 的示例程序
2
视图和视图维护
例
2.1为了演示视图扩充的效用,考虑使用区间抽象域分析图2中的程序片段。
假设
分析器
已经
发现
x
<$
→
[
-2
,
2
]
恰好
在
线
(a)之前成立
。
B
e
-
行
(a)上的测试的原因
,
x
∈
{−
2
,
2
}
刚好在行
(b)之前。
因此,就在行
(c)之前,
我们有
x
∈
{−
1
,
3
}
,因此行
(c)的断言总是
为真(因为
−1
<
$−1
>
0和3
<
$3
>
0)。
不幸的是,区间域不能以足够的精度表示信息x 2
,
2
,
这在(b)行之前成立
:
过度逼近x的最精确的区间域事实 二
、
二人 是x [ (2
,
2)表示 集合2
,
1
,
0
,
1
,
2
。
因此,就在第
(c)
行之前,我们有x[1
,
3],并且由于0γ([1
,
3]),根据区间域,x*x的值可以等于0-即使x*x使用最精确的区间平方运算来计
算。因此,分析器不能证明
(c)行的断言。
现在假设我们用视图变量
v
xx
来增加区间抽象,
以跟踪表达式x*x的值。 增强
区间抽象
意味着我们用一个额外的变量来增强抽象状态(即,一个辅助
维度),
它跟踪
v
xx
的值
。再次假设分析器
发现
x
<$
→
[
-2
,
2
]
恰好
在
直线
(a)之
前成立
。
view-variable必 须以 合 理的 初 始值 开 始。 我 们可 以 通 过 直接 计 算x*x
=
[−
2
,
2
]
·
[−
2
,
2
]
=
[−
4
,
4
]来 获 得 这 样 的值 。 因 此 ,
初 始 抽 象
状 态
是
{
x
[
−
4
,
4]
}
。
(
如果
x*
x
被
解释 为平 方
运 算
,
我 们
将
获 得
{
x
<$
→
[
-2
,
2
]
,
v
x
<$
x
→
<$
[0
,
4]
}
。)
就在第
(b)
行之前
,
我们希望视图变量
v
x
x
的值能够捕获x*x >= 4的假设。
此外,在抽象解释
(a)
行时
,
对视图变量
v
x
x x
x
的操作都应该是区间抽象域支
持的标准操作。为了获得这个结果,我们将表达式x*x解释为对视图变量
v
x x
x
的
访问,并将
假设
x*x >= 4的抽象Transformer(行
(a))
表示为
λ z
.z
H
{
x <
$
→
,
T
v
x
<$
x<$<$
→
[4
,
∞
]
}
=
λ z
.
z
[
v
x
<$
x
<$$>
→
(
z
(
v
x
<$
x
)
H
[4
,
∞
])]
}
。
在第
(b)
行之前的抽象状态变为
{
x
<$
→
[
−
2
,
2]
,
v
x<
$x
<$
→
[4
,
4]
}
,
(1
)
其捕获了x*x只有一个可能的具体值即4的事实。