是否有可能对 Leon 中的数据结构有要求？

Question

在与 leon 一起处理有理数时，我必须按要求添加 isRational 几乎所有地方。

例如：

import leon.lang._

case class Rational (n: BigInt, d: BigInt) {

  def +(that: Rational): Rational = {
    require(isRational && that.isRational)
    Rational(n * that.d + that.n * d, d * that.d)
  } ensuring { _.isRational }

  def *(that: Rational): Rational = {
    require(isRational && that.isRational)
    Rational(n * that.n, d * that.d)
  } ensuring { _.isRational }

  // ...

  def isRational = !(d == 0)
  def nonZero = n != 0

}

是否可以在 class 构造函数中添加 require 语句来 DRY 这段代码，以便它适用于数据结构的所有实例？我尝试将它添加到 class 正文的第一行，但它似乎没有效果...

case class Rational (n: BigInt, d: BigInt) {
    require(isRational) // NEW

    // ... as before ...

    def lemma(other: Rational): Rational = {
        Rational(n * other.d + other.n * d, d * other.d)
    }.ensuring{_.isRational}

    def lemmb(other: Rational): Boolean = {
        require(other.d * other.n >= 0)
        this <= (other + this)
    }.holds
}

这不会阻止 leon 创建 Rational(0, 0) 例如，如报告所示：

[  Info  ]  - Now considering 'postcondition' VC for Rational$$plus @9:16...
[  Info  ]  => VALID
[  Info  ]  - Now considering 'postcondition' VC for Rational$$times @14:16...
[  Info  ]  => VALID
[  Info  ]  - Now considering 'postcondition' VC for Rational$lemma @58:14...
[ Error  ]  => INVALID
[ Error  ] Found counter-example:
[ Error  ]   $this -> Rational(1, 0)
[ Error  ]   other -> Rational(1888, -1)
[  Info  ]  - Now considering 'postcondition' VC for Rational$lemmb @60:41...
[ Error  ]  => INVALID
[ Error  ] Found counter-example:
[ Error  ]   $this -> Rational(-974, 0)
[ Error  ]   other -> Rational(-5904, -1)
[  Info  ]  - Now considering 'precond. (call $this.<=((other + $this)))' VC for Rational$lemmb @62:5...
[ Error  ]  => INVALID
[ Error  ] Found counter-example:
[ Error  ]   $this -> Rational(-1, 0)
[ Error  ]   other -> Rational(0, -1)
[  Info  ]  - Now considering 'precond. (call other + $this)' VC for Rational$lemmb @62:14...
[ Error  ]  => INVALID
[ Error  ] Found counter-example:
[ Error  ]   $this -> Rational(1, 2)
[ Error  ]   other -> Rational(7719, 0)
[  Info  ]   ┌──────────────────────┐
[  Info  ] ╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └──────────────────────┘                                                                   ║
[  Info  ] ║ Rational$$plus     postcondition                      9:16   valid     U:smt-z3      0.010 ║
[  Info  ] ║ Rational$$times    postcondition                      14:16  valid     U:smt-z3      0.012 ║
[  Info  ] ║ Rational$lemma     postcondition                      58:14  invalid   U:smt-z3      0.011 ║
[  Info  ] ║ Rational$lemmb     postcondition                      60:41  invalid   U:smt-z3      0.018 ║
[  Info  ] ║ Rational$lemmb     precond. (call $this.<=((ot...     62:5   invalid   U:smt-z3      0.015 ║
[  Info  ] ║ Rational$lemmb     precond. (call other + $this)      62:14  invalid   U:smt-z3      0.011 ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 6      valid: 2      invalid: 4      unknown 0                                0.077 ║
[  Info  ] ╚════════════════════════════════════════════════════════════════════════════════════════════╝

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

我是不是漏掉了什么？

Answer 1

不变量的主要困难可以分解为两个问题：

问题 1

给定

case class A(v: BigInt) {
  require(v > 0)
}

Leon 必须在所有以 A 作为参数的函数的前提条件中注入此要求，因此

def foo(a: A) = { 
  a.v
} ensuring { _ > 0 }

需要变成：

def foo(a: A) = { 
  require(a.v > 0)
  a.v
} ensuring { _ > 0 }

虽然对于这种情况来说微不足道，但请考虑以下功能：

def foo2(as: List[A]) = { 
  require(as.nonEmpty)
  a.head.v
} ensuring { _ > 0 }

或

def foo3(as: Set[A], a: A) = { 
  as contains a
} ensuring { _ > 0 }

这里要约束 foo2 使列表只包含有效的 A 并不容易。 Leon 必须在 ADT 上合成遍历函数，以便可以注入这些先决条件。

此外，无法指定 Set[A] 仅包含有效的 A，因为 Leon 缺乏遍历和约束集合的能力。

问题 2

虽然编写以下函数会很实用：

case class A(a: BigInt) {
  require(invariant)
  def invariant: Boolean = // ...
}

您遇到了先有鸡还是先有蛋的问题，其中 invariant 将在 this.

上注入先决条件检查 invariant

我相信这两个问题都可以解决（或者我们可以限制这些不变量的使用），但它们构成了 class 个不变量被你简单实现的原因。

是否有可能对 Leon 中的数据结构有要求？

Is it possible to have requirement on data structure in Leon?

scala

leon

问题 1

问题 2