我有我的测试代码（用于研究 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，证明者 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;
}