CODEWITHSUNDEEP
scalaleon
Hiura
Hiura

Reputation: 3530

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

While working on rational numbers with leon, I have to add as requirement isRational pretty much everywhere.

For example:

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

}

Is it possible to add a require statement in a class constructor to DRY this code so that it applies to all instances of the data structure? I tried adding it on the first line of the class body but it seems to have no effect...

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
}

This does not prevent leon from creating a Rational(0, 0) for example as the report suggest:

[  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 and other don't always meet the constructor requirement.)

Am I missing something?

Upvotes: 0

Views: 60

Answers (1)

Etienne Kneuss
Etienne Kneuss

Reputation: 108

The main difficulty with invariants can be decomposed in two problems:

Problem 1

Given

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

Leon would have to inject this requirement in preconditions of all functions taking A as argument, so

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

will need to become:

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

While trivial for this case, consider the following functions:

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

or

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

Here it is not so easy to constraint foo2 so that the list contains only valid As. Leon would have to synthesize traversal functions on ADTs so that these preconditions can be injected.

Moreover, it is impossible to specify that the Set[A] contains only valid As as Leon lacks capabilities to traverse&constraint the set.

Problem 2

While it would be practical to write the following function:

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

You have a chicken-and-egg issue, where invariant would be injected with a precondition checking invariant on this.

I believe both problems can be solved (or we can restrict the usage of these invariants), but they constitute the reasons why class invariants have you been trivially implemented yet.

Upvotes: 2

Related Questions