c - 如何在frama-c wp中用计算证明迭代循环？

Question

我有我的测试代码（研究WP循环不变量），它将两个长整数与数组单元格中每个数字的表示相加：

int main(int argc, const char * argv[]) {

char a[32], b[32];//size can be very big
memset(a, 0, sizeof(a));
memset(b, 0, sizeof(b));
scanf("%s %s", a, b);
unsigned int size1 = strlen(a);
unsigned int size2 = strlen(b);
//code to reverse a string. currently proved 
reverse(a, size1);
reverse(b, size2);
for (unsigned int i = 0; i < size1; i++) a[i]-='0'; //move from chars to integers
for (unsigned int j = 0; j < size2; j++) b[j]-='0';
unsigned int maxsize = size1;
if (size2 > maxsize) maxsize = size2;
int over = 0;
//actual computation code

/*@
loop invariant maxsize == \max(size1, size2);
loop invariant bound: 0 <= k <= maxsize;
loop invariant ov: \forall integer i; 0 < i < k ==> \at(a[i], Here) == (\at(a[i], Pre) + b[i]+ Over((char *)a, (char *)b, i)) % 10;
loop assigns k, a[0..maxsize-1],over;
loop variant maxsize - k;
*/
for (unsigned int k = 0; k < maxsize; k++)
{
    char sum=a[k] + b[k] + over; 
    //over=overflow is for 9+9 = 18, result=8, over=1
    a[k] = sum % 10;
    over = sum / 10;
}
if (over != 0) a[maxsize++] = over;
//...
return 0;
}

我只想指定最后一个循环不变量我已经用\ at（a[I]，LoopCurrent）尝试了一些ACSL代码我收到未知状态或超时最后，我完成了一个公理化的递归解决方案，没有任何成功。
我现在不知道我还应该验证什么帮忙？
更新：
为实际计算创建了一个函数改进的公理。仍处于超时状态。使用opam的Frama-C最新版本运行，默认设置为（超时=10，prover Alt Ergo）。

/*@
@predicate
Unchanged{K,L}(char* a, integer first, integer last) = \forall integer i; first <= i < last ==> \at(a[i],K) == \at(a[i],L);

axiomatic ReminderAxiomatic
{
logic integer Reminder {l} (integer x, integer y);
axiom ReminderEmpty: \forall integer x, integer y; x < y ==> Reminder(x, y) == x;
axiom ReminderNext: \forall integer x, integer y; x>=y ==> Reminder(x, y) == Reminder(x-y, y)+0; 
}

axiomatic DivAxiomatic
{
logic integer Div {l} (integer x, integer y);
axiom DivEmpty: \forall integer x, integer y; x < y ==> Div(x, y) == 0 ;
axiom DivNext: \forall integer x, integer y; x >= y ==> Div(x, y) == Div(x - y, y) + 1 ;
}

axiomatic OverAxiomatic
{
logic integer Over {L}(char *a, char * b, integer step) reads a[0..step-1], b[0..step-1];
axiom OverEmpty: \forall char *a, char * b, integer step; step <= 0 ==> Over(a, b, step) == 0;
axiom OverNext: \forall char *a, char * b, integer step; step > 0 && a[step-1]<10 && a[step-1]>=0 && b[step-1]<10 && b[step-1]>=0
==> Over(a, b, step) ==  Div((int) a[step-1]+(int)b[step-1]+(int)Over(a,b,step-1), 10);
}
*/
/*@
requires 0 <= maxsize < 10;
requires \valid (a+(0..maxsize-1));
requires \valid (b+(0..maxsize-1));
requires \valid (res+(0..maxsize));
requires \forall integer i; 0 <= i < maxsize ==> 0 <= (int)a[i] < 10;
requires \forall integer i; 0 <= i < maxsize ==> 0 <= (int)b[i] < 10;
*/
void summ(char *a, char *b, char *res, unsigned int maxsize) {

char over = 0;

/*@
loop invariant bound: 0 <= k <=maxsize;
loop invariant step: \forall integer i; 0 <= i < k ==> res[i] == (char) Reminder((int)a[i]+ (int)b[i]+ (int)Over((char *)a, (char *)b, i) , 10);
loop invariant unch: Unchanged{Here,LoopEntry}((char *)res, k, maxsize);
loop assigns k, over, res[0..maxsize-1];
loop variant maxsize-k;
*/
for (unsigned int k = 0; k < maxsize; k++)
{
 char sum = a[k] + b[k] + over;
 res[k] = sum % 10;
 over = sum / 10;
}

//
if (over != 0) res[maxsize++] = over;

}

Answer 1

