From e814ee4888208bec030c7c1beffb27586f99e151 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Thu, 25 Nov 2010 09:34:42 +0000
Subject: [PATCH] examples
---
pldi2011-testcases/AssociativeList.scala | 2 +-
pldi2011-testcases/InsertionSort.scala | 13 ++++++
pldi2011-testcases/PropositionalLogic.scala | 10 ++--
pldi2011-testcases/RedBlackTree.scala | 6 +++
testcases/ListWithSize.scala | 51 +++++++++++----------
5 files changed, 51 insertions(+), 31 deletions(-)
diff --git a/pldi2011-testcases/AssociativeList.scala b/pldi2011-testcases/AssociativeList.scala
index 551d40450..ed18a6bba 100644
--- a/pldi2011-testcases/AssociativeList.scala
+++ b/pldi2011-testcases/AssociativeList.scala
@@ -37,7 +37,7 @@ object AssociativeList {
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) updateElem(xs, e) else Cons(KeyValuePair(k, v), updateElem(xs, e))
+ 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)
diff --git a/pldi2011-testcases/InsertionSort.scala b/pldi2011-testcases/InsertionSort.scala
index 339fc28ff..7d5e0eb62 100644
--- a/pldi2011-testcases/InsertionSort.scala
+++ b/pldi2011-testcases/InsertionSort.scala
@@ -67,6 +67,19 @@ object InsertionSort {
&& 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 {
diff --git a/pldi2011-testcases/PropositionalLogic.scala b/pldi2011-testcases/PropositionalLogic.scala
index 5c35713af..dbdf6e3ee 100644
--- a/pldi2011-testcases/PropositionalLogic.scala
+++ b/pldi2011-testcases/PropositionalLogic.scala
@@ -48,18 +48,18 @@ object PropositionalLogic {
case Literal(_) => true
}
- def freeVars(f: Formula): Set[Int] = {
+ def vars(f: Formula): Set[Int] = {
require(isNNF(f))
f match {
- case And(lhs, rhs) => freeVars(lhs) ++ freeVars(rhs)
- case Or(lhs, rhs) => freeVars(lhs) ++ freeVars(rhs)
- case Implies(lhs, rhs) => freeVars(lhs) ++ freeVars(rhs)
+ 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) = { freeVars(nnf(f)) }
+ def fv(f : Formula) = { vars(nnf(f)) }
@induct
def wrongCommutative(f: Formula) : Boolean = {
diff --git a/pldi2011-testcases/RedBlackTree.scala b/pldi2011-testcases/RedBlackTree.scala
index b2f6bb691..ed076c091 100644
--- a/pldi2011-testcases/RedBlackTree.scala
+++ b/pldi2011-testcases/RedBlackTree.scala
@@ -65,6 +65,12 @@ object RedBlackTree {
makeBlack(ins(x, t))
} ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+ def buggyAdd(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ // makeBlack(ins(x, t))
+ ins(x, t)
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
require(
Node(c,a,x,b) match {
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index 08f93d8b4..df2522cb8 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -7,12 +7,37 @@ object ListWithSize {
case class Cons(head: Int, tail: List) extends List
case class Nil() extends List
+ sealed abstract class IntPairList
+ case class IPCons(head: IntPair, tail: IntPairList) extends IntPairList
+ case class IPNil() extends IntPairList
+
+ sealed abstract class IntPair
+ case class IP(fst: Int, snd: Int) extends IntPair
+
// proved with unrolling=0
def size(l: List) : Int = (l match {
case Nil() => 0
case Cons(_, t) => 1 + size(t)
}) ensuring(_ >= 0)
+ def iplSize(l: IntPairList) : Int = (l match {
+ case IPNil() => 0
+ case IPCons(_, xs) => 1 + iplSize(xs)
+ }) ensuring(_ >= 0)
+
+ def zip(l1: List, l2: List) : IntPairList = {
+ // try to comment this and see how pattern-matching becomes
+ // non-exhaustive and post-condition fails
+ require(size(l1) == size(l2))
+
+ l1 match {
+ case Nil() => IPNil()
+ case Cons(x, xs) => l2 match {
+ case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys))
+ }
+ }
+ } ensuring(iplSize(_) == size(l1))
+
def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
def sizeTailRecAcc(l: List, acc: Int) : Int = {
require(acc >= 0)
@@ -34,7 +59,7 @@ object ListWithSize {
def sizeAndContent(l: List) : Boolean = {
size(l) == 0 || content(l) != Set.empty[Int]
} holds
-
+
def drunk(l : List) : List = (l match {
case Nil() => Nil()
case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
@@ -53,30 +78,6 @@ object ListWithSize {
case Cons(x, xs) => reverse0(xs, Cons(x, l2))
}) ensuring(content(_) == content(l1) ++ content(l2))
-
-
- /*** revAppend cannot use appendAssoc ***/
- /*
- @induct
- def revSimple(l: List) : List = (l match {
- case Nil() => Nil()
- case Cons(x, xs) => append(revSimple(xs), Cons(x, Nil()))
- }) ensuring(content(_) == content(l))
-
- @induct
- def revAppend(l1: List, l2: List) : Boolean = {
- require(l1 match {
- case Nil() => true
- case Cons(x, xs) => appendAssoc(revSimple(l2), revSimple(xs), Cons(x, Nil()))
- })
- revSimple(append(l1, l2)) == append(revSimple(l2), revSimple(l1))
- } holds
-
- @induct
- def reverseTwice(l: List): Boolean =
- (revSimple(revSimple(l)) == l) holds */
- /***************************************/
-
def append(l1 : List, l2 : List) : List = (l1 match {
case Nil() => l2
case Cons(x,xs) => Cons(x, append(xs, l2))
--
GitLab