From 541df399329df8966f4b11ec611f93082f61ebe9 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 24 Mar 2011 22:27:53 +0000
Subject: [PATCH]
---
vstte10competition/AmortizedQueue.scala | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/vstte10competition/AmortizedQueue.scala b/vstte10competition/AmortizedQueue.scala
index 9cb270f61..055e7042c 100644
--- a/vstte10competition/AmortizedQueue.scala
+++ b/vstte10competition/AmortizedQueue.scala
@@ -46,9 +46,9 @@ object AmortizedQueue {
Queue(concat(front, reverse(rear)), Nil())
} ensuring(isAmortized(_))
- def enqueue(queue : AbsQueue, elem : Int) : AbsQueue = queue match {
+ 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))
@@ -85,5 +85,4 @@ object AmortizedQueue {
} else
true
} holds
-
}
--
GitLab