From 5516de65c3e98742c816af31ca999ac7663c4432 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 10 Mar 2016 15:05:15 +0100
Subject: [PATCH] Fix this benchmark
---
.../list-algorithms/MergeSort.scala | 93 ++++++++-----------
1 file changed, 39 insertions(+), 54 deletions(-)
diff --git a/testcases/verification/list-algorithms/MergeSort.scala b/testcases/verification/list-algorithms/MergeSort.scala
index 5fc80d117..ed4cda282 100644
--- a/testcases/verification/list-algorithms/MergeSort.scala
+++ b/testcases/verification/list-algorithms/MergeSort.scala
@@ -1,67 +1,52 @@
import leon.lang._
-import leon.annotation._
+import synthesis._
+import leon.collection._
object MergeSort {
- sealed abstract class List
- case class Cons(head:Int,tail:List) extends List
- case class Nil() extends List
- case class Pair(fst:List,snd:List)
-
- def contents(l: List): Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(x,xs) => contents(xs) ++ Set(x)
+ def isSorted(l: List[BigInt]): Boolean = l match {
+ case Cons(x, t@Cons(y, _)) => x <= y && isSorted(t)
+ case _ => true
}
- def is_sorted(l: List): Boolean = l match {
- case Nil() => true
- case Cons(x,xs) => xs match {
- case Nil() => true
- case Cons(y, ys) => x <= y && is_sorted(Cons(y, ys))
+ def merge(l1: List[BigInt], l2: List[BigInt]): List[BigInt] = {
+ require(isSorted(l1) && isSorted(l2))
+ (l1, l2) match {
+ case (Nil(), _) => l2
+ case (_, Nil()) => l1
+ case (Cons(h1,t1), Cons(h2, t2)) =>
+ if (h1 <= h2) Cons(h1, merge(t1, l2))
+ else Cons(h2, merge(l1, t2))
}
+ } ensuring {
+ (res: List[BigInt]) =>
+ isSorted(res) &&
+ res.content == l1.content ++ l2.content &&
+ res.size == l1.size + l2.size
}
- def length(list:List): Int = list match {
- case Nil() => 0
- case Cons(x,xs) => 1 + length(xs)
- }
-
- def splithelper(aList:List,bList:List,n:Int): Pair =
- if (n <= 0) Pair(aList,bList)
- else
- bList match {
- case Nil() => Pair(aList,bList)
- case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+ def split(l: List[BigInt]): (List[BigInt], List[BigInt]) = {
+ l match {
+ case Cons(h1, Cons(h2, tail)) =>
+ val (rec1, rec2) = split(tail)
+ (h1 :: rec1, h2 :: rec2)
+ case _ => (l, Nil[BigInt]())
}
+ } ensuring { (res: (List[BigInt], List[BigInt])) =>
+ val (r1, r2) = res
+ r1.size + r2.size == l.size &&
+ r1.content ++ r2.content == l.content &&
+ r1.size - r2.size <= 1 &&
+ r2.size - r1.size <= 1
+ }
- def split(list:List,n:Int): Pair = splithelper(Nil(),list,n)
-
- def merge(aList:List, bList:List):List = (bList match {
- case Nil() => aList
- case Cons(x,xs) =>
- aList match {
- case Nil() => bList
- case Cons(y,ys) =>
- if (y < x)
- Cons(y,merge(ys, bList))
- else
- Cons(x,merge(aList, xs))
- }
- }) ensuring(res => contents(res) == contents(aList) ++ contents(bList))
-
- def mergeSort(list:List):List = (list match {
- case Nil() => list
- case Cons(x,Nil()) => list
- case _ =>
- val p = split(list,length(list)/2)
- merge(mergeSort(p.fst), mergeSort(p.snd))
- }) ensuring(res => contents(res) == contents(list) && is_sorted(res))
-
+ def mergeSort(l: List[BigInt]): List[BigInt] = {
+ val (l1, l2) = split(l)
+ merge(mergeSort(l1), mergeSort(l2))
+ } ensuring ( res =>
+ isSorted(res) &&
+ res.content == l.content &&
+ res.size == l.size
+ )
- @ignore
- def main(args: Array[String]): Unit = {
- val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
- println(ls)
- println(mergeSort(ls))
- }
}
--
GitLab