From b3f129fbf740f1514dd4129e37eac1bbae00c263 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Sun, 19 Apr 2015 00:39:54 +0200
Subject: [PATCH] A minimalistic sequential merge sort, to compare with
parallel one
---
.../verification/sorting/MergeSort.scala | 25 +++++++++++++++++++
1 file changed, 25 insertions(+)
create mode 100644 testcases/verification/sorting/MergeSort.scala
diff --git a/testcases/verification/sorting/MergeSort.scala b/testcases/verification/sorting/MergeSort.scala
new file mode 100644
index 000000000..474f768a5
--- /dev/null
+++ b/testcases/verification/sorting/MergeSort.scala
@@ -0,0 +1,25 @@
+import leon.lang._
+import leon.collection._
+object MergeSort {
+
+ def merge[T](less: (T, T) => Boolean)(xs: List[T], ys: List[T]): List[T] = {
+ (xs, ys) match {
+ case (Nil(), _) => ys
+ case (_, Nil()) => xs
+ case (Cons(x,xtail), Cons(y,ytail)) =>
+ if (less(x, y))
+ x :: merge(less)(xtail, ys)
+ else
+ y :: merge(less)(xs, ytail)
+ }
+ } 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] = {
+ if (l.size <= 1) l
+ else {
+ val (first, second) = l.evenSplit
+ merge(less)(msort(less)(first), msort(less)(second))
+ }
+ } ensuring { res => res.content == l.content && res.size == l.size }
+}
--
GitLab