如何验证 Proof Obligations 的 Why3 输出

Question

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

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

这会生成不同的 'why' 文件。我想用外部程序验证证明义务。似乎每项证明义务的格式都不同； ~~Lisp~~Clojure 和 OCaml？格式到底是什么？这些是证据并且足以证明 contract/proof 是正确的而不证明 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 向我展示了如何开发契约和注释。

另类

(* 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

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

It seems each proof obligation is in a different format; Lisp and OCaml? What exactly is the format?

这些文件代表提供给您要求 Frama-C 启动的证明者的公式。格式取决于证明者。如果我没记错的话，对于许多证明者来说，这将是 smtlib, or tptp, but some provers such as Alt-Ergo can also enjoy a custom output. The generation of the file is described by Why3's driver files, as mentioned (quite briefly) in section 12.4 of the Why3 manual.

Is it correct that these are proof ?

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

and are sufficient to show the contract/proof is correct without proving that Z3, alt-ergo, etc are correct?

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

如何验证 Proof Obligations 的 Why3 输出

How to verify Why3 output of Proof Obligations

frama-c

why3

swap.c

另类

z3-ce