diff --git a/testcases/verification/list-algorithms/MergeSort.scala b/testcases/verification/list-algorithms/MergeSort.scala index ed4cda282724dd60474325e58d78d53e1c13e923..9ba13b7893787c9b8c77ed9f2793c891ef319acb 100644 --- a/testcases/verification/list-algorithms/MergeSort.scala +++ b/testcases/verification/list-algorithms/MergeSort.scala @@ -26,7 +26,12 @@ object MergeSort { } def split(l: List[BigInt]): (List[BigInt], List[BigInt]) = { + require(l.size > 1) l match { + case Cons(h1, Cons(h2, Nil())) => + (List(h1), List(h2)) + case Cons(h1, Cons(h2, Cons(h3, Nil()))) => + (List(h1, h3), List(h2)) case Cons(h1, Cons(h2, tail)) => val (rec1, rec2) = split(tail) (h1 :: rec1, h2 :: rec2) @@ -34,15 +39,16 @@ object MergeSort { } } ensuring { (res: (List[BigInt], List[BigInt])) => val (r1, r2) = res + r1.size < l.size && r2.size < l.size && r1.size + r2.size == l.size && - r1.content ++ r2.content == l.content && - r1.size - r2.size <= 1 && - r2.size - r1.size <= 1 + r1.content ++ r2.content == l.content } def mergeSort(l: List[BigInt]): List[BigInt] = { - val (l1, l2) = split(l) - merge(mergeSort(l1), mergeSort(l2)) + if (l.size <= 1) l else { + val (l1, l2) = split(l) + merge(mergeSort(l1), mergeSort(l2)) + } } ensuring ( res => isSorted(res) && res.content == l.content &&