问题标签 [why3]

这感觉像是一个愚蠢的问题，但我很难过。我正在尝试使用 Frama-C Sodium 和 Why3 0.86.1（均通过 OPAM 安装）来证明一些简单的属性。考虑这个程序 ( toy.c)：

我想使用 Frama-C GUI 和 Why3 来证明这个断言。所以我运行frama-c-gui toy.c，选择“Why3 (ide)”作为证明者，然后在主函数上运行“Prove function annotations by WP”。（或者：我导航到“WP 目标”选项卡并从那里运行 Why3 IDE。）出现 Why3，我调用我选择的证明者将所有内容变为绿色，保存会话并退出 Why3，然后在 Frama 中没有任何反应-C GUI：该属性仍标记为橙色/“尝试验证但无法决定”。

我如何告诉 Frama-C 实际使用Why3 生成的证明？证明本身肯定在那里：如果我再次打开Why3，一切仍然是绿色的，所以会话被正确保存。此外，Frama-C 意识到发生了一些事情：当 Why3 IDE 打开时，在 WP 目标选项卡中可以看到一个小齿轮符号，当我关闭 Why3 时它消失了。

（我意识到Alt-Ergo 可以在不涉及Why3 的​​情况下证明这一特殊性质，但我确实需要Why3 来解决更难的问题。）

如何将 Jessie 一个外部插件（为什么是 2.36）与 Frama-c Aluminium 集成？

我正在按照他们的教程尝试Why3 ，但我收到了Unknown logical symbol map.Map.const多个证明者的消息。以下是我试图证明的理论的内容：

以下是各种证明者的结果：

z3：

cvc4:

光伏：

这是我的why3版本信息：

错误消息中提到的 .drv 文件上的时间戳与我的 why3 可执行文件上的时间戳相匹配。

我的理论或我的安装有问题吗？

编辑添加：在教程本身中，它说用来why3 demo_logic.why证明理论，但是当我尝试得到这个结果时：

相反，如果我只是这样做why3 prove demo_logic.why，则结果只是（大约）该理论的回声：

我正在尝试在 Simulink 模型的 Why3 规范中使用 32 位整数，并且我找到了mach.int 库，也就是说，至少在一个地方，它被描述为标准库的一部分。但是，当我尝试将它与以下导入命令一起使用时：

我收到消息：

这是我的第一个带有“。”的库。在其中，所以我不确定我的语法是否错误，或者这个库实际上不是标准库的一部分，或者我做错了什么。

mach.int.Int32使用模块的正确方法是什么？

附加细节

我的why3版本是 0.87.3：

我查看了我的 ~/.why3.conf 文件，发现了以下几行：

我查看/opt/gps/share/why3/modules(and /opt/gps/share/why3/theoriesand /opt/gps/share/spark/theories) 并发现 no mach.int.*，所以我在 中创建了一个mach.int.mlw文件/opt/gps/share/why3/modules，并确保它没why3问题：

结果是一样的。

我的配置文件包括不同证明者的替代条目。当我使用该证明者执行为什么 3 证明时，为什么 3 的输出是一条消息，通知我的配置文件中有多个具有给定名称的证明者，这些证明者的列表。

如果可能的话，我想知道如何在该证明者的特定替代方案上调用Why3。

我在规范中使用该mach.int库（另请参阅此问题），并且我正在尝试定义一个类型为的常量int32：

但是，在分析时，why3 返回消息：

This term has type int, but is expected to have type int32

我注意到Bounded_int（Int32用 type 实例化int32）有以下内容：

但是，我似乎无法使用它来投射1到int32. 例如，如果我使用：

我得到消息unbound symbol 'Int32.of_int'。我已经尝试了很多这样的排列，但都没有成功。谁能提供指导，告诉我为什么我想1成为那种类型的人int32？

我使用 frama-C WP 并想调试我的 ACSL 注释（以了解为什么证明者说我“不知道”）。我有一些绿色或橙色的结果。我打开 why3 IDE 并查看生成的脚本。然后我从列表中选择一个理论/目标并能够启动 Alt-Ergo 或 Coq IDE。我想在 Coq IDE 中使用生成的代码。我看到一些公理，然后是 Theorem WP，然后，例如：

当我在 Coq 中“走到最后”时，我看到一个错误“尝试保存不完整的证明”。如何在 Coq IDE 中获得我在 frama-c 或 why3 结果窗口中看到的结果“已证明”或“未知”？还有什么更好的方法来理解为什么我从证明者那里得到“我不知道”的消息，并确定我的程序是否存在错误或错误的 ACSL 规范？

我有以下引理why3：

这似乎是基本情况的行为，但显然不是。关于为什么这不起作用的任何想法？

更新
我能够将问题减少到一个缺失的引理：

考虑到文档array_eq_sub中指定的定义，这似乎也是微不足道的。为什么我的证明者找不到解决方案？

在其他 ML 变体（例如 SML）中，可以执行以下操作：

但是，使用 Why3ML 声明做类似的事情match会引发语法错误：

如何在元组中正确进行基于值的模式匹配？

如果我尝试：

然后我收到以下错误：

（FromInt.v 之前的所有其他文件似乎编译成功）。即使在通过 opam 卸载并重新安装 why3 和 frama-c 软件包后，此行为仍然存在。

有谁知道如何解决这个问题？

我正在使用 MacOS High Sierra。相关版本信息：Why3 平台，版本 0.88.3，OCaml 顶层，版本 4.05.0，Frama-C Phosphorus-20170501c02v53d5hv2r，和 Coq Proof Assistant，版本 8.7.0（2017 年 12 月），均通过 opam 安装。