我正在尝试使用Frama-C（Neon-20140301）和Alt-Ergo的WP教程示例。我陷入了“不匹配算法”的例子，而其他类似的例子，例如“等于”和“找到”则没有问题。该代码在下面列出。后置条件P0，P2没有释放。谁能告诉我这是怎么回事？
#include<stdbool.h>
/*@
@ predicate IsEqual {A,B} (float* a, integer n, float* b) =
@ \forall integer i; 0 <= i < n ==> \at(a[i], A) == \at(b[i], B);
*/a
/*@ requires n >= 0;
@ requires \valid(a+(0..n-1));
@ requires \valid(b+(0..n-1));
@
@ assigns \nothing;
@
@ behavior all_equal:
@ assumes IsEqual{Here,Here}(a, n, b);
@ ensures P0: \result == n;
@
@ behavior some_not_equal:
@ assumes !IsEqual{Here,Here}(a, n, b);
@ ensures P1: 0 <= \result < n;
@ ensures P2: a[\result] != b[\result];
@ ensures P3: IsEqual{Here,Here}(a, \result, b);
@
@ complete behaviors;
@ disjoint behaviors;
*/
bool mismatch (float* a, int n, float* b)
{
/*@ loop invariant 0 <= i <= n;
@ loop invariant IsEqual{Here,Here}(a, i, b);
@ loop assigns i;
@ loop variant n-i;
*/
for (int i=0; i<n; i++) {
if (a[i] != b[i])
return i;
}
return n;
}
您的函数应该返回a bool，即0或1。x可以将任何整数值转换为_Bool：布尔值0ifx==0和1else（请参见C99和C11的6.3.1.2节）。如果您查看由Frama-C规范化的代码，则正是针对return i和进行的操作return n。因此，没有理由\result等于n或两个数组都不相同的索引。如果您让函数返回an int，则所有内容都会由Alt-ergo释放。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句