问题标签 [leon]

我试图证明列表中的大小（元素数量）是非负的，但 Leon 未能证明这一点——它只是超时了。Leon 真的无法证明这个属性，还是我用错了？我的出发点是我在“Leon 验证系统概述”一文中读到的一个函数。

我尝试按照说明从 github 上的 README.md 文件为 MacOSX (yosemite) 构建 leon。

它运行良好，除了当我运行基本测试时，我遇到了一个找不到 scalaz3 库的问题：

我尝试从 EPFL 构建 ScalaZ3 包，这需要构建 Microsoft 的 Z3（来自 github）。构建 z3 本身可以找到，但构建 ScalaZ3 失败，缺少“gomp”库：

我发现这里有一个适用于 MacOSX 的 Clang OMP 库：

http://brewformulas.org

但是，这可能需要调整一些构建脚本以指向 brew 安装的 clang-omp。

有没有人遇到过或解决过类似的问题？

• 尼古拉斯。

我正在尝试直接使用 scalac 编译我的 Leon 代码。不幸的是，我无法正确构建代码所依赖的 Leon 库。

例如，我跑了

但这实际上会返回错误：

应该将什么传递给 scalac 以避免库中的这些错误并最终编译我自己的源文件？

谢谢！

在 Leon 验证器中，即使在 Leon 中进行归纳推理，为什么会有不同的选项使用相同的求解器？例如。所有 3 个选项：fairz3、smt-z3 和 unrollz3 似乎都使用 z3 求解器并在 leon 中执行归纳推理。

在使用 leon 和有理数时，我遇到了以下问题：inverse1函数的验证给出了一个反例，但它没有多大意义，而inverse2验证。

莱昂给我的反例是这样的：

但从数学上讲，这没有任何意义。

我期待这段代码调用==我定义的运算符，但由于这个总是返回true并且函数没有验证，我倾向于不这样认为......

有人可以指出这个程序有什么问题或我对 Scala/leon 的理解吗？谢谢。

在与 leon 一起研究有理数时，我几乎必须在isRational任何地方添加作为要求。

例如：

是否可以在类构造函数中添加一条require语句来干燥此代码，以便它适用于数据结构的所有实例？我尝试将它添加到类主体的第一行，但似乎没有效果......

正如报告所建议的那样，这并不妨碍 leon 创建一个Rational(0, 0)示例：

（this并且other并不总是满足构造函数的要求。）

我错过了什么吗？

考虑以下否定布尔值的复杂方法（取决于短路评估）：

如果我在 Scala 控制台中测试此代码，它会按预期工作。但是leon --xlang说后置条件无效。这是预期/指定的吗？

我对 Leon 的 PropositionalLogic 示例中的 wrongCommutative 的属性非常好奇。

这对我来说似乎是一个正确的属性，我不明白为什么它只是在莱昂超时。

这是链接： https://leon.epfl.ch#link/37040293ff5ff92c763f797f22f142f8-1

谁能帮我这个？

我想在事先不知道具体实现的情况下使用 Leon 来验证规范。例如，假设我有一个排序函数，以及排序列表的定义：

理想情况下，我应该能够证明引理，例如sort(sort(list)) == sort(list)基于sort 单独的后置条件。否则，我不能声称适用于插入排序的 Leon 证明也适用于快速排序（实际上很少这样做）。Leon 是否有可能在不研究实现的情况下根据前置条件和后置条件进行推理？

谢谢！

我有一个抽象的堆栈类型如下

我想验证pop返回最后推送的元素：

这两个引理是等价的，但 Leon 无法识别第二个引理中的类型参数。Stack有趣的是，Leon 在具体或非泛型时都没有问题 （请参阅下面的链接以获取示例）。这是 Leon 的功能还是只是一个错误？

完整的示例代码可以在这里找到。