From 6596b51188580fc2f59ad722dcfef771796f1a66 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Wed, 23 Sep 2015 16:27:39 +0200
Subject: [PATCH] Termination works in parallel merge sort, passing length as
parameter. Addeded it as testcase.
---
.../verification/list-algorithms/BasicMergeSortPar.scala | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/testcases/verification/list-algorithms/BasicMergeSortPar.scala b/testcases/verification/list-algorithms/BasicMergeSortPar.scala
index 4ea97244f..843a617ee 100644
--- a/testcases/verification/list-algorithms/BasicMergeSortPar.scala
+++ b/testcases/verification/list-algorithms/BasicMergeSortPar.scala
@@ -22,12 +22,13 @@ object MergeSortPar {
} ensuring { res => res.content == xs.content ++ ys.content &&
res.size == xs.size + ys.size }
- def msort[T](less: (T, T) => Boolean)(l: List[T]): List[T] = {
+ def msort[T](less: (T, T) => Boolean)(l: List[T], len : BigInt): List[T] = {
+ require(len == l.length)
if (l.size <= 1) l
else {
- val c = l.length/2
+ val c = len/2
val (first, second) = l.splitAtIndex(c) // evenSplit
- val (s1, s2) = parallel(msort(less)(first), msort(less)(second))
+ val (s1, s2) = parallel(msort(less)(first, c), msort(less)(second, len - c))
merge(less)(s1, s2)
}
} ensuring { res => res.content == l.content &&
--
GitLab