From 64c3a07c666a81128ec47b816c37d1471e3297d0 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 20 May 2015 18:55:38 +0200
Subject: [PATCH] pldi2011 testcases moved to proper directory
---
.../ForElimination.scala | 0
.../LambdaEval.scala | 0
.../SemanticsPreservation.scala | 0
.../ListTree.scala | 0
.../datastructures/QuickSort.scala | 90 +++++++++++--
.../RedBlackTreeDeletion.scala | 0
.../RedBlackTreeWithOrder.scala} | 0
.../TreeMap.scala | 0
.../list-algorithms/InsertionSort.scala | 19 +++
.../pldi2011-testcases/AssociativeList.scala | 59 --------
.../pldi2011-testcases/InsertionSort.scala | 98 --------------
.../pldi2011-testcases/MergeSort.scala | 69 ----------
.../PropositionalLogic.scala | 85 ------------
.../pldi2011-testcases/QuickSort.scala | 126 ------------------
14 files changed, 98 insertions(+), 448 deletions(-)
rename testcases/verification/{pldi2011-testcases => compilation}/ForElimination.scala (100%)
rename testcases/verification/{pldi2011-testcases => compilation}/LambdaEval.scala (100%)
rename testcases/verification/{pldi2011-testcases => compilation}/SemanticsPreservation.scala (100%)
rename testcases/verification/{pldi2011-testcases => datastructures}/ListTree.scala (100%)
rename testcases/verification/{pldi2011-testcases => datastructures}/RedBlackTreeDeletion.scala (100%)
rename testcases/verification/{pldi2011-testcases/RedBlackTree.scala => datastructures/RedBlackTreeWithOrder.scala} (100%)
rename testcases/verification/{pldi2011-testcases => datastructures}/TreeMap.scala (100%)
delete mode 100644 testcases/verification/pldi2011-testcases/AssociativeList.scala
delete mode 100644 testcases/verification/pldi2011-testcases/InsertionSort.scala
delete mode 100644 testcases/verification/pldi2011-testcases/MergeSort.scala
delete mode 100644 testcases/verification/pldi2011-testcases/PropositionalLogic.scala
delete mode 100644 testcases/verification/pldi2011-testcases/QuickSort.scala
diff --git a/testcases/verification/pldi2011-testcases/ForElimination.scala b/testcases/verification/compilation/ForElimination.scala
similarity index 100%
rename from testcases/verification/pldi2011-testcases/ForElimination.scala
rename to testcases/verification/compilation/ForElimination.scala
diff --git a/testcases/verification/pldi2011-testcases/LambdaEval.scala b/testcases/verification/compilation/LambdaEval.scala
similarity index 100%
rename from testcases/verification/pldi2011-testcases/LambdaEval.scala
rename to testcases/verification/compilation/LambdaEval.scala
diff --git a/testcases/verification/pldi2011-testcases/SemanticsPreservation.scala b/testcases/verification/compilation/SemanticsPreservation.scala
similarity index 100%
rename from testcases/verification/pldi2011-testcases/SemanticsPreservation.scala
rename to testcases/verification/compilation/SemanticsPreservation.scala
diff --git a/testcases/verification/pldi2011-testcases/ListTree.scala b/testcases/verification/datastructures/ListTree.scala
similarity index 100%
rename from testcases/verification/pldi2011-testcases/ListTree.scala
rename to testcases/verification/datastructures/ListTree.scala
diff --git a/testcases/verification/datastructures/QuickSort.scala b/testcases/verification/datastructures/QuickSort.scala
index cb193d2c8..30b362143 100644
--- a/testcases/verification/datastructures/QuickSort.scala
+++ b/testcases/verification/datastructures/QuickSort.scala
@@ -1,53 +1,121 @@
import leon.lang._
+import leon.annotation._
object QuickSort {
sealed abstract class List
case class Cons(head:Int,tail:List) extends List
case class Nil() extends List
- def contents(l: List): Set[Int] = l match {
+ sealed abstract class OptInt
+ case class Some(i: Int) extends OptInt
+ case class None() extends OptInt
+
+ def content(l: List): Set[Int] = l match {
case Nil() => Set.empty
- case Cons(x,xs) => contents(xs) ++ Set(x)
+ case Cons(x,xs) => content(xs) ++ Set(x)
+ }
+
+ def contains(l: List, e: Int): Boolean = l match {
+ case Nil() => false
+ case Cons(x, xs) => x == e || contains(xs, e)
}
- def is_sorted(l: List): Boolean = l match {
+ def isSorted(l: List): Boolean = l match {
case Nil() => true
case Cons(x,Nil()) => true
- case Cons(x,Cons(y,xs)) => x<=y && is_sorted(Cons(y,xs))
+ case Cons(x,Cons(y,xs)) => x<=y && isSorted(Cons(y,xs))
+ }
+
+ def min(l: List): OptInt = l match {
+ case Nil() => None()
+ case Cons(x, xs) => min(xs) match {
+ case Some(m) => if (x <= m) Some(x) else Some(m)
+ case None() => Some(x)
+ }
}
- def rev_append(aList:List,bList:List): List = aList match {
+ def max(l: List): OptInt = l match {
+ case Nil() => None()
+ case Cons(x, xs) => max(xs) match {
+ case Some(m) => if (x >= m) Some(x) else Some(m)
+ case None() => Some(x)
+ }
+ }
+
+ def rev_append(aList:List,bList:List): List = (aList match {
case Nil() => bList
case Cons(x,xs) => rev_append(xs,Cons(x,bList))
- }
+ }) ensuring(content(_) == content(aList) ++ content(bList))
- def reverse(list:List): List = rev_append(list,Nil())
+ def reverse(list:List): List = rev_append(list,Nil()) ensuring(content(_) == content(list))
- def append(aList:List,bList:List): List = aList match {
+ def append(aList:List,bList:List): List = (aList match {
case Nil() => bList
case _ => rev_append(reverse(aList),bList)
- }
-
+ }) ensuring(content(_) == content(aList) ++ content(bList))
+
def greater(n:Int,list:List) : List = list match {
case Nil() => Nil()
case Cons(x,xs) => if (n < x) Cons(x,greater(n,xs)) else greater(n,xs)
}
+ @induct
+ def greaterProp(n: Int, list: List): Boolean = (min(greater(n, list)) match {
+ case Some(m) => n < m
+ case None() => true
+ }) holds
+
def smaller(n:Int,list:List) : List = list match {
case Nil() => Nil()
case Cons(x,xs) => if (n>x) Cons(x,smaller(n,xs)) else smaller(n,xs)
}
+
+ @induct
+ def smallerProp(n: Int, list: List): Boolean = (max(smaller(n, list)) match {
+ case Some(m) => n > m
+ case None() => true
+ }) holds
def equals(n:Int,list:List) : List = list match {
case Nil() => Nil()
case Cons(x,xs) => if (n==x) Cons(x,equals(n,xs)) else equals(n,xs)
}
+ @induct
+ def equalsProp1(n: Int, list: List): Boolean = (max(equals(n, list)) match {
+ case Some(m) => n == m
+ case None() => true
+ }) holds
+
+ @induct
+ def equalsProp2(n: Int, list: List): Boolean = (min(equals(n, list)) match {
+ case Some(m) => n == m
+ case None() => true
+ }) holds
+
+ @induct
+ def smallerContent(n: Int, e: Int, l: List): Boolean = {
+ !(contains(l, e) && e < n) || contains(smaller(n, l),e)
+ } holds
+
+ @induct
+ def greaterContent(n: Int, e: Int, l: List): Boolean = {
+ !(contains(l, e) && e > n) || contains(greater(n, l),e)
+ } holds
+
+ @induct
+ def equalsContent(n: Int, e: Int, l: List): Boolean = {
+ !(contains(l, e) && e == n) || contains(equals(n, l),e)
+ } holds
+
+ def partitionProp(n: Int, e: Int, l: List): Boolean =
+ (!contains(l, e) || (contains(smaller(n, l), e) || contains(equals(n,l), e) || contains(greater(n, l), e))) // holds
+
def quickSort(list:List): List = (list match {
case Nil() => Nil()
case Cons(x,Nil()) => list
case Cons(x,xs) => append(append(quickSort(smaller(x,xs)),Cons(x,equals(x,xs))),quickSort(greater(x,xs)))
- }) ensuring(res => contents(res) == contents(list)) // && is_sorted(res))
+ }) ensuring(res => content(res) == content(list)) // && isSorted(res))
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/testcases/verification/pldi2011-testcases/RedBlackTreeDeletion.scala b/testcases/verification/datastructures/RedBlackTreeDeletion.scala
similarity index 100%
rename from testcases/verification/pldi2011-testcases/RedBlackTreeDeletion.scala
rename to testcases/verification/datastructures/RedBlackTreeDeletion.scala
diff --git a/testcases/verification/pldi2011-testcases/RedBlackTree.scala b/testcases/verification/datastructures/RedBlackTreeWithOrder.scala
similarity index 100%
rename from testcases/verification/pldi2011-testcases/RedBlackTree.scala
rename to testcases/verification/datastructures/RedBlackTreeWithOrder.scala
diff --git a/testcases/verification/pldi2011-testcases/TreeMap.scala b/testcases/verification/datastructures/TreeMap.scala
similarity index 100%
rename from testcases/verification/pldi2011-testcases/TreeMap.scala
rename to testcases/verification/datastructures/TreeMap.scala
diff --git a/testcases/verification/list-algorithms/InsertionSort.scala b/testcases/verification/list-algorithms/InsertionSort.scala
index 5c7419ce5..35062e263 100644
--- a/testcases/verification/list-algorithms/InsertionSort.scala
+++ b/testcases/verification/list-algorithms/InsertionSort.scala
@@ -28,6 +28,25 @@ object InsertionSort {
}
}
+ 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
diff --git a/testcases/verification/pldi2011-testcases/AssociativeList.scala b/testcases/verification/pldi2011-testcases/AssociativeList.scala
deleted file mode 100644
index 5f5dd8ae1..000000000
--- a/testcases/verification/pldi2011-testcases/AssociativeList.scala
+++ /dev/null
@@ -1,59 +0,0 @@
-import leon.lang._
-import leon.annotation._
-
-object AssociativeList {
- sealed abstract class KeyValuePairAbs
- case class KeyValuePair(key: Int, value: Int) extends KeyValuePairAbs
-
- sealed abstract class List
- case class Cons(head: KeyValuePairAbs, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class OptInt
- case class Some(i: Int) extends OptInt
- case class None() extends OptInt
-
- def domain(l: List): Set[Int] = l match {
- case Nil() => Set.empty[Int]
- case Cons(KeyValuePair(k,_), xs) => Set(k) ++ domain(xs)
- }
-
- def find(l: List, e: Int): OptInt = l match {
- case Nil() => None()
- case Cons(KeyValuePair(k, v), xs) => if (k == e) Some(v) else find(xs, e)
- }
-
- def noDuplicates(l: List): Boolean = l match {
- case Nil() => true
- case Cons(KeyValuePair(k, v), xs) => find(xs, k) == None() && noDuplicates(xs)
- }
-
- def update(l1: List, l2: List): List = (l2 match {
- case Nil() => l1
- case Cons(x, xs) => update(updateElem(l1, x), xs)
- }) ensuring(domain(_) == domain(l1) ++ domain(l2))
-
- def updateElem(l: List, e: KeyValuePairAbs): List = (l match {
- case Nil() => Cons(e, Nil())
- case Cons(KeyValuePair(k, v), xs) => e match {
- case KeyValuePair(ek, ev) => if (ek == k) Cons(KeyValuePair(ek, ev), xs) else Cons(KeyValuePair(k, v), updateElem(xs, e))
- }
- }) ensuring(res => e match {
- case KeyValuePair(k, v) => domain(res) == domain(l) ++ Set[Int](k)
- })
-
- @induct
- def readOverWrite(l: List, e: KeyValuePairAbs, k: Int) : Boolean = (e match {
- case KeyValuePair(key, value) =>
- find(updateElem(l, e), k) == (if (k == key) Some(value) else find(l, k))
- }) holds
-
- // def prop0(e: Int): Boolean = (find(update(Nil(), Nil()), e) == find(Nil(), e)) holds
-
- def main(args: Array[String]): Unit = {
- val l = Cons(KeyValuePair(6, 1), Cons(KeyValuePair(5, 4), Cons(KeyValuePair(3, 2), Nil())))
- val e = 0
- println(find(update(Nil(), l), e))
- println(find(l, e))
- }
-}
diff --git a/testcases/verification/pldi2011-testcases/InsertionSort.scala b/testcases/verification/pldi2011-testcases/InsertionSort.scala
deleted file mode 100644
index a201e6eb1..000000000
--- a/testcases/verification/pldi2011-testcases/InsertionSort.scala
+++ /dev/null
@@ -1,98 +0,0 @@
-import leon.annotation._
-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))
- }
-
- /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
- * the expected content and size */
- def sortedIns(e: Int, l: List): List = {
- require(isSorted(l))
- 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)
- && size(res) == size(l) + 1
- )
-
- /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
- * the expected content and size */
- def buggySortedIns(e: Int, l: List): List = {
- // require(isSorted(l))
- l match {
- case Nil() => Cons(e,Nil())
- case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
- && isSorted(res)
- && size(res) == size(l) + 1
- )
-
- /* Insertion sort yields a sorted list of same size and content as the input
- * list */
- 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)
- && size(res) == size(l)
- )
-
- 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/pldi2011-testcases/MergeSort.scala b/testcases/verification/pldi2011-testcases/MergeSort.scala
deleted file mode 100644
index 96e81e40e..000000000
--- a/testcases/verification/pldi2011-testcases/MergeSort.scala
+++ /dev/null
@@ -1,69 +0,0 @@
-import leon.lang._
-
-object MergeSort {
- sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
- case class Nil() extends List
-
- sealed abstract class PairAbs
- case class Pair(fst : List, snd : List) extends PairAbs
-
- def contents(l : List) : Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(x,xs) => contents(xs) ++ Set(x)
- }
-
- def isSorted(l : List) : Boolean = l match {
- case Nil() => true
- case Cons(x,xs) => xs match {
- case Nil() => true
- case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
- }
- }
-
- def size(list : List) : Int = list match {
- case Nil() => 0
- case Cons(x,xs) => 1 + size(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(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,size(list)/2)
- merge(mergeSort(p.fst), mergeSort(p.snd))
- }) ensuring(res => contents(res) == contents(list) && 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(mergeSort(ls))
- }
-}
diff --git a/testcases/verification/pldi2011-testcases/PropositionalLogic.scala b/testcases/verification/pldi2011-testcases/PropositionalLogic.scala
deleted file mode 100644
index 8356d2cbf..000000000
--- a/testcases/verification/pldi2011-testcases/PropositionalLogic.scala
+++ /dev/null
@@ -1,85 +0,0 @@
-import leon.lang._
-import leon.annotation._
-
-object PropositionalLogic {
-
- sealed abstract class Formula
- case class And(lhs: Formula, rhs: Formula) extends Formula
- case class Or(lhs: Formula, rhs: Formula) extends Formula
- case class Implies(lhs: Formula, rhs: Formula) extends Formula
- case class Not(f: Formula) extends Formula
- case class Literal(id: Int) extends Formula
-
- def simplify(f: Formula): Formula = (f match {
- case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
- case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
- case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
- case Not(f) => Not(simplify(f))
- case Literal(_) => f
- }) ensuring(isSimplified(_))
-
- def isSimplified(f: Formula): Boolean = f match {
- case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
- case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
- case Implies(_,_) => false
- case Not(f) => isSimplified(f)
- case Literal(_) => true
- }
-
- def nnf(formula: Formula): Formula = (formula match {
- case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
- case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
- case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
- case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
- case Not(Not(f)) => nnf(f)
- case Not(Literal(_)) => formula
- case Literal(_) => formula
- }) ensuring(isNNF(_))
-
- def isNNF(f: Formula): Boolean = f match {
- case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
- case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
- case Implies(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
- case Not(Literal(_)) => true
- case Not(_) => false
- case Literal(_) => true
- }
-
- def vars(f: Formula): Set[Int] = {
- require(isNNF(f))
- f match {
- case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Not(Literal(i)) => Set[Int](i)
- case Literal(i) => Set[Int](i)
- }
- }
-
- def fv(f : Formula) = { vars(nnf(f)) }
-
- @induct
- def wrongCommutative(f: Formula) : Boolean = {
- nnf(simplify(f)) == simplify(nnf(f))
- } holds
-
- @induct
- def simplifyBreaksNNF(f: Formula) : Boolean = {
- require(isNNF(f))
- isNNF(simplify(f))
- } holds
-
- @induct
- def nnfIsStable(f: Formula) : Boolean = {
- require(isNNF(f))
- nnf(f) == f
- } holds
-
- @induct
- def simplifyIsStable(f: Formula) : Boolean = {
- require(isSimplified(f))
- simplify(f) == f
- } holds
-}
diff --git a/testcases/verification/pldi2011-testcases/QuickSort.scala b/testcases/verification/pldi2011-testcases/QuickSort.scala
deleted file mode 100644
index 30b362143..000000000
--- a/testcases/verification/pldi2011-testcases/QuickSort.scala
+++ /dev/null
@@ -1,126 +0,0 @@
-import leon.lang._
-import leon.annotation._
-
-object QuickSort {
- 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(i: Int) extends OptInt
- case class None() extends OptInt
-
- def content(l: List): Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(x,xs) => content(xs) ++ Set(x)
- }
-
- def contains(l: List, e: Int): Boolean = l match {
- case Nil() => false
- case Cons(x, xs) => x == e || contains(xs, e)
- }
-
- def isSorted(l: List): Boolean = l match {
- case Nil() => true
- case Cons(x,Nil()) => true
- case Cons(x,Cons(y,xs)) => x<=y && isSorted(Cons(y,xs))
- }
-
- def min(l: List): OptInt = l match {
- case Nil() => None()
- case Cons(x, xs) => min(xs) match {
- case Some(m) => if (x <= m) Some(x) else Some(m)
- case None() => Some(x)
- }
- }
-
- def max(l: List): OptInt = l match {
- case Nil() => None()
- case Cons(x, xs) => max(xs) match {
- case Some(m) => if (x >= m) Some(x) else Some(m)
- case None() => Some(x)
- }
- }
-
- def rev_append(aList:List,bList:List): List = (aList match {
- case Nil() => bList
- case Cons(x,xs) => rev_append(xs,Cons(x,bList))
- }) ensuring(content(_) == content(aList) ++ content(bList))
-
- def reverse(list:List): List = rev_append(list,Nil()) ensuring(content(_) == content(list))
-
- def append(aList:List,bList:List): List = (aList match {
- case Nil() => bList
- case _ => rev_append(reverse(aList),bList)
- }) ensuring(content(_) == content(aList) ++ content(bList))
-
- def greater(n:Int,list:List) : List = list match {
- case Nil() => Nil()
- case Cons(x,xs) => if (n < x) Cons(x,greater(n,xs)) else greater(n,xs)
- }
-
- @induct
- def greaterProp(n: Int, list: List): Boolean = (min(greater(n, list)) match {
- case Some(m) => n < m
- case None() => true
- }) holds
-
- def smaller(n:Int,list:List) : List = list match {
- case Nil() => Nil()
- case Cons(x,xs) => if (n>x) Cons(x,smaller(n,xs)) else smaller(n,xs)
- }
-
- @induct
- def smallerProp(n: Int, list: List): Boolean = (max(smaller(n, list)) match {
- case Some(m) => n > m
- case None() => true
- }) holds
-
- def equals(n:Int,list:List) : List = list match {
- case Nil() => Nil()
- case Cons(x,xs) => if (n==x) Cons(x,equals(n,xs)) else equals(n,xs)
- }
-
- @induct
- def equalsProp1(n: Int, list: List): Boolean = (max(equals(n, list)) match {
- case Some(m) => n == m
- case None() => true
- }) holds
-
- @induct
- def equalsProp2(n: Int, list: List): Boolean = (min(equals(n, list)) match {
- case Some(m) => n == m
- case None() => true
- }) holds
-
- @induct
- def smallerContent(n: Int, e: Int, l: List): Boolean = {
- !(contains(l, e) && e < n) || contains(smaller(n, l),e)
- } holds
-
- @induct
- def greaterContent(n: Int, e: Int, l: List): Boolean = {
- !(contains(l, e) && e > n) || contains(greater(n, l),e)
- } holds
-
- @induct
- def equalsContent(n: Int, e: Int, l: List): Boolean = {
- !(contains(l, e) && e == n) || contains(equals(n, l),e)
- } holds
-
- def partitionProp(n: Int, e: Int, l: List): Boolean =
- (!contains(l, e) || (contains(smaller(n, l), e) || contains(equals(n,l), e) || contains(greater(n, l), e))) // holds
-
- def quickSort(list:List): List = (list match {
- case Nil() => Nil()
- case Cons(x,Nil()) => list
- case Cons(x,xs) => append(append(quickSort(smaller(x,xs)),Cons(x,equals(x,xs))),quickSort(greater(x,xs)))
- }) ensuring(res => content(res) == content(list)) // && 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(quickSort(ls))
- }
-}
--
GitLab