问题标签 [why3]

我下载了Why3 tarball 并使用make 安装，并make install-lib按照Why3 API 文档中的说明进行安装。但是当我这样做时open Why3，ocamlc 和 utop 仍然抱怨unbound module Why3。

有人可以帮我如何使用 OCaml 代码中的 Whye API 吗？

我按照这里给出的说明http://why3.lri.fr/doc/install.html。

使用最新版本的 Why3 (1.0.0)，当我尝试执行以下操作时：

我收到以下形式的错误：文件“../something.why”，第 x 行，字符 yz：未绑定符号 'add_one'。难道我做错了什么？我看到的大多数WhyML 代码示例实际上仅使用内置/标准库函数，但确实调用了同一文件中定义的其他谓词。在定义谓词时，是否没有类似的方法来调用我在同一个文件中定义的函数？

使用示例 find.c 文件，我可以使用默认的 alt-ergo 证明它没有问题。但是当更改为 cvc4 时，会收到警告消息和语法错误。这里的代码：

运行此命令并获取以下消息： frama-c -wp -wp-prover CVC4 -wp-out out find.c

如何摆脱警告和语法错误？我的 CVC4 是 1.6 版。

我想用 lambda 验证一个函数。例如：

但是，这会产生错误：

文件“map_reduce.mlw”，第 25 行，字符 4-7：此应用程序使用可变类型数组 int 实例化纯类型变量 'b

是否可以在Why3 中使用 lambda 函数？输入这些 lambda 函数的正确方法是什么？

我正在尝试使用 Frama-c 测试一个函数：

安装完所有要求后：OPAM、why3、alt-ergo 每当我执行frama-c -wp fct.c 时，我都会收到：

在 macOS 上安装 Frama-C (23)、Why3 和 Coq 后，我运行了命令

显示以下消息

• 这是否意味着我不能将 coq 与 Frama-C 一起使用？
• 如何指示 opam 编译上述Why3 库？

问候

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

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

变体

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

z3-ce

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

我想创建一个具有以下先决条件的程序：不变：

变体：

程序结构如下：

程序应该如何看起来像用 frama-c 或why3 编写的？

编辑： 我通过删除乘法并添加加法来修改您的程序。通过这样做，我使用了两个循环。我运行了我的程序，但我收到了警告。这是程序：

这些是警告：

你能解释一下为什么即使我为内部循环指定了不变量和变体，我也会收到那些讨厌的警告吗？