gpt4 book ai didi

c - ACSL - 无法证明功能

转载 作者:行者123 更新时间:2023-11-30 17:05:58 26 4
gpt4 key购买 nike

我试图证明这个功能,但没有成功。我还使用了另一个函数,但我证明了它。

有人可以帮助我吗?

        I'm using Frama-C Sodium version with Alt-ergo 3 as prover.

Given a not-empty string x. An integer number p such that
0 < p ≤|x| is meant to be "a period of x" if

x[i] = x[i + p]

for i = 0, 1, ... , |x| − p − 1.
Note that, for each not-empty string, the length of the string
is a period of itself. In this way, every not-empty string
has got at least one period. So is well formed the concept of minimum
period of string x, denoted by per(x):

per(x) = min { p | p is period of x }.

Write a C function

unsigned per(const char x[], unsigned l)

that, given a string x of length l, returns per(x).

这是我迄今为止编写的代码和规范:

/*@ 
requires l > 0;
requires p >= 0;

behavior zero:
assumes p == l;
ensures \result == 1;

behavior one:
assumes l != p && (l%p) == 0;
assumes \forall int i; 0 <= i < l-p-1 ==> x[i] == x[i+p];
ensures \result == 1;

behavior two:
assumes l != p && (l%p) == 0;
assumes !(\forall int i; 0 <= i < l-p-1 ==> x[i] == x[i+p]);
ensures \result == 0;

behavior three:
assumes p != l && l%p != 0;
ensures \result == 0;

complete behaviors;
disjoint behaviors;
*/

unsigned has_period(const char x[], unsigned int p, unsigned l) {
if (p == l) return 1;
if ((l % p) != 0) return 0;
/*@
loop assigns i;

loop invariant \forall int j; 0 <= j < i ==> (x[j] == x[j+p]);
loop invariant i <= l-p-1;
loop invariant i >= 0;
*/

for (int i = 0 ; i < l-p-1 ; ++i) {
if (x[i] != x[i + p])
return 0;
}

return 1;
}

/*
predicate has_period(char* x, unsigned int p, unsigned l) =
\forall int i; i < (l-p-1) ==> x[i] == x[i+p];
*/

/*@
requires l > 0;
requires \valid(x+(0..l-1));

ensures 1 <= \result <= l;
ensures \forall unsigned int i; i < (l-\result-1) ==> x[i] == x[i+\result];
ensures \forall unsigned int p; 1 <= p < \result ==> !(\forall int i; i < (l-p-1) ==> x[i] == x[i+p]);
*/

unsigned per(const char x[], unsigned l) {
int p = 1;

/*@
loop assigns p;

loop invariant 1 <= p <= l;
loop invariant \forall unsigned j; 1 <= j < p ==> !(\forall int i; i < (l-j-1) ==> x[i] == x[i+j] || (l%p) == 0);
loop invariant p >= 0;
*/

while(p < l && !has_period(x,p,l))
++p;

return p;
}

最佳答案

如果您告诉我们您的具体问题是什么,而不是笼统地说“它不起作用”,那将会有所帮助,但这里有一些要点:

  • 您的契约(Contract)缺少分配条款。使用 WP 时,这些不是可选,特别是对于在开发中调用的诸如 has_period 之类的函数。 WP 需要这些子句来了解哪些位置在调用过程中可能发生了变化,并通过补码来了解哪些位置保持不变。
  • 您对周期字符串给出了一个很好的半正式定义。您应该使用它来定义 ACSL 谓词 periodic(采用与 C 函数 has_period 相同的参数),并根据此谓词编写规范。这将大大简化您的注释。特别是 has_period 不需要 4 个行为:如果 periodic 成立,则必须返回 1,如果 periodic 不成立,它必须返回 0
  • 使用-wp-rte会导致一堆未经证实的义务。根据您的任务,您可能需要加强您的规范,尤其是关于 x 指向的位置的有效性。

关于c - ACSL - 无法证明功能,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/34996324/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com