leon

1热度

1回答

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

0热度

1回答

的INOX文档指出以下 Inox公司提供的实用程序类型TypedADTSort和TypedADTConstructor （见文件INOX/AST/Definitions.scala）对应于ADT 定义其类型参数具有已经用具体的类型来实例化。可以使用这些来访问参数/字段，并用实例化的类型包含表达式。以下对象包含建模数学字段所需的排序和构造函数。 import inox._ import ino

0热度

1回答

在焊机

定义管道符我曾经在一个领域中的加法运算以下简单求定义：要与中间符号和当前的解决方案，我觉得做使用 import inox._ import inox.trees.{forall => _, _} import inox.trees.dsl._ object Field { val element = FreshIdentifier("element") val ze

0热度

1回答

建模Inox公司

类层次我想在Inox公司解算器界面下面的斯卡拉层次结构模型： abstract class Element() abstract class nonZero() extends Element final case class Zero() extends Element final case class One() extends nonZero() final case class n

1热度

1回答

引入终止在莱昂/一个前提不锈钢

我是根据以下功能无类型演算的评价试图证明： def eval(t: Term): Option[Term] = t match { case App(t1, t2) => eval(t1) match { case Some(Abs(x, body)) => eval(t2) match { case Some(v2) => eval(subst(x, v2, b

0热度

1回答

如何在Inox中声明抽象函数

我证明了椭圆曲线上的某些属性，并且我依赖于一些处理字段操作的函数。但是，我不希望Inox推断这些函数的实现，而只是假设它们具有某些属性。举例来说，我证明点p1 = (x1,y1) and p2 = (x2,y2)的添加是可交换的。为了实现点的添加，我需要一个在其组件（即字段的元素）上实现加法的函数。加入将具有以下形状： val addFunction = mkFunDef(addID)() {

0热度

1回答

在焊机中使用notI。示例矛盾证明

在焊机中使用notI构造时存在一些问题。以下列为例证：我的例子使用了有关环的结构和导出的引理（zeroDivisorLemma）的一般引理，它说环a0 = 0 = 0a中的所有'a'。我证明如果两个元素不为零，他们的产品不是零。如下。 val theorem: Theorem = forallI("a"::F,"b"::F){ case (a,b) => implI(and

1热度

1回答

证明有序列表的串联是在不锈钢

有序列表我有一个排序，我想在不锈钢（以前称为莱昂），以验证阵列下面的代码： import stainless.lang._ import stainless.collection._ object QuickSort { def isSorted(list: List[BigInt]): Boolean = list match { case Cons(x, xs @

1热度

1回答

是否有可能根据规范进行推理而不是实施？

我想使用Leon在事先不知道具体实现的情况下验证规范。例如，假设我有一个排序的功能，还有一个什么样的排序列表看起来像定义： def sort (list: List[BigInt]): List[BigInt] = { ... } ensuring { res => res.content == list.content && isSorted(res) }

0热度

1回答

匹配错误，同时证明终止功能在不锈钢

我有这个代码证明在不锈钢/莱昂排序算法的终止。请注意，所采用的排名功能或措施并不是正确的，因为这来自作业集。 import stainless.lang._ import stainless.collection._ object QuickSort { def isSorted(list: List[BigInt]): Boolean = list match {