c - 如何知道 ACSL 谓词的哪些部分失败了？

Question

我有一个约 37 行长的 ACSL 谓词(谓词返回传递的结构是否处于有效状态)。 它是一系列 && 组合在一起的条件。

当我断言谓词时:

//@ assert MyPredicate(myArg);

并且验证失败，我不知道是哪个&&的条件失败了。

我如何知道谓词的哪些部分失败了？

当验证失败时，我用frama-c-gui -wp -wp-rte myfile.c打开C文件。我更经常使用相同的参数运行 frama-c，但我使用 GUI 来帮助调查故障。

$ frama-c-gui --version
24.0 (Chromium)

如果谓词永远不会改变，我可能会手动将它分解成单独的 /*@assert ... */ 部分，但我会在工作时定期更新谓词在程序上，并且不希望使谓词和断言 block 保持同步。

如果证明者版本是相关的:

$ why3 config detect
Found prover Alt-Ergo version 2.4.1, OK.
Found prover Z3 version 4.8.9 (alternative: counterexamples)
Found prover Z3 version 4.8.9, OK.
Found prover Z3 version 4.8.9 (alternative: noBV)
4 prover(s) added

Answer 1

证明谓词的方法有很多种，有时，问题不是不能证明谓词的子部分。例如，这解释了为什么您有时可以证明谓词而无法证明连词的单独元素。例如，如果您有以下内容:

/*@
  predicate P(integer a) = R(a) && Q(a) && ...
  lemma l{L1, L2}: \forall a ; P{L1}(a) ==> Z{L1, L2}(a) ==> P{L2}(a) ;
*/

//@ requires P(a);
void foo(int a){
  ...
  //@ assert Z{Pre,Here}(a);
  //@ assert P(a);
}

由于引理，P(a) 的证明是直接的。证明 P(a) 的单独元素至少需要展开定义(如果您要执行多个级别的展开，这可能会失败)。 SMT 求解器并不都擅长展开定义。根据我的经验，CVC4 在这场比赛中比 Alt-Ergo 和 Z3 好一点，但无论 SMT 解算器如何，总会有一个深度，没有 SMT 解算器会继续展开定义。

在这种情况下，使用引理函数可以帮助提取您感兴趣的谓词部分。例如:

/*@ ghost
  /@ requires P(a);
     assigns \nothing ;
     ensures R(a);
  @/
  void lemma_P_means_R(int a){}
*/

一旦你有了这个函数，你就可以在任何需要从 P 中提取 R 的地方使用它。

现在，假设您需要找到在证明过程中失败的谓词子部分。在识别谓词的哪一部分无法证明的过程中，我会使用嵌入在 WP GUI 中的交互式定理证明器。让我们以下面的代码片段为例:

/*@ axiomatic Ax {
      predicate A ;
      predicate B ;
    }
    predicate AB = A && B ;
*/

int main(void){
  //@ assert AB ;
}

一旦断言失败，可以在GUI中选择目标，然后应用定义策略展开目标:

然后，您可以拆分结果目标:

这将导致两个不同的子目标来证明:

同样，一旦您知道哪一部分难以证明以及如何证明它们，添加正确的断言和引理函数调用可能有助于证明。否则，您还可以保存生成的证明脚本以便稍后重播。 (命令行证明的名字是script)。