使用Frama-C验证数组true值计数变更失败的解决方法咨询

使用Frama-C 25.0（搭配Alt-Ergo 2.4.2、CVC4 1.8、Z3 4.8.6）验证数组中true值数量与计数变量一致性时，将数组false值改为true后验证失败，相关代码及验证结果如下：

验证代码 #

#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>

#define SIZE        150

bool table[SIZE] = {true};
int true_counter;
/*@
    logic integer count_true(integer idx) = 
        idx<=0 ? 0 :
            (table[idx-1]==true ? count_true(idx-1) + 1 : count_true(idx-1));
*/

/*@
    requires table[0] == false;
    requires true_counter == count_true(SIZE);
    
    assigns table[0], true_counter;
    
    ensures table[0] == true;
    ensures true_counter == \old(true_counter) + 1;
*/
void ATEST(void) {
    int countBF = 0;
    int countAF = 0;
      
    /*@
      loop invariant 0 <= idx <= SIZE;
      loop invariant 0 <= countBF == count_true(idx) <= idx;
      loop assigns idx, countBF;
      loop variant SIZE - idx;
    */
    for(int idx=0; idx<SIZE; idx++) {
        if(table[idx] == true) countBF += 1;
    }
    //@ assert true_counter == countBF;

    table[0] = true;
    true_counter += 1;
    
    /*@
      loop invariant 0 <= idx <= SIZE;
      loop invariant 0 <= countAF == count_true(idx) <= idx;
      loop assigns idx, countAF;
      loop variant SIZE - idx;
    */
    for(int idx=0; idx<SIZE; idx++) {
        if(table[idx] == true) countAF += 1;
    }
    
    //@ assert true_counter == countAF;
    //@ assert countAF == countBF + 1;
}

验证结果 #

[kernel] Parsing test.c (with preprocessing)
[rte:annot] annotating function ATEST
[wp] 33 goals scheduled
[wp] [Failed] Goal typed_ATEST_assert_2
  Z3 4.8.6: Unknown (Qed:8ms) (cached)
  CVC4 1.8: Timeout (Qed:8ms) (10s) (cached)
  Alt-Ergo 2.4.2: Timeout (Qed:8ms) (10s) (cached)
[wp] [Cache] found:17
[wp] Proved goals:   32 / 33
  Qed:              26  (0.84ms-7ms-24ms)
  Alt-Ergo 2.4.2:    6  (7ms-13ms-27ms) (629) (interrupted: 1) (cached: 7)
  CVC4 1.8:          4  (20ms-28ms-30ms) (11375) (interrupted: 1) (cached: 5)
  Z3 4.8.6:          4  (10ms-20ms) (46252) (unknown: 1) (cached: 5)

解决方法 #

• 替换递归逻辑函数为求和式定义：原递归的count_true深度达150，易导致证明器超时或无法处理。改用Frama-C支持的求和逻辑，更直观且证明器更容易分析：

  /*@ logic integer count_true(bool t[], integer size) = 
        \sum integer i; 0 <= i < size; (t[i] == true) ? 1 : 0;
  */
  

  使用时需调整函数内的引用，比如第一个循环不变式改为countBF == count_true(table, idx)，明确关联当前数组。

• 区分修改前后的数组状态：在修改table[0]后，添加中间断言明确计数变化，利用前置条件table[0] == false推导整体计数增量：

  table[0] = true;
  true_counter += 1;
  //@ assert count_true(table, SIZE) == \old(count_true(table, SIZE)) + 1;
  

  该断言可帮助证明器关联修改前后的计数关系，为后续countAF与countBF的关联提供依据。

• 优化第二个循环的不变式：明确修改后数组的局部状态，告诉证明器仅table[0]发生变化，其余元素与修改前一致：

  /*@
    loop invariant 0 <= idx <= SIZE;
    loop invariant 0 <= countAF == count_true(table, idx) <= idx;
    loop invariant \forall integer i; 0 < i < idx ==> table[i] == \old(table[i]);
    loop assigns idx, countAF;
    loop variant SIZE - idx;
  */
  

  额外的不变式缩小了证明器的推理范围，减少复杂度。

• 简化断言依赖链：将true_counter == countAF的断言拆分为两步，先关联true_counter与修改后的计数，再关联countAF与该计数：

  //@ assert true_counter == count_true(table, SIZE);
  //@ assert countAF == count_true(table, SIZE);
  //@ assert true_counter == countAF;
  

  拆分后的断言更易被证明器逐个验证，避免一次性处理复杂关联。

内容的提问来源于stack exchange，提问作者蔡登瑞