summaryrefslogtreecommitdiff
path: root/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/VSComp2010/Problem5-DoubleEndedQueue.dfy')
-rw-r--r--Test/VSComp2010/Problem5-DoubleEndedQueue.dfy12
1 files changed, 4 insertions, 8 deletions
diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
index cf109c1a..df8cb1b7 100644
--- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
+++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
@@ -30,10 +30,8 @@ class AmortizedQueue<T> {
modifies this;
ensures Valid() && List == [];
{
- var tmp := new LinkedList<T>.Init();
- front := tmp;
- tmp := new LinkedList<T>.Init();
- rear := tmp;
+ front := new LinkedList<T>.Init();
+ rear := new LinkedList<T>.Init();
Repr := {this};
Repr := Repr + front.Repr + rear.Repr;
List := [];
@@ -52,8 +50,7 @@ class AmortizedQueue<T> {
call ff := f.Concat(rr);
front := ff;
- var tmp := new LinkedList<T>.Init();
- rear := tmp;
+ rear := new LinkedList<T>.Init();
}
Repr := {this};
Repr := Repr + front.Repr + rear.Repr;
@@ -79,8 +76,7 @@ class AmortizedQueue<T> {
ensures r != null && r.Valid() && r.List == List + [item];
{
call rr := rear.Cons(item);
- var tmp := new AmortizedQueue<T>.InitFromPieces(front, rr);
- r := tmp;
+ r := new AmortizedQueue<T>.InitFromPieces(front, rr);
}
}