diff --git a/testcases/synthesis/repair/OffByOne/FirstIndexOf.scala b/testcases/synthesis/repair/OffByOne/FirstIndexOf.scala new file mode 100644 index 0000000000000000000000000000000000000000..d591315063d90c26b2adfbe7bdd36b03d4871a99 --- /dev/null +++ b/testcases/synthesis/repair/OffByOne/FirstIndexOf.scala @@ -0,0 +1,31 @@ +import leon.lang._ +import leon.collection._ +import leon.lang.synthesis._ + + +object FirstIndexOf { + def firstIndexOf(l: List[Int], v: Int): Int = { + l match { + case Cons(h, t) if v == h => 0 + case Cons(h, t) => + if (firstIndexOf(t, v) >= 0) { + firstIndexOf(t, v)+1 + } else { + -1 + } + case Nil() => + -1 + } + } ensuring { + (res: Int) => (if (l.content contains v) { + l.size > res && l.apply(res) == v + } else { + res == -1 + }) && (((l,v), res) passes { + case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) => 3 + case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) => 3 + case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) => 1 + case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) => -1 + }) + } +} diff --git a/testcases/synthesis/repair/OffByOne/FirstIndexOf1.scala b/testcases/synthesis/repair/OffByOne/FirstIndexOf1.scala new file mode 100644 index 0000000000000000000000000000000000000000..382e09a2f4d20e7a0bc53be5a56f132e6b6ba717 --- /dev/null +++ b/testcases/synthesis/repair/OffByOne/FirstIndexOf1.scala @@ -0,0 +1,31 @@ +import leon.lang._ +import leon.collection._ +import leon.lang.synthesis._ + + +object FirstIndexOf { + def firstIndexOf(l: List[Int], v: Int): Int = { + l match { + case Cons(h, t) if v == h => 0 + case Cons(h, t) => + if (firstIndexOf(t, v) >= 0) { + firstIndexOf(t, v) // Should be +1 (Solves with CEGIS) + } else { + -1 + } + case Nil() => + -1 + } + } ensuring { + (res: Int) => (if (l.content contains v) { + l.size > res && l.apply(res) == v + } else { + res == -1 + }) && (((l,v), res) passes { + case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) => 3 + case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) => 3 + case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) => 1 + case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) => -1 + }) + } +} diff --git a/testcases/synthesis/repair/OffByOne/FirstIndexOf2.scala b/testcases/synthesis/repair/OffByOne/FirstIndexOf2.scala new file mode 100644 index 0000000000000000000000000000000000000000..bf78b606fdf3895f3814882a8eb53e2139bec51b --- /dev/null +++ b/testcases/synthesis/repair/OffByOne/FirstIndexOf2.scala @@ -0,0 +1,31 @@ +import leon.lang._ +import leon.collection._ +import leon.lang.synthesis._ + + +object FirstIndexOf { + def firstIndexOf(l: List[Int], v: Int): Int = { + l match { + case Cons(h, t) if v == h => 0 + case Cons(h, t) => + if (firstIndexOf(t, v) >= 0) { + firstIndexOf(t, v)+2 // Should be +1 + } else { + -1 + } + case Nil() => + -1 + } + } ensuring { + (res: Int) => (if (l.content contains v) { + l.size > res && l.apply(res) == v + } else { + res == -1 + }) && (((l,v), res) passes { + case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) => 3 + case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) => 3 + case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) => 1 + case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) => -1 + }) + } +}