From 86ac59d3d1ffbe225acc4af1c88d2f92728de307 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Fri, 25 Mar 2011 16:49:32 +0000
Subject: [PATCH] Snapshot for benchmarks from VS competition.
---
sas2011-testcases/AmortizedQueue.scala | 124 +++++++++++++++++++++++
sas2011-testcases/SearchLinkedList.scala | 48 +++++++++
sas2011-testcases/SumAndMax.scala | 46 +++++++++
3 files changed, 218 insertions(+)
create mode 100644 sas2011-testcases/AmortizedQueue.scala
create mode 100644 sas2011-testcases/SearchLinkedList.scala
create mode 100644 sas2011-testcases/SumAndMax.scala
diff --git a/sas2011-testcases/AmortizedQueue.scala b/sas2011-testcases/AmortizedQueue.scala
new file mode 100644
index 000000000..9c049989d
--- /dev/null
+++ b/sas2011-testcases/AmortizedQueue.scala
@@ -0,0 +1,124 @@
+import scala.collection.immutable.Set
+import funcheck.Utils._
+import funcheck.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 asList(queue : AbsQueue) : List = queue match {
+ case Queue(front, rear) => concat(front, reverse(rear))
+ }
+
+ 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 isAmortized(queue : AbsQueue) : Boolean = queue match {
+ case Queue(front, rear) => size(front) >= size(rear)
+ }
+
+ def isEmpty(queue : AbsQueue) : Boolean = queue match {
+ case Queue(Nil(), Nil()) => true
+ case _ => false
+ }
+
+ def reverse(l : List) : List = (l match {
+ case Nil() => Nil()
+ case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil()))
+ }) ensuring (content(_) == content(l))
+
+ def amortizedQueue(front : List, rear : List) : AbsQueue = {
+ if (size(rear) <= size(front))
+ Queue(front, rear)
+ else
+ Queue(concat(front, reverse(rear)), Nil())
+ } ensuring(isAmortized(_))
+
+ def enqueue(queue : AbsQueue, elem : Int) : AbsQueue = (queue match {
+ case Queue(front, rear) => amortizedQueue(front, Cons(elem, rear))
+ }) ensuring(isAmortized(_))
+
+ def tail(queue : AbsQueue) : AbsQueue = {
+ require(isAmortized(queue) && !isEmpty(queue))
+ queue match {
+ case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear)
+ }
+ } ensuring (isAmortized(_))
+
+ def front(queue : AbsQueue) : Int = {
+ require(isAmortized(queue) && !isEmpty(queue))
+ queue match {
+ case Queue(Cons(f, _), _) => f
+ }
+ }
+
+ @induct
+ def propEnqueue(rear : List, front : List, list : List, elem : Int) : Boolean = {
+ require(isAmortized(Queue(front, rear)))
+ val queue = Queue(front, rear)
+ if (asList(queue) == list) {
+ asList(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 (asList(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 (asList(Queue(front, rear)) == list) {
+ list match {
+ case Cons(_, xs) => asList(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/sas2011-testcases/SearchLinkedList.scala b/sas2011-testcases/SearchLinkedList.scala
new file mode 100644
index 000000000..d14b9fee6
--- /dev/null
+++ b/sas2011-testcases/SearchLinkedList.scala
@@ -0,0 +1,48 @@
+import scala.collection.immutable.Set
+import funcheck.Utils._
+import funcheck.Annotations._
+
+object SearchLinkedList {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ def size(list : List) : Int = (list match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contains(list : List, elem : Int) : Boolean = (list match {
+ case Nil() => false
+ case Cons(x, xs) => x == elem || contains(xs, elem)
+ })
+
+ def firstZero(list : List) : Int = (list match {
+ case Nil() => 0
+ case Cons(x, xs) => if (x == 0) 0 else firstZero(xs) + 1
+ }) ensuring (res =>
+ res >= 0 && (if (contains(list, 0)) {
+ firstZeroAtPos(list, res)
+ } else {
+ res == size(list)
+ }))
+
+ def firstZeroAtPos(list : List, pos : Int) : Boolean = {
+ list match {
+ case Nil() => false
+ case Cons(x, xs) => if (pos == 0) x == 0 else x != 0 && firstZeroAtPos(xs, pos - 1)
+ }
+ }
+
+ def goal(list : List, i : Int) : Boolean = {
+ if(firstZero(list) == i) {
+ if(contains(list, 0)) {
+ firstZeroAtPos(list, i)
+ } else {
+ i == size(list)
+ }
+ } else {
+ true
+ }
+ } holds
+}
diff --git a/sas2011-testcases/SumAndMax.scala b/sas2011-testcases/SumAndMax.scala
new file mode 100644
index 000000000..c4265e25b
--- /dev/null
+++ b/sas2011-testcases/SumAndMax.scala
@@ -0,0 +1,46 @@
+import funcheck.Utils._
+import funcheck.Annotations._
+
+object SumAndMax {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ def max(list : List) : Int = {
+ require(list != Nil())
+ list match {
+ case Cons(x, Nil()) => x
+ case Cons(x, xs) => {
+ val m2 = max(xs)
+ if(m2 > x) m2 else x
+ }
+ }
+ }
+
+ def sum(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x, xs) => x + sum(xs)
+ }
+
+ def size(list : List) : Int = (list match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def allPos(list : List) : Boolean = list match {
+ case Nil() => true
+ case Cons(x, xs) => x >= 0 && allPos(xs)
+ }
+
+ def prop0(list : List) : Boolean = {
+ require(list != Nil())
+ !allPos(list) || max(list) >= 0
+ } holds
+
+ @induct
+ def property(list : List) : Boolean = {
+ // This precondition was given in the problem but isn't actually useful :D
+ // require(allPos(list))
+ sum(list) <= size(list) * (if(list == Nil()) 0 else max(list))
+ } holds
+}
--
GitLab