3

I have an abstract Stack type as follows

abstract class Stack[T] {
  def empty  : Stack[T]
  def pop () : (Option[T], Stack[T])
  def push (e : T) : Stack[T]
  def size : BigInt
}

I would like to verify that pop returns the last pushed element:

// ok
def test_v1[T] (e : T, s : Stack[T]) : Boolean = {
  s.push(e).pop()._1 match {
    case Some(e2) => e == e2
    case _        => false
  }
} holds

// failed
def test_v2[T] (e : T, s : Stack[T]) : Boolean = {
  s.push(e).pop()._1 == Some(e)
} holds

The two lemmas are equivalent, but Leon fails to identify the type parameters in the second lemma. Interestingly, Leon has no problem when Stack is concrete or non-generic (see the link below for examples). Is this a feature of Leon or just a bug?

The full example code can be found here.

Eric Pony
  • 43
  • 4
  • You should not wrap e with Some(e) - it will work incorrectly on nullable e. Use Option(e) instead. – vvg Oct 29 '15 at 10:25
  • Judging by the error message I would think it's a bug. There's a type mismatch between to different `T`s. – larsrh Oct 29 '15 at 22:10
  • I tried the example in the gist link (under "can be found *here*") and it works in the current version of Leon, both online and in the git repository. So, if this was a bug it is fixed now. – vkuncak Mar 14 '16 at 16:02

1 Answers1

1

I tried the example in your gist link (under "can be found here") and it works in the current version of Leon, both online and in the git repository. So, if this was a bug, it is fixed now. If you have any related questions, we are happy to answer, because Leon supports only objects and case classes at this time, so there are differences compared to full Scala.

vkuncak
  • 123
  • 7