diff --git a/vstte10competition/AmortizedQueue.scala b/vstte10competition/AmortizedQueue.scala index 9cb270f61be1f680742dd070ff232f811b46390d..055e7042cb6be157a6b7cc5a9266a35b8f8f2ca4 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 - }