-1

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

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 <=(that: Rational): Boolean = {
    require(isRational && that.isRational)
    if (that.d * d > 0)
      n * that.d <= d * that.n
    else
      n * that.d >= d * that.n
  }

  def ==(that: Rational): Boolean = {
    require(isRational && that.isRational)
    //that <= this && this <= that
    true // for testing purpose of course!
  }

  // fails to verify
  def inverse1: Rational = {
    require(isRational && nonZero)
    Rational(d, n)
  }.ensuring { res => res.isRational && res.nonZero && res * this == Rational(1, 1) }

  // verifies
  def inverse2: Rational = {
    require(isRational && nonZero)
    Rational(d, n)
  }.ensuring { res => res.isRational && res.nonZero /*&& res * this == Rational(1, 1)*/ }

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

}

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

[  Info  ]  - Now considering 'postcondition' VC for Rational$inverse1 @33:16...
[ Error  ]  => INVALID
[ Error  ] Found counter-example:
[ Error  ]   $this -> Rational(-2, -2)

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

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

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

4

1 回答 1

3

恐怕这是不可能的。正如您在源代码中看到的here和here== ， Leon没有将其视为普通的方法调用，而是变成了一个特殊的AST节点，称为Equals.

但是有一个简单的解决方法：只需调用你的相等===而不是==.

于 2015-05-25T16:53:02.837 回答