问题标签 [leon]

我想验证以下代码

请帮助我如何使用 Leon 在线系统来验证上述代码

得到以下编译错误

10：可变变量（例如 'var x' 而不是 'val x'）需要 xlang 去糖

14：变异变量需要xlang去糖

9：可变变量（例如 'var x' 而不是 'val x'）需要 xlang 去糖

13：块表达式需要xlang去糖变异变量需要xlang去糖

12：块表达式需要xlang去糖而表达式需要xlang去糖

我曾尝试在 Leon 进行以下程序

结果——成功

结果--失败（未终止）

我是否犯了任何错误，为什么系统无法生产？有人可以指导我吗？

我正在http://leon.epfl.ch/在线使用 Leon 验证系统。我在连接时遇到以下错误：

连接失败：Leon 无法联系到母舰 :( 这通常表明您的防火墙阻止了 websocket 端口上的流量。

连接失败：Leon 服务器现在似乎无法访问。

有什么办法可以自己解决这种问题吗？

我想证明Inox / Welder上集合的一些属性，但我缺乏帮助我弄清楚如何做到这一点的示例。说我想证明：

content(y::xs).contains(x) && x != y ==> content(xs).contains(x)

我定义属性：

但事实证明这个属性不会编译，因为它没有很好地制定（显然错误的部分是 .contains, &&, !==...）

那么，什么是制定财产的正确方法呢？在这里，我假设我有一个内容函数定义为：

关于证明部分，假设我被赋予了以下功能：

这应该从列表 xs 中删除 x 并说我想证明

内容（没有（x，l））==内容（l）--设置（x）

你能给出一个如何做的草图吗？我应该使用诸如SetDifference 之类的 BuiltInNames 吗？

在与 Welder 合作时，我遇到了必须证明的情况：

如果 content(l1) == content(l2) 并且 f 是幂等、关联和交换运算符，则 fold(f,z,l1) = fold(f,z,l2)

在我证明的一个阶段，我想证明对于 x::xs 形式的列表 l1：

折叠(f,z,不带(x,xs)) == 折叠(f,z,不带(x,l2))

where without(x,.) 从列表中删除 x 的出现。因此很明显 without(x,xs) 的大小小于 x::xs 的大小，因此如果 Welder 中允许强归纳，我应该得到相等（内容相等）。

目前，系统只是告诉我没有没有（x，xs）的归纳假设。那么如何对 Welder 进行强感应呢？

inox 文档说明了以下内容

Inox 提供了实用程序类型 TypedADTSort 和 TypedADTConstructor（参见文件 inox/ast/Definitions.scala），它们对应于类型参数已用具体类型实例化的 ADT 定义。可以使用这些来访问参数/字段和带有实例化类型的封闭表达式。

以下对象包含对数学领域建模所需的排序和构造函数。

现在我介绍用于对椭圆曲线的仿射点进行建模的种类和构造。

您可以观察到最后我使用TypedADTSort并TypedADTConstructor使用字段元素作为参数而不是通用参数。我需要这个来讨论仿射点上下文中对字段元素的操作。

编译错误

编译它会给出类型的错误

为什么会这样？有哪些解决方案？

我对字段的加法操作有以下简化定义：

我希望将此操作与中缀表示法一起使用，并且我在 Scala 中找到的当前解决方案在此处给出。所以这就是我在底部包含隐式类的原因。

现在说我想使用这个加法的定义：

这不会编译给出以下错误：

事实上，正在发生的事情是在表达式 x === y+y 中 + 没有被正确应用，因此它是无类型的。我记得在 Welder 证明的对象中无法定义嵌套对象或类，我不知道这是否与它有关。

无论如何，我是否必须忘记在我的 Welder 代码中使用中缀表示法，或者有解决方案？

我想在 Inox 求解器界面中对以下 Scala 层次结构进行建模：

如何建模非零？

如果我将其建模为构造函数

然后我无法指定它有其他构造函数扩展它。而如果我将其建模为一种：

然后我不能指定它是 Element 的子类型。

为什么我需要这个

我需要这个层次结构，因为我需要这样声明属性：

字段的非零元素的集合与非零元素的一、逆和乘积形成一个群。

然后我需要一些机制来生成一个类型来限制一个排序的构造函数，在这种情况下，限制ElementtoOne和的构造函数notZeroOne()。在那种情况下，我将建模：

什么是最干净的解决方案？

我正在证明椭圆曲线上的某些属性，为此我依赖于一些处理现场操作的函数。但是，我不希望 Inox 对这些函数的实现进行推理，而只是假设它们具有某些属性。

比如说我证明点的加法p1 = (x1,y1) and p2 = (x2,y2)是可交换的。为了实现点的加法，我需要一个在其组件（即字段的元素）上实现加法的函数。

添加将具有以下形状：

对于这个函数，我可以声明如下属性：

where^+只是与 add 相对应的中缀运算符，如另一个问题中所示。

插入正文中的正确表达式是什么，以便 Inox 在展开时不会在其上假设任何内容？

在 Welder 中使用 notI 构造时遇到一些问题。以以下为例证明：

我的示例使用关于环结构的常用引理和派生引理 (zeroDivisorLemma)，它表示对于环 a0 = 0 = 0a 中的所有“a”。

我证明如果两个元素不为零，则它们的乘积不为零。如下。

代码可以编译，但 Welder 说：

SMT求解器无法证明属性：false

从假设： (mult(a, b) == zero()) == false。

我会说我没有将正确的函数传递给构造。有人可以解释我应该写什么才能成功吗？是否与类型有关，即 (Theorem, Goal) => Attempt[Witness]？我是否需要提供一个定理来证明目标？

我还能证明什么是假的？我应该使用某种暗示介绍吗？