我相信我漏掉了一些明显的东西，但我尝试了很多，但我没有设法找到问题的根源。
我是按照acsl 指南 从Frama-C.有这个介绍性的例子，如何验证在数组中寻找最大值的正确性。
/*@ requires n > 0;
requires \valid(p+ (0 .. n-1));
ensures \forall int i; 0 <= i <= n-1 ==> \result >= p[i];
ensures \exists int e; 0 <= e <= n-1 && \result == p[e];
*/
int max_seq(int* p, int n) {
int res = *p;
for(int i = 0; i < n; i++) {
if (res < *p) { res = *p; }
p++;
}
return res;
}
然而，运行 frama-c -wp -wp-prover alt-ergo samenum.c -then -report 我明白了。
[wp] Warning: Missing RTE guards
[wp] samenum.c:8: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_max_seq_ensures_2 : Timeout (Qed:1ms) (10s)
[wp] [Alt-Ergo] Goal typed_max_seq_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals: 0 / 2
Alt-Ergo: 0 (interrupted: 2)
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'max_seq'
--------------------------------------------------------------------------------
[ - ] Post-condition (file samenum.c, line 3)
tried with Wp.typed.
[ - ] Post-condition (file samenum.c, line 4)
tried with Wp.typed.
[ - ] Default behavior
tried with Frama-C kernel.
似乎alt -ergo在证明属性之前就超时了。值得一提的是，我试过用更高的超时，但还是不行。
我使用的是
我在Ubuntu 18.04上运行这个命令，在运行命令之前，我运行了以下命令。why3 config --detect 以确保 why3 知道 alt-ergo。
有什么好办法吗？有谁能验证一下这个例子是不是行不通？
这个小教程是很久之前写的，并不是真正的最新版本。新版本的网站应该会在未来几个月内出现。基本上，这个合同，以及@iguerNL指出的循环的不变式都是要用Jessie插件，而不是Frama-C的WP插件来验证的。在这两个插件的不同之处中，Jessie不需 assigns 循环和函数的子句，而WP需要它们。
因此，一个完整的注释的 max_seq 函数可以是这个。
/*@ requires n > 0;
requires \valid(p+ (0..n−1));
assigns \nothing;
ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i];
ensures \exists int e; 0 <= e <= n−1 && \result == p[e];
*/
int max_seq(int* p, int n) {
int res = *p;
//@ ghost int e = 0;
/*@ loop invariant \forall integer j; 0 <= j < i ==> res >= \at(p[j],Pre);
loop invariant \valid(\at(p,Pre)+e) && \at(p,Pre)[e] == res;
loop invariant 0<=i<=n;
loop invariant p==\at(p,Pre)+i;
loop invariant 0<=e<n;
loop assigns i, res, p, e;
loop variant n-i;
*/
for(int i = 0; i < n; i++) {
if (res < *p) {
res = *p;
//@ ghost e = i;
}
p++;
}
return res;
}
我们指定函数不在内存中分配任何东西, 而循环分配不同的本地变量。i, res, p 和 e (从而使 n 不变）。)
需要注意的是，最近有更多的教程，可以了解Frama-C与WP插件的使用。未来版本的Frama-C网站提到。
你可能忘了为 "for "循环添加不变量。参见你给的手册中的 "10.2 循环不变量" (https:/frama-c.comacsl_tutorial_index.html。)