1

I would like to use Leon to verify a spec without knowing the concrete implementations in advance. For example, suppose I have a sort function, as well as the definition of what a sorted list looks like:

def sort (list: List[BigInt]): List[BigInt] = {
    ...
  } ensuring {
    res => res.content == list.content && isSorted(res)
  }

def isSorted (list: List[BigInt]): Boolean = {
    list match {
      case Nil()                  => true
      case Cons(_, Nil())         => true
      case Cons(x1, Cons(x2, xs)) => x1 <= x2 && isSorted(list.tail)
    }
  }

Ideally, I should be able to prove lemmas such as sort(sort(list)) == sort(list) based on the post-condition of sort alone. Otherwise, I cannot claim that a Leon proof that works for insertion sort also works for quick sort (and in practice it seldom does). Is it possible for Leon to reason based on the pre- and post-conditions without looking into the implementation?

Thank you!

Eric Pony
  • 43
  • 4

1 Answers1

2

With the xlang extension (use --xlang on the command line, and supported by default in the web interface) you get access to the epsilon expression that takes a predicate and return an expression satisfying it. WIth it you can basically omit the implementation of some functions in the code. Your example then can be written as:

import leon.lang._
import leon.collection._
import leon.lang.xlang._

object Test {
  def isSorted(l: List[BigInt]): Boolean = l match {
    case Nil() => true
    case Cons(x, Nil()) => true
    case Cons(x, Cons(y, ys)) => x <= y && isSorted(l.tail)
  }
  def sort(l: List[BigInt]): List[BigInt] = epsilon((o: List[BigInt]) =>
    l.content == o.content && isSorted(l))
  def prop1(l: List[BigInt]): Boolean = {
    sort(sort(l)) == sort(l)
  } holds
}

Which does what you want. However the property prop1 above is invalid, as Leon will tell you. The issue is that the specification of sort only guarantees the same content, but it doesn't check for duplicates. So it would be valid for an implementation of sort to behave as such:

sort(List(1)) == List(1, 1)

and hence you could get:

sort(sort(List(1))) == List(1, 1, 1) != sort(List(1))

However, if you find a way to make the postcondition of sort stronger, then you should be able to use the above as a way to verify against a specification. Of course, if you have a different example than sort, you may be able to use epsilon without any issue, just watch out for the issue of under-specification.

Regis Blanc
  • 549
  • 2
  • 5
  • Thank you very much for the reply. This epsilon expression helps me find many flaws in my spec. The only problem is that the Leon web interface doesn't seem to support xlang desugaring by now, so I have to build Leon myself to use it. – Eric Pony Sep 08 '15 at 11:34
  • Regis: What is the difference between `epsilon` and `choose`? – larsrh Sep 08 '15 at 20:44
  • I am not very familiar with the details of `choose`, but I would say `choose` is more of a construct used for the synthesis module in Leon and might not be handled in the same way when doing verification. Epsilon are documented [here](http://leon.epfl.ch/doc/xlang.html#epsilon) and are not used in synthesis, only for specification. You can find some documentation on `choose` [here](http://leon.epfl.ch/doc/synthesis.html) but their main use is to express a code segment that should be synthesized. – Regis Blanc Sep 09 '15 at 14:05