From 8b01cfead09490a59fc7ef1c9da69da0504bd196 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 20 May 2015 18:58:56 +0200
Subject: [PATCH] some datastructure benchmark are actually algorithms
---
.../datastructures/InsertionSort.scala | 74 -------------------
.../MergeSort.scala | 0
.../QuickSort.scala | 0
3 files changed, 74 deletions(-)
delete mode 100644 testcases/verification/datastructures/InsertionSort.scala
rename testcases/verification/{datastructures => list-algorithms}/MergeSort.scala (100%)
rename testcases/verification/{datastructures => list-algorithms}/QuickSort.scala (100%)
diff --git a/testcases/verification/datastructures/InsertionSort.scala b/testcases/verification/datastructures/InsertionSort.scala
deleted file mode 100644
index fcb2b94d5..000000000
--- a/testcases/verification/datastructures/InsertionSort.scala
+++ /dev/null
@@ -1,74 +0,0 @@
-import leon.lang._
-
-object InsertionSort {
- sealed abstract class List
- case class Cons(head:Int,tail:List) extends List
- case class Nil() extends List
-
- sealed abstract class OptInt
- case class Some(value: Int) extends OptInt
- case class None() extends OptInt
-
- def size(l : List) : Int = (l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def contents(l: List): Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(x,xs) => contents(xs) ++ Set(x)
- }
-
- def min(l : List) : OptInt = l match {
- case Nil() => None()
- case Cons(x, xs) => min(xs) match {
- case None() => Some(x)
- case Some(x2) => if(x < x2) Some(x) else Some(x2)
- }
- }
-
- def minProp0(l : List) : Boolean = (l match {
- case Nil() => true
- case c @ Cons(x, xs) => min(c) match {
- case None() => false
- case Some(m) => x >= m
- }
- }) holds
-
- def minProp1(l : List) : Boolean = {
- require(isSorted(l) && size(l) <= 5)
- l match {
- case Nil() => true
- case c @ Cons(x, xs) => min(c) match {
- case None() => false
- case Some(m) => x == m
- }
- }
- } holds
-
- def isSorted(l: List): Boolean = l match {
- case Nil() => true
- case Cons(x, Nil()) => true
- case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
-
- def sortedIns(e: Int, l: List): List = {
- require(isSorted(l) && size(l) <= 5)
- l match {
- case Nil() => Cons(e,Nil())
- case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e) && isSorted(res))
-
- def sort(l: List): List = (l match {
- case Nil() => Nil()
- case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l) && isSorted(res))
-
- 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(sort(ls))
- }
-}
diff --git a/testcases/verification/datastructures/MergeSort.scala b/testcases/verification/list-algorithms/MergeSort.scala
similarity index 100%
rename from testcases/verification/datastructures/MergeSort.scala
rename to testcases/verification/list-algorithms/MergeSort.scala
diff --git a/testcases/verification/datastructures/QuickSort.scala b/testcases/verification/list-algorithms/QuickSort.scala
similarity index 100%
rename from testcases/verification/datastructures/QuickSort.scala
rename to testcases/verification/list-algorithms/QuickSort.scala
--
GitLab