From abd6a94c856d20e5771d46bdf233a54389830929 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 19 Dec 2012 02:26:53 +0100
Subject: [PATCH] Add various benchmarks
New Verification Benchmarks:
- Addresses
- AmortizedQueue
- TreeListSet
New Synthesis Benchmarks:
- List
- BinaryTree
- AVLTree (incomplete)
---
testcases/Addresses.scala | 74 +++++++
testcases/AmortizedQueueStrongSpec.scala | 212 +++++++++++++++++++
testcases/TreeListSetNoDup.scala | 100 +++++++++
testcases/synthesis/cav2013/AVLTree.scala | 90 ++++++++
testcases/synthesis/cav2013/BinaryTree.scala | 61 ++++++
testcases/synthesis/cav2013/List.scala | 64 ++++++
6 files changed, 601 insertions(+)
create mode 100644 testcases/Addresses.scala
create mode 100644 testcases/AmortizedQueueStrongSpec.scala
create mode 100644 testcases/TreeListSetNoDup.scala
create mode 100644 testcases/synthesis/cav2013/AVLTree.scala
create mode 100644 testcases/synthesis/cav2013/BinaryTree.scala
create mode 100644 testcases/synthesis/cav2013/List.scala
diff --git a/testcases/Addresses.scala b/testcases/Addresses.scala
new file mode 100644
index 000000000..82e354d76
--- /dev/null
+++ b/testcases/Addresses.scala
@@ -0,0 +1,74 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ // list of integers
+ sealed abstract class List
+ case class Cons(a:Int,b:Int,c:Int, tail:List) extends List
+ case class Nil() extends List
+
+ def empty() = Set.empty[Int]
+
+ def setA(l:List) : Set[Int] = l match {
+ case Nil() => empty
+ case Cons(a,b,c,l1) => Set(a) ++ setA(l1)
+ }
+
+ def containsA(x:Int,l:List) : Boolean = (l match {
+ case Nil() => false
+ case Cons(a,b,c,t) => a==x || containsA(x,t)
+ }) ensuring (res => res == (setA(l) contains x))
+
+ def theseAunique1(as:Set[Int],l:List) : Boolean = l match {
+ case Nil() => true
+ case Cons(a,b,c,l1) =>
+ theseAunique1(as,l1) && !(as contains a) && (setA(l1) contains a)
+ }
+
+ def theseAunique2(as:Set[Int],l:List) : Boolean = (l match {
+ case Nil() => true
+ case Cons(a,b,c,l1) =>
+ theseAunique2(as,l1) && !(as contains a) && containsA(a,l1)
+ }) ensuring (res => res==theseAunique1(as,l))
+
+ def disjoint(x:Set[Int],y:Set[Int]):Boolean =
+ x.intersect(y).isEmpty
+
+ def uniqueAbsentAs(unique:Set[Int],absent:Set[Int],l:List) : Boolean = (l match {
+ case Nil() => true
+ case Cons(a,b,c,l1) => {
+ !(absent contains a) &&
+ (if (unique contains a) uniqueAbsentAs(unique -- Set(a), absent ++ Set(a), l1)
+ else uniqueAbsentAs(unique, absent, l1))
+ }
+ }) ensuring (res => theseAunique1(unique,l) && disjoint(setA(l),absent))
+
+ def allPos(l:List) : Boolean = l match {
+ case Nil() => true
+ case Cons(a,b,c,l1) => 0 <= a && 0 <= b && 0 <= c && allPos(l1)
+ }
+
+ def max(x:Int,y:Int) = if (x <= y) x else y
+
+ def collectA(x:Int,l:List) : (Int,Int,List) = (l match {
+ case Nil() => (0,0,Nil())
+ case Cons(a,b,c,l1) if (a==x) => {
+ val (b2,c2,l2) = collectA(x,l1)
+ (max(b,b2),max(c,c2),l2)
+ }
+ case Cons(a,b,c,l1) if (a!=x) => {
+ val (b2,c2,l2) = collectA(x,l1)
+ (b2,c2,Cons(a,b,c,l2))
+ }
+ }) ensuring (res => {
+ val (b,c,l1) = res
+ !setA(l1).contains(x)
+ })
+
+ def makeUniqueA(x:Int,l:List) : List = {
+ require(allPos(l))
+ val (b,c,l1) = collectA(x,l)
+ Cons(x,b,c,l1)
+ } ensuring(res => theseAunique1(Set(x),res))
+}
diff --git a/testcases/AmortizedQueueStrongSpec.scala b/testcases/AmortizedQueueStrongSpec.scala
new file mode 100644
index 000000000..410be2255
--- /dev/null
+++ b/testcases/AmortizedQueueStrongSpec.scala
@@ -0,0 +1,212 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+object AmortizedQueue {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class AbsQueue
+ case class Queue(front : List, rear : List) extends AbsQueue
+
+ def size(list : List) : Int = (list match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def q2l(queue : AbsQueue) : List = queue match {
+ case Queue(front, rear) => concat(front, reverse(rear))
+ }
+
+ def nth(l:List, n:Int) : Int = {
+ require(0 <= n && n < size(l))
+ l match {
+ case Cons(x,xs) =>
+ if (n==0) x else nth(xs, n-1)
+ }
+ }
+
+ def l2mFrom(k:Int, l:List) : Map[Int,Int] = (l match {
+ case Nil() => Map[Int,Int]()
+ case Cons(x,xs) => l2mFrom(k+1,xs).updated(k,x)
+ })
+
+ def l2m(l:List) : Map[Int,Int] = l2mFrom(0,l)
+
+ def concat(l1 : List, l2 : List) : List = (l1 match {
+ case Nil() => l2
+ case Cons(x,xs) => Cons(x, concat(xs, l2))
+ }) ensuring (res => size(res) == size(l1) + size(l2) && content(res) == content(l1) ++ content(l2))
+
+ def concatTest(l1 : List, l2 : List, i:Int) : List = ({
+ require(0 <= i && i < size(l1) + size(l2))
+ l1 match {
+ case Nil() => l2
+ case Cons(x,xs) => Cons(x,
+ if (i == 0) concat(xs, l2)
+ else concatTest(xs, l2, i-1))
+ }
+ }) ensuring (res => size(res) == size(l1) + size(l2) &&
+ content(res) == content(l1) ++ content(l2) &&
+ nth(res,i) == (if (i < size(l1)) nth(l1,i) else nth(l2,i-size(l1))) &&
+ res == concat(l1,l2))
+
+ def nthConcat(l1:List, l2:List, i:Int) : Boolean = {
+ require(0 <= i && i < size(l1) + size(l2))
+ concatTest(l1, l2, i) == concatTest(l1, l2, i) &&
+ nth(concat(l1,l2), i) == (if (i < size(l1)) nth(l1,i) else nth(l2,i-size(l1)))
+ } holds
+
+ def sameUpto(l1:List, l2:List, k:Int) : Boolean = {
+ require(0 <= k)
+ (l1,l2) match {
+ case (Nil(),Nil()) => true
+ case (Nil(),_) => false
+ case (_,Nil()) => false
+ case (Cons(x,xs),Cons(y,ys)) => {
+ x==y && (if (k==0) true else sameUpto(xs,ys,k-1))
+ }
+ }
+ } ensuring(res => !(size(l1)==k && size(l2)==k && res) || l1==l2)
+
+ @induct
+ def concatAssoc(l1:List, l2:List, l3:List) : Boolean = {
+ concat(l1, concat(l2,l3)) == concat(concat(l1,l2), l3)
+ } holds
+
+ def concatCons(x:Int, l2:List, l3:List) : Boolean = {
+ Cons(x, concat(l2,l3)) == concat(Cons(x,l2), l3)
+ } holds
+
+ def isAmortized(queue : AbsQueue) : Boolean = queue match {
+ case Queue(front, rear) => size(front) >= size(rear)
+ }
+
+ def reverse(l : List) : List = (l match {
+ case Nil() => Nil()
+ case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil()))
+ }) ensuring (res => content(res) == content(l))
+
+ def revConcatNth(l1:List, l2:List, i:Int) : Boolean = {
+ require(0 <= i && i < size(l1)+size(l2))
+ nth(reverse(concat(l1,l2)),i) == nth(concat(reverse(l2), reverse(l1)),i)
+ } holds
+
+ def revrev(l:List) : Boolean = {
+ reverse(reverse(l)) == l
+ } holds
+
+ def amortizedQueue(front : List, rear : List) : AbsQueue = {
+ if (size(rear) <= size(front))
+ Queue(front, rear)
+ else
+ Queue(concat(front, reverse(rear)), Nil())
+ } ensuring(res => isAmortized(res) && q2l(Queue(front, rear)) == q2l(res))
+
+ def isEmpty(queue : AbsQueue) : Boolean = (queue match {
+ case Queue(Nil(), Nil()) => true
+ case _ => false
+ }) ensuring(res => (res == (q2l(queue) == Nil())))
+
+ def enqueue(queue : AbsQueue, elem : Int) : AbsQueue = (queue match {
+ case Queue(front, rear) => amortizedQueue(front, Cons(elem, rear))
+ }) ensuring(res => isAmortized(res) && q2l(res) == concat(q2l(queue), Cons(elem, Nil())))
+ // this did not find a counterexample:
+ // ensuring(res => isAmortized(res) && q2l(res) == Cons(elem, q2l(queue)))
+
+ def push(queue : AbsQueue, elem : Int) : AbsQueue = (queue match {
+ case Queue(front, rear) => amortizedQueue(Cons(elem,front), rear)
+ }) ensuring(res => isAmortized(res) && q2l(res) == Cons(elem, q2l(queue)))
+
+
+ // I did not know why this does not type check
+ def matchQ(queue : AbsQueue) : (Int, AbsQueue) = ({
+ require(isAmortized(queue) && !isEmpty(queue))
+ queue match {
+ case Queue(Cons(f, fs), rear) => (f, amortizedQueue(fs, rear))
+ }
+ }) ensuring(res => {
+ val (f,q) = res
+ q2l(queue) == Cons(f, q2l(q))
+ })
+
+ def tail(queue : AbsQueue) : AbsQueue = ({
+ require(isAmortized(queue) && !isEmpty(queue))
+ queue match {
+ case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear)
+ }
+ }) ensuring(res => isAmortized(res) && (q2l(queue) match {
+ case Nil() => false
+ case Cons(_,xs) => q2l(res)==xs
+ }))
+
+ def front(queue : AbsQueue) : Int = ({
+ require(isAmortized(queue) && !isEmpty(queue))
+ queue match {
+ case Queue(Cons(f, _), _) => f
+ }
+ }) ensuring(res => q2l(queue) match {
+ case Nil() => false
+ case Cons(x,_) => x==res
+ })
+
+ // @induct
+ // def propEnqueue(rear : List, front : List, list : List, elem : Int) : Boolean = {
+ // require(isAmortized(Queue(front, rear)))
+ // val queue = Queue(front, rear)
+ // if (q2l(queue) == list) {
+ // q2l(enqueue(queue, elem)) == concat(list, Cons(elem, Nil()))
+ // } else
+ // true
+ // } holds
+
+ @induct
+ def propFront(queue : AbsQueue, list : List, elem : Int) : Boolean = {
+ require(!isEmpty(queue) && isAmortized(queue))
+ if (q2l(queue) == list) {
+ list match {
+ case Cons(x, _) => front(queue) == x
+ }
+ } else
+ true
+ } holds
+
+ @induct
+ def propTail(rear : List, front : List, list : List, elem : Int) : Boolean = {
+ require(!isEmpty(Queue(front, rear)) && isAmortized(Queue(front, rear)))
+ if (q2l(Queue(front, rear)) == list) {
+ list match {
+ case Cons(_, xs) => q2l(tail(Queue(front, rear))) == xs
+ }
+ } else
+ true
+ } // holds
+
+ def enqueueAndFront(queue : AbsQueue, elem : Int) : Boolean = {
+ if (isEmpty(queue))
+ front(enqueue(queue, elem)) == elem
+ else
+ true
+ } holds
+
+ def enqueueDequeueThrice(queue : AbsQueue, e1 : Int, e2 : Int, e3 : Int) : Boolean = {
+ if (isEmpty(queue)) {
+ val q1 = enqueue(queue, e1)
+ val q2 = enqueue(q1, e2)
+ val q3 = enqueue(q2, e3)
+ val e1prime = front(q3)
+ val q4 = tail(q3)
+ val e2prime = front(q4)
+ val q5 = tail(q4)
+ val e3prime = front(q5)
+ e1 == e1prime && e2 == e2prime && e3 == e3prime
+ } else
+ true
+ } holds
+}
diff --git a/testcases/TreeListSetNoDup.scala b/testcases/TreeListSetNoDup.scala
new file mode 100644
index 000000000..2a208d3d0
--- /dev/null
+++ b/testcases/TreeListSetNoDup.scala
@@ -0,0 +1,100 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+ // list of integers
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ // set of elements from l
+ def l2s(l: List): Set[Int] = l match {
+ case Nil() => Set()
+ case Cons(i, t) => Set(i) ++ l2s(t)
+ }
+
+ // list of t, in order, in from of l0
+ def seqWith(t:Tree,l0:List) : List = (t match {
+ case Leaf() => l0
+ case Node(l, v, r) => seqWith(l,Cons(v,seqWith(r,l0)))
+ }) ensuring (res => l2s(res) == t2s(t) ++ l2s(l0))
+
+ // list of tree t
+ def t2l(t:Tree) : List = seqWith(t,Nil())
+
+ // l has no duplicates, nor elements from s
+ def noDupWith(l:List,s:Set[Int]) : Boolean = l match {
+ case Nil() => true
+ case Cons(h,l1) => !s.contains(h) && noDupWith(l1,Set(h) ++ s)
+ }
+
+ // l has no duplicates
+ def noDup(l:List): Boolean = noDupWith(l,Set.empty[Int])
+
+ // removing duplicates from l1 gives l2
+ def removeDupGives(l1:List,l2:List) : Boolean =
+ l2s(l1)==l2s(l2) && noDup(l2)
+
+ def removeDupAnd(l:List,s0:Set[Int]) : List = (l match {
+ case Nil() => Nil()
+ case Cons(h,l1) => {
+ if (s0.contains(h)) removeDupAnd(l1,s0)
+ else Cons(h,removeDupAnd(l1,Set(h)++s0))
+ }
+ }) ensuring (res => noDupWith(res,s0) && l2s(l) ++ s0 == l2s(res) ++ s0)
+
+ def removeDup(l:List) : List = ({
+ removeDupAnd(l,Set.empty[Int])
+ }) ensuring (res => removeDupGives(l,res))
+
+ def revRemoveDupAnd(l:List,s0:Set[Int],l0:List) : List = ({
+ require(l2s(l0).subsetOf(s0) && noDup(l0))
+ l match {
+ case Nil() => l0
+ case Cons(h,l1) => {
+ if (s0.contains(h)) revRemoveDupAnd(l1,s0,l0)
+ else revRemoveDupAnd(l1,Set(h)++s0,Cons(h,l0))
+ }
+ }
+ }) ensuring (res => noDupWith(res,s0) && l2s(l) ++l2s(l0) ++ s0 == l2s(res) ++ s0)
+
+ def revRemoveDup(l:List) : List = ({
+ revRemoveDupAnd(
+ revRemoveDupAnd(l,Set.empty[Int],Nil()),
+ Set.empty[Int],Nil())
+ }) ensuring (res => removeDupGives(l,res))
+
+ // tree of integers
+ sealed abstract class Tree
+ case class Node(left : Tree, value : Int, right : Tree) extends Tree
+ case class Leaf() extends Tree
+
+ // set of elements from t
+ def t2s(t : Tree): Set[Int] = t match {
+ case Leaf() => Set.empty[Int]
+ case Node(l, v, r) => t2s(l) ++ Set(v) ++ t2s(r)
+ }
+
+ // list of elements of t, in order, without duplicates, in front of l0
+ def seqNoDup(t:Tree,l0:List,s0:Set[Int]) : (List,Set[Int]) = ({
+ require(l2s(l0).subsetOf(s0) && noDup(l0))
+ t match {
+ case Leaf() => (l0,s0)
+ case Node(l, v, r) => {
+ val (rl,rs) = seqNoDup(r,l0,s0)
+ val (l1,s1) = if (rs.contains(v)) (rl,rs) else (Cons(v,rl),Set(v)++rs)
+ seqNoDup(l,l1,s1)
+ }
+ }
+ }) ensuring (res => {
+ val (lres,sres) = res
+ l2s(lres).subsetOf(sres) &&
+ removeDupGives(t2l(t), lres)
+ })
+
+ // list of elements of t, without duplicates
+ def t2lNoDup(t:Tree) : List = ({
+ seqNoDup(t,Nil(),Set.empty[Int])._1
+ }) ensuring (res => removeDupGives(t2l(t), res))
+}
diff --git a/testcases/synthesis/cav2013/AVLTree.scala b/testcases/synthesis/cav2013/AVLTree.scala
new file mode 100644
index 000000000..9e40228e1
--- /dev/null
+++ b/testcases/synthesis/cav2013/AVLTree.scala
@@ -0,0 +1,90 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object AVLTree {
+ sealed abstract class Tree
+ case class Node(left : Tree, value : Int, right : Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def content(t : Tree): Set[Int] = t match {
+ case Leaf() => Set.empty[Int]
+ case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def height(t: Tree): Int = t match {
+ case Leaf() => 0
+ case Node(l, _, r) =>
+ val lh = height(l)
+ val rh = height(r)
+ if (rh > lh) {
+ rh+1
+ } else {
+ lh+1
+ }
+ }
+
+ def isSortedMinMax(t: Tree, min: Int, max: Int): Boolean = t match {
+ case Node(l, v, r) =>
+ isSortedMinMax(l, min, v) &&
+ isSortedMinMax(r, v, max) &&
+ v < max && v > min
+ case _ => true
+ }
+
+ def isSortedMin(t: Tree, min: Int): Boolean = t match {
+ case Node(l, v, r) =>
+ isSortedMinMax(l, min, v) &&
+ isSortedMin(r, v) &&
+ v > min
+ case _ => true
+ }
+
+ def isSortedMax(t: Tree, max: Int): Boolean = t match {
+ case Node(l, v, r) =>
+ isSortedMax(l, v) &&
+ isSortedMinMax(r, v, max) &&
+ v < max
+ case _ => true
+ }
+
+ def isBalanced(t: Tree): Boolean = t match {
+ case Node(l, v, r) =>
+ val diff = height(l)-height(r)
+
+ !(diff > 1 || diff < -1) && isBalanced(l) && isBalanced(r)
+ case Leaf() =>
+ true
+ }
+
+ def isSorted(t: Tree): Boolean = t match {
+ case Node(l, v, r) =>
+ isSortedMin(r, v) &&
+ isSortedMax(l, v)
+ case _ => true
+ }
+
+ def deleteSynth(in : Tree, v : Int) = choose {
+ (out : Tree) => content(out) == (content(in) -- Set(v))
+ }
+
+ def insertSynth(in : Tree, v : Int) = choose {
+ (out : Tree) => content(out) == (content(in) ++ Set(v))
+ }
+
+ def insertBalancedSynth(in: Tree, v: Int) = choose {
+ (out : Tree) => isBalanced(in) && (content(out) == (content(in) ++ Set(v))) && isBalanced(out)
+ }
+
+ def insertSortedSynth(in : Tree, v : Int) = choose {
+ (out : Tree) => isSorted(in) && (content(out) == (content(in) ++ Set(v))) && isSorted(out)
+ }
+
+ def deleteSortedSynth(in : Tree, v : Int) = choose {
+ (out : Tree) => isSorted(in) && (content(out) == (content(in) -- Set(v))) && isSorted(out)
+ }
+
+ def deleteBalancedSynth(in: Tree, v: Int) = choose {
+ (out : Tree) => isBalanced(in) && (content(out) == (content(in) -- Set(v))) && isBalanced(out)
+ }
+}
diff --git a/testcases/synthesis/cav2013/BinaryTree.scala b/testcases/synthesis/cav2013/BinaryTree.scala
new file mode 100644
index 000000000..cbebc3808
--- /dev/null
+++ b/testcases/synthesis/cav2013/BinaryTree.scala
@@ -0,0 +1,61 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+ sealed abstract class Tree
+ case class Node(left : Tree, value : Int, right : Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def content(t : Tree): Set[Int] = t match {
+ case Leaf() => Set.empty[Int]
+ case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def isSortedMinMax(t: Tree, min: Int, max: Int): Boolean = t match {
+ case Node(l, v, r) =>
+ isSortedMinMax(l, min, v) &&
+ isSortedMinMax(r, v, max) &&
+ v < max && v > min
+ case _ => true
+ }
+
+ def isSortedMin(t: Tree, min: Int): Boolean = t match {
+ case Node(l, v, r) =>
+ isSortedMinMax(l, min, v) &&
+ isSortedMin(r, v) &&
+ v > min
+ case _ => true
+ }
+
+ def isSortedMax(t: Tree, max: Int): Boolean = t match {
+ case Node(l, v, r) =>
+ isSortedMax(l, v) &&
+ isSortedMinMax(r, v, max) &&
+ v < max
+ case _ => true
+ }
+
+ def isSorted(t: Tree): Boolean = t match {
+ case Node(l, v, r) =>
+ isSortedMin(r, v) &&
+ isSortedMax(l, v)
+ case _ => true
+ }
+
+ def deleteSynth(in : Tree, v : Int) = choose {
+ (out : Tree) => content(out) == (content(in) -- Set(v))
+ }
+
+ def insertSynth(in : Tree, v : Int) = choose {
+ (out : Tree) => content(out) == (content(in) ++ Set(v))
+ }
+
+ def insertSortedSynth(in : Tree, v : Int) = choose {
+ (out : Tree) => isSorted(in) && (content(out) == (content(in) ++ Set(v))) && isSorted(out)
+ }
+
+ def deleteSortedSynth(in : Tree, v : Int) = choose {
+ (out : Tree) => isSorted(in) && (content(out) == (content(in) -- Set(v))) && isSorted(out)
+ }
+}
diff --git a/testcases/synthesis/cav2013/List.scala b/testcases/synthesis/cav2013/List.scala
new file mode 100644
index 000000000..ce9c60f4e
--- /dev/null
+++ b/testcases/synthesis/cav2013/List.scala
@@ -0,0 +1,64 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ 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 isStrictSorted(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 deleteSynth(in: List, v: Int) = choose {
+ (out: List) => (content(out) == (content(in) -- Set(v)))
+ }
+
+ def deleteSortedSynth(in: List, v: Int) = choose {
+ (out: List) => isSorted(in) && (content(out) == (content(in) -- Set(v))) && isSorted(out)
+ }
+
+ def insertSynth(in: List, v: Int) = choose {
+ (out: List) => (content(out) == (content(in) ++ Set(v)))
+ }
+
+ def insertSortedSynth(in: List, v: Int) = choose {
+ (out: List) => isSorted(in) && (content(out) == (content(in) ++ Set(v))) && isSorted(out)
+ }
+
+ def insertStrictSortedSynth(in: List, v: Int) = choose {
+ (out: List) => isStrictSorted(in) && (content(out) == (content(in) ++ Set(v))) && isStrictSorted(out)
+ }
+
+ def concatSynth(in1: List, in2: List) = choose {
+ (out : List) => content(out) == content(in1) ++ content(in2)
+ }
+
+ def mergeSynth(in1: List, in2: List) = choose {
+ (out : List) => isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+
+ def mergeStrictSynth(in1: List, in2: List) = choose {
+ (out : List) => isStrictSorted(in1) && isStrictSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isStrictSorted(out)
+ }
+
+}
--
GitLab