From 24d8dfc112abb3aab7d68e5963305cbecf5cdcdf Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 11 Dec 2014 17:51:30 +0100
Subject: [PATCH] Add some challenging tests
---
.../repair/OffByOne/FirstIndexOf.scala | 31 +++++++++++++++++++
.../repair/OffByOne/FirstIndexOf1.scala | 31 +++++++++++++++++++
.../repair/OffByOne/FirstIndexOf2.scala | 31 +++++++++++++++++++
3 files changed, 93 insertions(+)
create mode 100644 testcases/synthesis/repair/OffByOne/FirstIndexOf.scala
create mode 100644 testcases/synthesis/repair/OffByOne/FirstIndexOf1.scala
create mode 100644 testcases/synthesis/repair/OffByOne/FirstIndexOf2.scala
diff --git a/testcases/synthesis/repair/OffByOne/FirstIndexOf.scala b/testcases/synthesis/repair/OffByOne/FirstIndexOf.scala
new file mode 100644
index 000000000..d59131506
--- /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 000000000..382e09a2f
--- /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 000000000..bf78b606f
--- /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
+ })
+ }
+}
--
GitLab