From a5cfd07a3fabe2d024492495ecdb73964c646c14 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 25 Apr 2016 13:49:55 +0200
Subject: [PATCH] Fix mergeSort in list algorithms
---
.../verification/list-algorithms/MergeSort.scala | 16 +++++++++++-----
1 file changed, 11 insertions(+), 5 deletions(-)
diff --git a/testcases/verification/list-algorithms/MergeSort.scala b/testcases/verification/list-algorithms/MergeSort.scala
index ed4cda282..9ba13b789 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 &&
--
GitLab