From 9fccd029f944ecde07e48bc6733706d9344cc442 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 20 Dec 2012 20:48:09 +0100
Subject: [PATCH] New verification testcase.

Finite sorting functions (essentially, hard-coded insertion sort for up
to 5 values). Also included as a regression test.
---
 .../purescala/invalid/FiniteSort.scala        | 54 +++++++++++++
 .../purescala/valid/FiniteSort.scala          | 59 ++++++++++++++
 testcases/FiniteSort.scala                    | 80 +++++++++++++++++++
 3 files changed, 193 insertions(+)
 create mode 100644 src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala
 create mode 100644 src/test/resources/regression/verification/purescala/valid/FiniteSort.scala
 create mode 100644 testcases/FiniteSort.scala

diff --git a/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala b/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala
new file mode 100644
index 000000000..4020135ac
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala
@@ -0,0 +1,54 @@
+import leon.Utils._
+
+object FiniteSorting {
+
+  // These finite sorting functions essentially implement insertion sort.
+  def sort2(x : Int, y : Int) : (Int,Int) = {
+    if(x < y) (x, y) else (y, x)
+  }
+
+  def sort3(x1 : Int, x2 : Int, x3 : Int) : (Int, Int, Int) = {
+    val (x1s, x2s) = sort2(x1, x2)
+
+    if(x2s <= x3) {
+      (x1s, x2s, x3)
+    } else if(x1s <= x3) {
+      (x1s, x3, x2s)
+    } else {
+      (x3, x1s, x2s)
+    }
+  }
+
+  def sort4(x1 : Int, x2 : Int, x3 : Int, x4 : Int) : (Int, Int, Int, Int) = {
+    val (x1s, x2s, x3s) = sort3(x1, x2, x3)
+
+    if(x3s <= x4) {
+      (x1s, x2s, x3s, x4)
+    } else if(x2s <= x4) {
+      (x1s, x2s, x4, x3s)
+    } else if(x1s <= x4) {
+      (x1s, x4, x2s, x3s)
+    } else {
+      (x4, x1s, x2s, x3s)
+    }
+  }
+
+  def sort5WrongSpec(x1 : Int, x2 : Int, x3 : Int, x4 : Int, x5 : Int) : (Int, Int, Int, Int, Int) = {
+    val (x1s, x2s, x3s, x4s) = sort4(x1, x2, x3, x4)
+
+    if(x4s <= x5) {
+      (x1s, x2s, x3s, x4s, x5)
+    } else if(x3s <= x5) {
+      (x1s, x2s, x3s, x5, x4s)
+    } else if(x2s <= x5) {
+      (x1s, x2s, x5, x3s, x4s)
+    } else if(x1s <= x5) {
+      (x1s, x5, x2s, x3s, x4s)
+    } else {
+      (x5, x1s, x2s, x3s, x4s)
+    }
+
+  } ensuring (_ match {
+    case (a, b, c, d, e) => a <= b && b <= c && c <= d && d <= e && Set(a,b,c,d,e) == Set(x1,x2,x3,x4,x4) // last one should be x5
+  })
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/FiniteSort.scala b/src/test/resources/regression/verification/purescala/valid/FiniteSort.scala
new file mode 100644
index 000000000..5a4e243b8
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/FiniteSort.scala
@@ -0,0 +1,59 @@
+import leon.Utils._
+
+object FiniteSorting {
+
+  // These finite sorting functions essentially implement insertion sort.
+  def sort2(x : Int, y : Int) : (Int,Int) = {
+    if(x < y) (x, y) else (y, x)
+  } ensuring (_ match {
+    case (a, b) => a <= b && Set(a,b) == Set(x,y)
+  })
+
+  def sort3(x1 : Int, x2 : Int, x3 : Int) : (Int, Int, Int) = {
+    val (x1s, x2s) = sort2(x1, x2)
+
+    if(x2s <= x3) {
+      (x1s, x2s, x3)
+    } else if(x1s <= x3) {
+      (x1s, x3, x2s)
+    } else {
+      (x3, x1s, x2s)
+    }
+  } ensuring (_ match {
+    case (a, b, c) => a <= b && b <= c && Set(a,b,c) == Set(x1,x2,x3)
+  })
+
+  def sort4(x1 : Int, x2 : Int, x3 : Int, x4 : Int) : (Int, Int, Int, Int) = {
+    val (x1s, x2s, x3s) = sort3(x1, x2, x3)
+
+    if(x3s <= x4) {
+      (x1s, x2s, x3s, x4)
+    } else if(x2s <= x4) {
+      (x1s, x2s, x4, x3s)
+    } else if(x1s <= x4) {
+      (x1s, x4, x2s, x3s)
+    } else {
+      (x4, x1s, x2s, x3s)
+    }
+  } ensuring (_ match {
+    case (a, b, c, d) => a <= b && b <= c && c <= d && Set(a,b,c,d) == Set(x1,x2,x3,x4)
+  })
+
+  def sort5(x1 : Int, x2 : Int, x3 : Int, x4 : Int, x5 : Int) : (Int, Int, Int, Int, Int) = {
+    val (x1s, x2s, x3s, x4s) = sort4(x1, x2, x3, x4)
+
+    if(x4s <= x5) {
+      (x1s, x2s, x3s, x4s, x5)
+    } else if(x3s <= x5) {
+      (x1s, x2s, x3s, x5, x4s)
+    } else if(x2s <= x5) {
+      (x1s, x2s, x5, x3s, x4s)
+    } else if(x1s <= x5) {
+      (x1s, x5, x2s, x3s, x4s)
+    } else {
+      (x5, x1s, x2s, x3s, x4s)
+    }
+  } ensuring (_ match {
+    case (a, b, c, d, e) => a <= b && b <= c && c <= d && d <= e && Set(a,b,c,d,e) == Set(x1,x2,x3,x4,x5)
+  })
+}
diff --git a/testcases/FiniteSort.scala b/testcases/FiniteSort.scala
new file mode 100644
index 000000000..6f1431ced
--- /dev/null
+++ b/testcases/FiniteSort.scala
@@ -0,0 +1,80 @@
+import leon.Utils._
+
+object FiniteSorting {
+
+  // These finite sorting functions essentially implement insertion sort.
+  def sort2(x : Int, y : Int) : (Int,Int) = {
+    if(x < y) (x, y) else (y, x)
+  } ensuring (_ match {
+    case (a, b) => a <= b && Set(a,b) == Set(x,y)
+  })
+
+  def sort3(x1 : Int, x2 : Int, x3 : Int) : (Int, Int, Int) = {
+    val (x1s, x2s) = sort2(x1, x2)
+
+    if(x2s <= x3) {
+      (x1s, x2s, x3)
+    } else if(x1s <= x3) {
+      (x1s, x3, x2s)
+    } else {
+      (x3, x1s, x2s)
+    }
+  } ensuring (_ match {
+    case (a, b, c) => a <= b && b <= c && Set(a,b,c) == Set(x1,x2,x3)
+  })
+
+  def sort4(x1 : Int, x2 : Int, x3 : Int, x4 : Int) : (Int, Int, Int, Int) = {
+    val (x1s, x2s, x3s) = sort3(x1, x2, x3)
+
+    if(x3s <= x4) {
+      (x1s, x2s, x3s, x4)
+    } else if(x2s <= x4) {
+      (x1s, x2s, x4, x3s)
+    } else if(x1s <= x4) {
+      (x1s, x4, x2s, x3s)
+    } else {
+      (x4, x1s, x2s, x3s)
+    }
+
+  } ensuring (_ match {
+    case (a, b, c, d) => a <= b && b <= c && c <= d && Set(a,b,c,d) == Set(x1,x2,x3,x4)
+  })
+
+  def sort5(x1 : Int, x2 : Int, x3 : Int, x4 : Int, x5 : Int) : (Int, Int, Int, Int, Int) = {
+    val (x1s, x2s, x3s, x4s) = sort4(x1, x2, x3, x4)
+
+    if(x4s <= x5) {
+      (x1s, x2s, x3s, x4s, x5)
+    } else if(x3s <= x5) {
+      (x1s, x2s, x3s, x5, x4s)
+    } else if(x2s <= x5) {
+      (x1s, x2s, x5, x3s, x4s)
+    } else if(x1s <= x5) {
+      (x1s, x5, x2s, x3s, x4s)
+    } else {
+      (x5, x1s, x2s, x3s, x4s)
+    }
+
+  } ensuring (_ match {
+    case (a, b, c, d, e) => a <= b && b <= c && c <= d && d <= e && Set(a,b,c,d,e) == Set(x1,x2,x3,x4,x4)
+  })
+
+  def sort5WrongSpec(x1 : Int, x2 : Int, x3 : Int, x4 : Int, x5 : Int) : (Int, Int, Int, Int, Int) = {
+    val (x1s, x2s, x3s, x4s) = sort4(x1, x2, x3, x4)
+
+    if(x4s <= x5) {
+      (x1s, x2s, x3s, x4s, x5)
+    } else if(x3s <= x5) {
+      (x1s, x2s, x3s, x5, x4s)
+    } else if(x2s <= x5) {
+      (x1s, x2s, x5, x3s, x4s)
+    } else if(x1s <= x5) {
+      (x1s, x5, x2s, x3s, x4s)
+    } else {
+      (x5, x1s, x2s, x3s, x4s)
+    }
+
+  } ensuring (_ match {
+    case (a, b, c, d, e) => a <= b && b <= c && c <= d && d <= e && Set(a,b,c,d,e) == Set(x1,x2,x3,x4,x4)
+  })
+}
-- 
GitLab