0

在与 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

}

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

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并不总是满足构造函数的要求。）

我错过了什么吗？

4

1 回答 1

2

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

问题 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的 s。Leon 必须在 ADT 上综合遍历函数，以便注入这些先决条件。

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

问题 2

虽然编写以下函数是可行的：

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

你有一个先有鸡还是先有蛋的问题，invariant将在其中注入前提条件invariant检查this。

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

于 2015-05-26T12:09:33.297 回答