如何验证证明义务的Why3输出

Question

我相信我可以使用Why3 和不同的证明者生成证明，

1. frama-c -wp -wp-prover cvc4 -wp-rte -wp-out proof swap.c
2. frama-c -wp -wp-prover z3-ce -wp-rte -wp-out proof swap.c
3. frama-c -wp -wp-prover alt-ergo -wp-rte -wp-out proof swap.c

这会生成不同的“为什么”文件。我想通过外部程序验证证明义务。似乎每个证明义务的格式都不同； LispClojure 和 OCaml？格式到底是什么？这些是证据并且足以证明合同/证明是正确的，而不证明 Z3、alt-ergo 等是正确的，这是否正确？

swap.c

对于wp tutorial，

int h = 42;
/*@
  requires \valid(a) && \valid(b);
  assigns *a, *b;
  ensures *a == \old(*b) && *b == \old(*a);
*/
void swap(int* a, int* b)
{
    int tmp = *a;
    *a = *b;
    *b = tmp;
}

int main()
{
    int a = 24;
    int b = 37;

    //@ assert h == 42;

    swap(&a, &b);

    //@ assert a == 37 && b == 24;
    //@ assert h == 42;
    
    return 0;
}

这很好用，frama-c-gui 向我展示了如何开发合同和注释。

Alter-ergo

(* WP Task for Prover Alt-Ergo,2.4.1 *) (* this is the prelude for Alt-Ergo, version >= 2.4.0 *) (* this is a prelude for Alt-Ergo integer arithmetic *) (* this is a prelude for Alt-Ergo real arithmetic *) type string

logic match_bool : bool, 'a, 'a -> 'a

axiom match_bool_True :   (forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z))

为简洁起见，完整的证明被截断。

z3-ce

(* WP Task for Prover Z3,4.8.11,counterexamples *) ;;; generated by SMT-LIB2 driver ;;; SMT-LIB2 driver: bit-vectors, common part ;;; generated by SMT-LIB strings ;;; generated by SMT-LIB strings (set-option :produce-models true) ;;; SMT-LIB2: integer arithmetic ;;; SMT-LIB2: real arithmetic (declare-sort uni 0)

(declare-sort ty 0)

(declare-fun sort (ty uni) Bool)

(declare-fun witness (ty) uni)

为简洁起见，完整的证明被截断。

Answer 1

我不得不承认，我并不完全确定我是否完全理解您想要在这里实现的目标，但这里是您问题的答案：

似乎每个证明义务的格式都不同； Lisp 和 OCaml？具体是什么格式？

这些文件代表提供给您要求 Frama-C 启动的证明者的公式。格式取决于证明者。如果我没记错的话，对于许多证明者来说，这将是 smtlib 或 tptp，但一些证明者（例如 Alt-Ergo）也可以享受自定义输出。文件的生成由 Why3 的​​驱动程序文件描述，如 Why3 manual 的第 12.4 节所述（非常简要地）。

这些是证据对吗？

不，这些是要由为其生成的证明者验证的公式。

并且足以证明合同/证明是正确的而不证明 Z3、alt-ergo 等是正确的？

没有。如果您使用的证明者有错误，他们可能会错误地告诉您给定的证明义务是有效的。一些证明者能够提供证明跟踪（例如，如果您调整驱动程序以使用 smtlib 的 get-proof 命令），但据我所知，这种跟踪的格式是特定于证明者的，因此它可能会很难通过外部工具对其进行检查。