问题标签 [key-formal-verification]

有哪些代码示例可以展示KeyY的强大功能？

细节

有这么多可用的形式方法工具，我想知道 KeyY 在哪里比它的竞争对手更好，以及如何？一些可读的代码示例对比较和理解很有帮助。

更新

在 Key 网站上搜索，我找到了书中的代码示例——那里有合适的代码示例吗？

此外，我在 TimSort 中找到了一篇关于 Key 在 Java 8 的 mergeCollapse 中发现的错误的论文。什么是 TimSort 中展示 KeyY 实力的最小代码？然而，我不明白为什么模型检查不能找到错误——一个包含 64 个元素的位数组不应该太大而无法处理。其他演绎验证工具是否同样能够找到错误？

是否存在具有合适代码示例的既定验证竞赛？

我正在使用 Key ( https://www.key-project.org ) 进行教学项目。

一方面，我很高兴 Key 很容易证明以下带 jml 注释的 java 代码的正确性

但另一方面，令人惊讶的是，我无法证明以下等效程序的正确性

有人知道我是否遗漏了什么吗？

目前，我正在尝试使用 Java 程序的Key工具进行一些形式验证。

这是我的带注释的 Java 代码：

令我惊讶的是 Key，它无法证明当前程序根据其规范是有效的。Key在目标 54 失败。当前目标窗口显示：

我不太明白：未能证明规范的主要原因是什么？

以下是 Key Dynamic Logic 问题文件 (.key) 的条目。当我使用 Key theorem proover 运行时，该文件得到了证明。为什么这个Key动态逻辑问题得到证明，肯定将2147483647的java int增加1应该是-2147483648？

我很想更好地理解 Java 密钥证明的限制。我想出了一个特定的数组元素将触发空指针异常的场景。当我通过证明程序运行它时，它通过了。知道这是为什么吗？它应该会失败，因为将在数组元素 86454 处抛出空指针。请注意“normal_behaviour”意味着它应该无异常终止。

有什么方法可以禁用 Z3（版本 4.8.8）中断言的简化/重写？

我目前正在 KeyY ( https://www.key-project.org ) 中对 Z3 证明进行证明重放。但是，为了能够重放 Z3 的“断言”规则，我需要在 Z3 的 SMT-LIB 输入中指定的确切断言，而不是它的简化版本。

作为可能发生的情况的一个极端示例，请考虑以下 SMT-LIB 输入：

运行 Z3 4.8.8 会导致以下输出：

显然，断言已被简化，这使得证明没有真正的帮助。有没有办法完全禁用这种简化（从而从 Z3 获得“真实”证明，我可以在我们的工具中重播）？

我有这门课。当我使用 getBar() 的合同时，我可以证明 pass(int i) 方法，而不是没有它。除了 getBar() 的合约也被证明。为什么我不能通过内联证明通过？我尝试了 Key 2.8 和 Key 2.7。

我正在开发一个使用 Java 密钥进行形式验证的项目。我正在为此使用 Eclipse 插件。当我拥有 Xtext 2.10 版时，一切正常。但由于某些原因，我不想更新到 Xtext 2.25。不幸的是，我现在收到以下错误：

当我寻找解决方案时，我发现其他人偶然发现了类似的问题，但使用了不同的库。解决方案是简单地更新库。来自密钥的 Eclipse 更新站点已损坏，因此我无法更新我的项目。我当前的 Key-Eclipse 版本是 1.0.0

我是 KeyY 的新手，我正在尝试设置所有内容，以便我可以开始验证程序。为此，我需要启用 SMT Solver: Z3。我下载了Z3文件，但是在KeyY中Z3设置的命令行中填写目录路径时，得到错误“null”（见截图）。我为我的 Z3.exe 文件尝试了许多不同的位置，但仍然出现相同的错误。我通过转到文件->右键单击->按选项键（macbook）->复制路径来获得目录路径。

有没有人知道我做错了什么？

提前致谢！

错误截图 （为隐私起见已删除名称）