Leon：如何使用自定义的 `==` 运算符？

Question

在使用leon和rationals的过程中，我遇到了以下问题：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

}

leon 给我的反例是这样的：

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

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

我原以为这段代码会调用我定义的 == 运算符，但由于这个总是 returns true 并且该函数未验证，我倾向于不这么想...

谁能指出这个程序有什么问题或我对 Scala/leon 的理解？谢谢。

Answer 1

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

但有一个简单的解决方法：只需将等式命名为 === 而不是 ==。

Leon：如何使用自定义的 `==` 运算符？

Leon: how to use custom `==` operator?

scala

leon