From aa1c6a512520f06a24221aefb8c50f803625300c 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:12:22 +0000
Subject: [PATCH] Trying to prove properties with list abstraction but have
another problem with z3 translation
---
vstte10competition/AmortizedQueue.scala | 37 +++++++++++++++++++++++++
1 file changed, 37 insertions(+)
diff --git a/vstte10competition/AmortizedQueue.scala b/vstte10competition/AmortizedQueue.scala
index 055e7042c..7968b415e 100644
--- a/vstte10competition/AmortizedQueue.scala
+++ b/vstte10competition/AmortizedQueue.scala
@@ -19,6 +19,10 @@ object AmortizedQueue {
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
@@ -64,6 +68,39 @@ object AmortizedQueue {
}
}
+ @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)))
+ val queue = Queue(front, rear)
+ if (asList(queue) == list) {
+ list match {
+ case Cons(_, xs) => asList(tail(queue)) == xs
+ }
+ } else
+ true
+ } // holds
+
def enqueueAndFront(queue : AbsQueue, elem : Int) : Boolean = {
if (isEmpty(queue))
front(enqueue(queue, elem)) == elem
--
GitLab