summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/VSI-Benchmarks/b3.dfy3
-rw-r--r--Test/VSI-Benchmarks/b4.dfy3
-rw-r--r--Test/VSI-Benchmarks/b5.dfy4
-rw-r--r--Test/VSI-Benchmarks/b6.dfy2
-rw-r--r--Test/VSI-Benchmarks/b7.dfy3
-rw-r--r--Test/VSI-Benchmarks/b8.dfy8
-rw-r--r--Test/dafny0/BinaryTree.dfy9
-rw-r--r--Test/dafny0/Queue.dfy4
-rw-r--r--Test/dafny0/Termination.dfy1
-rw-r--r--Test/dafny0/TypeParameters.dfy1
10 files changed, 1 insertions, 37 deletions
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index a11dec52..4f717f48 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -94,7 +94,6 @@ class Benchmark3 {
decreases |q.contents|;
{
- var m,k;
call m,k := RemoveMin(q);
perm := perm + [p[k]]; //adds index of min to perm
p := p[k+1..]+ p[..k]; //remove index of min from p
@@ -126,7 +125,6 @@ class Benchmark3 {
invariant (forall i ::0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far
decreases n-j;
{
- var x;
call x:= q.Dequeue();
call q.Enqueue(x);
if ( x < m) {k := j; m := x;}
@@ -140,7 +138,6 @@ class Benchmark3 {
invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j];
decreases k-j;
{
- var x;
call x := q.Dequeue();
call q.Enqueue(x);
j:= j +1;
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index ac58b7d1..5a9d46c8 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -30,7 +30,6 @@ class Map<Key,Value> {
ensures present ==> (exists i :: 0 <= i && i < |keys| &&
keys[i] == key && values[i] == val);
{
- var j;
call j := FindIndex(key);
if (j == -1) {
present := false;
@@ -55,7 +54,6 @@ class Map<Key,Value> {
ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>
values[i] == old(values)[i]);
{
- var j;
call j := FindIndex(key);
if (j == -1) {
keys := keys + [key];
@@ -88,7 +86,6 @@ class Map<Key,Value> {
keys[h..] == old(keys)[h+1..] &&
values[h..] == old(values)[h+1..]);
{
- var j;
call j := FindIndex(key);
if (0 <= j) {
keys := keys[..j] + keys[j+1..];
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index 9d384c38..8026e60f 100644
--- a/Test/VSI-Benchmarks/b5.dfy
+++ b/Test/VSI-Benchmarks/b5.dfy
@@ -99,7 +99,6 @@ class Queue<T> {
ensures Valid() && fresh(footprint - old(footprint));
ensures contents == old(contents)[1..] + old(contents)[..1];
{
- var t: T;
call t := Front();
call Dequeue();
call Enqueue(t);
@@ -113,7 +112,6 @@ class Queue<T> {
ensures (exists i :: 0 <= i && i <= |contents| &&
contents == old(contents)[i..] + old(contents)[..i]);
{
- var t: T;
call t := Front();
call Dequeue();
call Enqueue(t);
@@ -163,7 +161,6 @@ class Main<U> {
assert |q0.contents| == 2;
- var w;
call w := q0.Front();
assert w == t;
call q0.Dequeue();
@@ -191,7 +188,6 @@ class Main<U> {
assert |q0.contents| == 2;
- var w;
call w := q0.Front();
assert w == t;
call q0.Dequeue();
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index f6e7879f..48306e9b 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -114,7 +114,7 @@ class Client
call c.Add(45);
call c.Add(78);
- var iter,b,x, s:= [ ];
+ var s:= [ ];
call iter:=c.GetIterator();
call b:= iter.MoveNext();
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index 95267823..f7d51058 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -129,12 +129,10 @@ class Client {
call rd.Open();
var q:= new Queue<int>;
- var ch;
while (true)
invariant rd.Valid() && fresh(rd.footprint) && fresh(q);
decreases |rd.stream|;
{
- var eos:bool;
call eos := rd.AtEndOfStream();
if (eos)
{
@@ -146,7 +144,6 @@ class Client {
}
call rd.Close();
- var perm;
call q,perm := Sort(q);
var wr:= new Stream;
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 643609d0..51172419 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -61,7 +61,6 @@ class Glossary {
// ** invariant q.contents == glossary.keys; need a quantifer to express this (map doesnt necessarily add to end)
// we leave out the decreases clause - unbounded stream
{
- var term,definition;
call term,definition := readDefinition(rs);
if (term == null)
{
@@ -72,7 +71,6 @@ class Glossary {
}
call rs.Close();
- var p;
call q,p := Sort(q);
var wr := new WriterStream;
call wr.Create();
@@ -84,7 +82,6 @@ class Glossary {
invariant q !in wr.footprint;
decreases |q.contents|;
{
- var term, present, definition;
call term:= q.Dequeue();
call present,definition:= glossary.Find(term);
assume present; // to change this into an assert we need the loop invariant ** above that we commented out
@@ -103,7 +100,6 @@ class Glossary {
decreases |definition| -i;
{
var w := definition[i];
- var d;
assume w != null; // to convert this into an assert we need invariant *** above
call present, d := glossary.Find(w);
if (present)
@@ -135,7 +131,6 @@ class Glossary {
invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint));
invariant null !in definition;
{
- var w;
call w := rs.GetWord();
if (w == null)
{
@@ -275,7 +270,6 @@ class Map<Key,Value> {
ensures present ==> (exists i :: 0 <= i && i < |keys| &&
keys[i] == key && values[i] == val);
{
- var j;
call j := FindIndex(key);
if (j == -1) {
present := false;
@@ -300,7 +294,6 @@ class Map<Key,Value> {
ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>
values[i] == old(values)[i]);
{
- var j;
call j := FindIndex(key);
if (j == -1) {
keys := keys + [key];
@@ -333,7 +326,6 @@ class Map<Key,Value> {
keys[h..] == old(keys)[h+1..] &&
values[h..] == old(values)[h+1..]);
{
- var j;
call j := FindIndex(key);
if (0 <= j) {
keys := keys[..j] + keys[j+1..];
diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 7a5fb3c7..138a22df 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -42,7 +42,6 @@ class IntSet {
ensures Valid() && fresh(footprint - old(footprint));
ensures contents == old(contents) + {x};
{
- var t;
call t := InsertHelper(x, root);
root := t;
contents := root.contents;
@@ -64,12 +63,10 @@ class IntSet {
m := n;
} else {
if (x < n.data) {
- var t;
call t := InsertHelper(x, n.left);
n.left := t;
n.footprint := n.footprint + n.left.footprint;
} else {
- var t;
call t := InsertHelper(x, n.right);
n.right := t;
n.footprint := n.footprint + n.right.footprint;
@@ -86,7 +83,6 @@ class IntSet {
ensures contents == old(contents) - {x};
{
if (root != null) {
- var newRoot;
call newRoot := root.Remove(x);
root := newRoot;
if (root == null) {
@@ -169,13 +165,11 @@ class Node {
{
node := this;
if (left != null && x < data) {
- var t;
call t := left.Remove(x);
left := t;
contents := contents - {x};
if (left != null) { footprint := footprint + left.footprint; }
} else if (right != null && data < x) {
- var t;
call t := right.Remove(x);
right := t;
contents := contents - {x};
@@ -189,7 +183,6 @@ class Node {
node := left;
} else {
// rotate
- var min, r;
call min, r := right.RemoveMin();
data := min; right := r;
contents := contents - {x};
@@ -211,7 +204,6 @@ class Node {
min := data;
node := right;
} else {
- var t;
call min, t := left.RemoveMin();
left := t;
node := this;
@@ -229,7 +221,6 @@ class Main {
call s.Insert(12);
call s.Insert(24);
- var present;
call present := s.Find(x);
assert present <==> x == 12 || x == 24;
}
diff --git a/Test/dafny0/Queue.dfy b/Test/dafny0/Queue.dfy
index ab83a75d..5c22ec92 100644
--- a/Test/dafny0/Queue.dfy
+++ b/Test/dafny0/Queue.dfy
@@ -49,7 +49,6 @@ class Queue<T> {
ensures Valid() && fresh(footprint - old(footprint));
ensures contents == old(contents)[1..] + old(contents)[..1];
{
- var t: T;
call t := Front();
call Dequeue();
call Enqueue(t);
@@ -63,7 +62,6 @@ class Queue<T> {
ensures (exists i :: 0 <= i && i <= |contents| &&
contents == old(contents)[i..] + old(contents)[..i]);
{
- var t: T;
call t := Front();
call Dequeue();
call Enqueue(t);
@@ -163,7 +161,6 @@ class Main<U> {
assert |q0.contents| == 2;
- var w;
call w := q0.Front();
assert w == t;
call q0.Dequeue();
@@ -191,7 +188,6 @@ class Main<U> {
assert |q0.contents| == 2;
- var w;
call w := q0.Front();
assert w == t;
call q0.Dequeue();
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 43fe63df..ee9d9613 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -28,7 +28,6 @@ class Termination {
}
method Lex() {
- var x: int, y: int;
call x := Update();
call y := Update();
while (!(x == 0 && y == 0))
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index a5764be5..3f57f369 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -13,7 +13,6 @@ class C<U> {
method Main(u: U)
{
var t := F(3,u) && F(this,u);
- var kz;
call kz := M(t,u);
assert kz && (G() || !G());
}
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-28 17:21:26 +0000