Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Counterexample does not violate precondition of lambda passed to HOF #109

Open
samuelgruetter opened this issue May 26, 2015 · 1 comment

Comments

@samuelgruetter
Copy link
Contributor

In this example

import leon.collection._

object Test {

  def id(x: BigInt): BigInt = {
    require(x >= 2)
    x
  }

  def go(start: BigInt): List[BigInt] = {
    require(start >= 2)
    Cons(start, Nil()).map(id)
  }

  // let's --eval this:
  def c1 = go(2)
}

Leon says it found a counter-example:

[  Info  ]  - Now considering 'precond. (call id(x))' VC for go @15:28...
[ Error  ]  => INVALID
[ Error  ] Found counter-example:
[ Error  ]   start -> 2
[ Error  ]   x     -> 0
[  Info  ]  - Now considering 'precond. (call go(2))' VC for c1 @19:12...
[  Info  ]  => VALID
[  Info  ]   ┌──────────────────────┐
[  Info  ] ╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └──────────────────────┘                                                                   ║
[  Info  ] ║ c1    precond. (call go(2))                   19:12      valid          Z3-f         0.004 ║
[  Info  ] ║ go    precond. (call id(x))                   15:28      invalid        Z3-f         0.023 ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 2      valid: 1      invalid: 1      unknown 0                                0.027 ║
[  Info  ] ╚════════════════════════════════════════════════════════════════════════════════════════════╝

If I understand correctly, it says that the call to id in Cons(start, Nil()).map(id) does not respect the precondition of id. But it does, because start is required to be >= 2.

@samarion
Copy link
Member

Yes, this is a known issue. Currently, we cannot handle functions with preconditions inside of lambdas (id is desugared to x => id(x)). I'm currently working on finding a nice way of dealing with this limitation but I'm afraid this might require some form of universal quantification.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants