From 6dea823a83a29a82a10897df72d2f3d598ff4ccc Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Wed, 23 Sep 2015 10:40:34 +0200
Subject: [PATCH] Made merge sort verify using better specified splitAtIndex.
---
library/par/package.scala | 1 +
testcases/verification/list-algorithms/BasicMergeSort.scala | 3 ++-
.../verification/list-algorithms/BasicMergeSortPar.scala | 6 ++++--
3 files changed, 7 insertions(+), 3 deletions(-)
diff --git a/library/par/package.scala b/library/par/package.scala
index 4690eddbf..6e8d1d571 100644
--- a/library/par/package.scala
+++ b/library/par/package.scala
@@ -9,6 +9,7 @@ import leon.lang.synthesis.choose
package object par {
// @library
+ @inline
def parallel[A,B](x: => A, y: => B) : (A,B) = {
(x,y)
}
diff --git a/testcases/verification/list-algorithms/BasicMergeSort.scala b/testcases/verification/list-algorithms/BasicMergeSort.scala
index 474f768a5..55e632ff8 100644
--- a/testcases/verification/list-algorithms/BasicMergeSort.scala
+++ b/testcases/verification/list-algorithms/BasicMergeSort.scala
@@ -18,7 +18,8 @@ object MergeSort {
def msort[T](less: (T, T) => Boolean)(l: List[T]): List[T] = {
if (l.size <= 1) l
else {
- val (first, second) = l.evenSplit
+ val c = l.length/2
+ val (first, second) = l.splitAtIndex(c) // evenSplit
merge(less)(msort(less)(first), msort(less)(second))
}
} ensuring { res => res.content == l.content && res.size == l.size }
diff --git a/testcases/verification/list-algorithms/BasicMergeSortPar.scala b/testcases/verification/list-algorithms/BasicMergeSortPar.scala
index e5620482d..493122b2f 100644
--- a/testcases/verification/list-algorithms/BasicMergeSortPar.scala
+++ b/testcases/verification/list-algorithms/BasicMergeSortPar.scala
@@ -19,9 +19,11 @@ object MergeSortPar {
def msort[T](less: (T, T) => Boolean)(l: List[T]): List[T] = {
if (l.size <= 1) l
else {
- val (first, second) = l.evenSplit
+ val c = l.length/2
+ val (first, second) = l.splitAtIndex(c) // evenSplit
val (s1, s2) = parallel(msort(less)(first), msort(less)(second))
merge(less)(s1, s2)
}
- } ensuring { res => res.content == l.content && res.size == l.size }
+ } ensuring { res => res.content == l.content &&
+ res.size == l.size }
}
--
GitLab