summaryrefslogtreecommitdiff
path: root/Test/dafny1
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny1')
-rw-r--r--Test/dafny1/ExtensibleArray.dfy9
-rw-r--r--Test/dafny1/PriorityQueue.dfy6
-rw-r--r--Test/dafny1/UnboundedStack.dfy3
3 files changed, 7 insertions, 11 deletions
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index b790eea5..4ceca552 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -39,7 +39,7 @@ class ExtensibleArray<T> {
ensures Valid() && fresh(Repr - {this});
ensures Contents == [];
{
- var arr := new T[256]; elements := arr;
+ elements := new T[256];
more := null;
length := 0;
M := 0;
@@ -90,15 +90,14 @@ class ExtensibleArray<T> {
elements[length - M] := t;
} else {
if (more == null) {
- var mr := new ExtensibleArray<array<T>>.Init();
- more := mr;
- Repr := Repr + {mr} + mr.Repr;
+ more := new ExtensibleArray<array<T>>.Init();
+ Repr := Repr + {more} + more.Repr;
}
// "elements" is full, so move it into "more" and allocate a new array
call more.Append(elements);
Repr := Repr + more.Repr;
M := M + 256;
- var arr := new T[256]; elements := arr;
+ elements := new T[256];
Repr := Repr + {elements};
elements[0] := t;
}
diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 957eb7cb..db1c60fa 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -27,8 +27,7 @@ class PriorityQueue {
ensures N == capacity;
{
N := capacity;
- var arr := new int[N+1];
- a := arr;
+ a := new int[N+1];
n := 0;
Repr := {this};
Repr := Repr + {a};
@@ -143,8 +142,7 @@ class PriorityQueue_Alternative {
ensures N == capacity;
{
N := capacity;
- var arr := new int[N+1];
- a := arr;
+ a := new int[N+1];
n := 0;
Repr := {this};
Repr := Repr + {a};
diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy
index 940e1a0a..dfc10327 100644
--- a/Test/dafny1/UnboundedStack.dfy
+++ b/Test/dafny1/UnboundedStack.dfy
@@ -31,8 +31,7 @@ class UnboundedStack<T> {
ensures IsUnboundedStack();
ensures content == [val] + old(content);
{
- var tmp := new Node<T>.InitNode(val,top);
- top := tmp;
+ top := new Node<T>.InitNode(val,top);
representation := representation + top.footprint;
content := [val] + content;
}