From 738383f7381f5e086d7e046d44bf20147d0af326 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:27:47 +0000
Subject: [PATCH] avoid the crash, but cannot prove tail and enqueue specs
---
vstte10competition/AmortizedQueue.scala | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/vstte10competition/AmortizedQueue.scala b/vstte10competition/AmortizedQueue.scala
index 7968b415e..9c049989d 100644
--- a/vstte10competition/AmortizedQueue.scala
+++ b/vstte10competition/AmortizedQueue.scala
@@ -92,10 +92,9 @@ object AmortizedQueue {
@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) {
+ if (asList(Queue(front, rear)) == list) {
list match {
- case Cons(_, xs) => asList(tail(queue)) == xs
+ case Cons(_, xs) => asList(tail(Queue(front, rear))) == xs
}
} else
true
--
GitLab