java - 在 Java 中使用“KeyY”进行形式验证无法证明数组重置循环
问题描述
目前,我正在尝试使用 Java 程序的Key工具进行一些形式验证。
这是我的带注释的 Java 代码:
public class Test {
public int[] a;
/*@ public normal_behavior
@ ensures (\forall int x; 0<=x && x<a.length; a[x]==1);
@*/
public void fillArray() {
int i = 0;
while(i < a.length) {
a[i] = 1;
i++;
}
}
}
令我惊讶的是 Key,它无法证明当前程序根据其规范是有效的。Key在目标 54 失败。当前目标窗口显示:
self.a.<created> = TRUE,
wellFormed(heap),
self.<created> = TRUE,
Test::exactInstance(self) = TRUE,
measuredByEmpty
==>
self.a = null,
self = null,
{exc:=null || i:=0}
\<{
try {
method-frame(source=fillArray()@Test, this=self)
: {
while (i<this.a.length) {
this.a[i] = 1;
i++;
}
}
}
catch (java.lang.Throwable e) {
exc = e;
}
}\> (\forall int x; (x <= -1 | x >= self.a.length | self.a[x] = 1) & self.<inv> & exc = null)
我不太明白:未能证明规范的主要原因是什么?
解决方案
失败的最基本原因是,如果证明者在一个方法中发现了一个无限循环——那么它就不能遵循一个没有循环不变规范的方法规范。
因此,对于每个无界循环,我们必须指定一个循环不变量。循环不变量是对每个循环迭代都适用的规则。每个循环都可以有自己特定的不变规则。因此,具有规范的 Java 代码必须固定为:
public class Test{
public int[] a;
/*@ public normal_behavior
@ ensures (\forall int x; 0<=x && x<a.length; a[x]==1); // method post-condition
@ diverges true; // not necessary terminates
@*/
public void fillArray() {
int i = 0;
/*@ loop_invariant
@ 0 <= i && i <= a.length && // i ∈ [0, a.length]
@ (\forall int x; 0<=x && x<i; a[x]==1); // x ∈ [0, i) | a[x] = 1
@ assignable a[*]; // Valid array location
@*/
while(i < a.length) {
a[i] = 1;
i++;
}
}
}
思考如何指定方法最难的部分是找出循环不变量。但同时 - 这是最有趣的。出于某种原因,我将重复此循环的不变量:
i ∈ [0, a.length]
x ∈ [0, i) | a[x] = 1
而且这个条件在任何迭代中都不会在循环中改变。这就是为什么它是一个不变量。
顺便说一句,如果正确地完成正式规范 - 我们可以将TDD和单元测试扔到窗外。如果程序可以根据其规范在数学上被证明是正确的,那么谁会关心运行时结果呢?
如果规范很好并且代码语义得到证明——那么程序执行中就不会出错——这是肯定的。正因为如此 - 正式验证是一个非常有前途的领域。
推荐阅读
- python - python-shell历史
- apache - 防止 htaccess 将 ¤ 更改为符号
- msbuild - MSBuild Force Item Include 被视为自定义/文字
- python-2.7 - Python2.7:我可以为 ODE 求解器中雅可比行列式的前向差分近似设置步长吗?
- c++ - tcp & ipc 的 zmq_bind 段错误
- r - 不包含父目录的 zip 文件
- ruby-on-rails - 使用 Mina 时无法通过 ssh 连接到服务器
- ruby - Ruby 中的指针
- azure - Azure KeyVault:SPN KeyVault 访问被拒绝
- java - postgresql / 真空中的大量活/死元组不起作用