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 0000000000000000000000000000000000000000..4020135aca5f042d07a693cbdbe1f7dce8195361 --- /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 0000000000000000000000000000000000000000..5a4e243b833052c0af6bc011e191bb6d28ea42a0 --- /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 0000000000000000000000000000000000000000..6f1431ced3c0e90a25d0b5469a17f0b5c1ae348b --- /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) + }) +}