如何以简洁方式全局指定代码中变量的边界约束？

• 自定义ACSL宏
  把重复的单变量约束打包成宏，单独存到头文件里，所有函数直接引用即可：

  /*@ macro LOG_BLOCK_RANGE(lb) = 0 <= lb < N_LOG_BLOCKS; */
  /*@ macro PAGE_RANGE(lp) = 0 <= lp < N_PAGE; */
  /*@ macro PHY_BLOCK_INDEX_RANGE(idx) = 0 <= idx < N_PHY_BLOCKS; */
  

  函数里引用时会大幅简化：

  /*@
      requires LOG_BLOCK_RANGE(lb) && PAGE_RANGE(lp);
      requires PHY_BLOCK_INDEX_RANGE(h_act_block_index_p) && PAGE_RANGE(h_act_page_p);
      ...
  */
  

  后续要调整边界，只改宏定义就行，不用挨个修改函数的requires块。

• 用ACSL谓词封装复杂组合约束
  针对多变量的组合约束，定义谓词来打包逻辑：

  /*@ predicate ValidPhysicalBlock(int idx) = 
        0 <= idx < N_PHY_BLOCKS && 0 <= index_2_physical[idx] < N_PHY_BLOCKS; */
  /*@ predicate ValidCleanCounters() = 
        1 <= h_clean_counter + l_clean_counter <= N_PHY_BLOCKS && 
        l_clean_counter == low_array_counter && 
        h_clean_counter == high_array_counter; */
  

  函数里直接调用谓词，代码更简洁清晰：

  /*@
      requires ValidPhysicalBlock(h_act_block_index_p);
      requires ValidCleanCounters();
      ...
  */
  

• 全局不变式处理全程生效的约束
  如果有些约束是程序运行全程必须满足的（比如index_2_physical数组所有元素始终合法），直接声明全局不变式，不用每个函数都重复写：

  /*@ global invariant \forall integer i; 0 <= i < N_PHY_BLOCKS ==> ValidPhysicalBlock(i); */
  

  注意要确认你使用的静态分析工具（比如Frama-C）支持全局不变式的验证。

• 从C类型层面减少重复约束
  对非负变量直接用unsigned类型，固定小范围的变量用uint8_t/uint16_t这类精确宽度类型，从根源上减少“0 <= x”这类重复约束的写法。

内容的提问来源于stack exchange，提问作者Yu-Fang Chen