0

我相信我可以使用带有不同证明者的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

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

交换文件

对于wp 教程，

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)

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

4

1 回答 1

1

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

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

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

这些是证据对吗？

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

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

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

于 2021-08-24T12:25:18.280 回答