首先，如果您的问题包含一个MCVE，在本例中包括您当前正在处理的C函数（而不仅仅是它的主体）和您编写的ACSL注释，它们在代码中的确切位置会更好。用于启动Frama-C的命令行也不会受到影响，同时也不会影响您遇到问题的注释列表。
除此之外，这里还有一些可能与您的问题有关的事情（同样，如果没有准确的描述，很难确定）。
loop assigns是错误的：您在循环中分配了over，但这里没有提到它。
我不确定WP是否支持\max。
模除法和整数除法是自动校准器经常遇到的两种运算您可能需要一些额外的断言和/或公理来帮助它们。
你的loop invariant没有提到a[i]的值由于k <= i< maxsize表示loop assigns的所有细胞都可能已被修改，您必须添加一个不变量，告诉具有更高索引的细胞到目前为止尚未被触摸。
我不完全确定您使用的a：\at(a[i],Pre)表示当前函数的开始因此，如果Pre和scanf与循环处于相同的函数中（同样，MCVE会澄清这一点），则这不是真的您可能想谈论reverse来引用第一次进入循环的状态下的单元格值。
更新
恐怕WP无法完全证明您的注释，但我设法获得了一个版本，其中只有一个\at(a[i],Loop_entry)，基本上是lemma函数的reads子句的扩展版本未经验证（我相信在WP的实际C内存表示下无法证明）请注意，这意味着要玩WP的提示功能下面提供了代码和脚本，但我将从评论您的原始版本开始：
不需要Over和Div如果有什么问题，他们会把证明人弄糊涂的。你可以坚持使用Reminder和xxx/10实际上，我对除法和模的评论有点过于谨慎。在目前的情况下，在这个水平上一切似乎都很好。
类似地，xxx%10可以是内联的，但是保持这种方式应该不会有什么坏处。
我使用了Unchanged而不是unsigned char，因为它避免了由于整数提升而产生的一些虚假转换，并且删除了逻辑中的任何转换通常，您不必在ACSL注释中引入这种类型转换，除非可能是为了指示某些计算保持在适当的范围内（如char）。这样的强制转换被转换为证明义务中的函数调用，而且它可能再次混淆证明者。
缺少一个不变量，表示\let x = y + z; x == (int) x;确实包含上一步的潜在进位（同样，缺少不变量的一个好提示是over中提到的位置不会出现在任何loop assigns中）。
最后，还有一个小的微妙之处：如果您不以某种方式指出loop invariant只能是over或0，则没有任何东西可以阻止加法溢出1（这使得无法证明具有unsigned char的C计算及其具有无限整数的ACSL对应项给出相同的结果）。由于unsigned char函数的递归性质，这可以通过所谓的引理函数来建立，在引理函数中，数学归纳是通过一个带有适当不变量的简单for循环来实现的
此外，我还作为不变量明确地添加了Over和a保持不变这通常是由b暗示的，但是有了这些明确的假设，在脚本中就更容易了。
总而言之，这里是最后的代码：

/*@
axiomatic Carry {
 logic integer Over {L}(unsigned char* a, unsigned char* b, integer step)
 reads a[0 .. step - 1], b[0 .. step - 1];

 axiom null_step: \forall unsigned char* a, *b, integer step;
                  step <= 0 ==> Over(a,b,step) == 0;
 axiom prev_step: \forall unsigned char* a, *b, integer step;
                  step > 0 ==>
                  Over(a,b,step) ==
                  (a[step-1] + b[step - 1] + Over(a,b,step-1)) / 10;

lemma OverFootPrint{L1,L2}:
\forall unsigned char* a, unsigned char*b, integer step;
(\forall integer i; 0<=i<step ==> \at(a[i],L1) == \at(a[i],L2)) &&
(\forall integer i; 0<=i<step ==> \at(b[i],L1) == \at(b[i],L2)) ==>
Over{L1}(a,b,step) == Over{L2}(a,b,step);
}
*/

/*@
  requires \valid(a+(0 .. step-1));
  requires \valid(b+(0 .. step - 1));
  requires \forall integer i; 0<=i<step ==> 0<=a[i]<10 && 0<=b[i]<10;
  assigns \nothing;
  ensures 0<= Over(a,b,step) <= 1;
*/
void lemma_function(unsigned char* a, unsigned char* b, unsigned int step) {
  /*@
      loop invariant 0<=i<=step;
      loop invariant \forall integer k; 0<=k<=i ==> 0 <= Over(a, b, k) <= 1;
      loop assigns i;
  */
  for (int i = 0; i < step; i++);
}

/*@
requires 0 <= maxsize < 10;
requires \valid (a+(0..maxsize-1));
requires \valid (b+(0..maxsize-1));
requires \valid (res+(0..maxsize));
requires \separated (a+(0..maxsize-1),res+(0..maxsize));
requires \separated (b+(0..maxsize-1),res+(0..maxsize));
requires \forall integer i; 0 <= i < maxsize ==> 0 <= a[i] < 10;
requires \forall integer i; 0 <= i < maxsize ==> 0 <= b[i] < 10;
*/
void summ(unsigned char* a, unsigned char*b, unsigned char* res,
          unsigned int maxsize) {

unsigned char over = 0;

/*@
loop invariant bound: 0 <= k <=maxsize;
loop invariant step: \forall integer i; 0 <= i < k ==> res[i] == (a[i]+ b[i]+ Over(a,b,i)) % 10;
loop invariant over: over == Over(a,b,k);
loop invariant a_unchanged: \forall integer i; 0 <= i < maxsize ==>
\at(a[i],LoopEntry) == a[i];
loop invariant b_unchanged: \forall integer i; 0 <= i < maxsize ==>
\at(b[i],LoopEntry) == b[i];
loop invariant unch: \forall integer i; k<=i<=maxsize ==> \at(res[i],LoopEntry) == res[i];
loop assigns k, over, res[0..maxsize-1];
loop variant maxsize-k;
*/
for (unsigned int k = 0; k < maxsize; k++)
{
 unsigned char sum = a[k] + b[k] + over;
 res[k] = sum % 10;
 over = sum / 10;
 lemma_function(a,b,k);
}

//
if (over != 0) res[maxsize++] = over;

}

这两个提示脚本可用 here要使用它们，请将它们放在代码旁边的目录 loop assigns中（例如 scripts/typed），然后使用以下命令行：

frama-c[-gui] -wp -wp-prover alt-ergo,script -wp-session scripts file.c

如果您愿意，可以更改 file.c目录的名称（它必须与 scripts的参数匹配），但是 -wp-session和脚本的文件名必须与给定的一样，因为WP将使用它们来检测它们应该证明的证明义务。在GUI模式下，您可以查看脚本，但可能很难理解和解释每个步骤不符合SO的答案。