diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-26 00:02:57 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-26 00:02:57 -0700 |
| commit | a7731599b7ab802c7c47e5ccf33e21953a238c2d (patch) | |
| tree | af68f595ddddfc2195487f90754080635038fe24 /Test | |
| parent | daba6b774c3f945de58229f28078e8dccaaec782 (diff) | |
Dafny: retired the "call" keyword
Diffstat (limited to 'Test')
43 files changed, 348 insertions, 343 deletions
diff --git a/Test/VSComp2010/Problem1-SumMax.dfy b/Test/VSComp2010/Problem1-SumMax.dfy index 1b105ac1..3db9bf72 100644 --- a/Test/VSComp2010/Problem1-SumMax.dfy +++ b/Test/VSComp2010/Problem1-SumMax.dfy @@ -38,6 +38,6 @@ method Main() a[7] := 1;
a[8] := 10;
a[9] := 6;
- call s, m := M(10, a);
+ var s, m := M(10, a);
print "N = ", a.Length, " sum = ", s, " max = ", m, "\n";
}
diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy index bf6aca37..2a262d70 100644 --- a/Test/VSComp2010/Problem2-Invert.dfy +++ b/Test/VSComp2010/Problem2-Invert.dfy @@ -61,11 +61,11 @@ method Main() a[8] := 5;
a[9] := 6;
var b := new int[10];
- call M(10, a, b);
+ M(10, a, b);
print "a:\n";
- call PrintArray(a);
+ PrintArray(a);
print "b:\n";
- call PrintArray(b);
+ PrintArray(b);
}
method PrintArray(a: array<int>)
diff --git a/Test/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy index 03e6bdfe..3d24255d 100644 --- a/Test/VSComp2010/Problem3-FindZero.dfy +++ b/Test/VSComp2010/Problem3-FindZero.dfy @@ -82,11 +82,11 @@ static method Search(ll: Node) returns (r: int) method Main()
{
var list: Node := null;
- call list := list.Cons(0, list);
- call list := list.Cons(5, list);
- call list := list.Cons(0, list);
- call list := list.Cons(8, list);
- call r := Search(list);
+ list := list.Cons(0, list);
+ list := list.Cons(5, list);
+ list := list.Cons(0, list);
+ list := list.Cons(8, list);
+ var r := Search(list);
print "Search returns ", r, "\n";
assert r == 1;
}
diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy index ef084674..2f21b7a1 100644 --- a/Test/VSComp2010/Problem4-Queens.dfy +++ b/Test/VSComp2010/Problem4-Queens.dfy @@ -39,7 +39,7 @@ method Search(N: int) returns (success: bool, board: seq<int>) ==>
(exists p :: 0 <= p && p < N && !IsConsistent(B, p)));
{
- call success, board := SearchAux(N, []);
+ success, board := SearchAux(N, []);
}
// Given a board, this function says whether or not the queen placed in column 'pos'
@@ -110,7 +110,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard: // Thus, we meet the precondition of 'SearchAux' on 'candidateBoard', so let's search
// for a solution that extends 'candidateBoard'.
- call s, b := SearchAux(N, candidateBoard);
+ var s, b := SearchAux(N, candidateBoard);
if (s) {
// The recursive call to 'SearchAux' found consistent positions for all remaining columns
newBoard := b;
@@ -137,11 +137,11 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard: method Main()
{
- call s, b := Search(2);
+ var s, b := Search(2);
print "N=2 returns ", s, "\n";
- call s, b := Search(4);
+ s, b := Search(4);
print "N=4 returns ", s, "\n";
- call PrintSeq(b);
+ PrintSeq(b);
}
method PrintSeq(b: seq<int>)
diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy index df8cb1b7..0e141927 100644 --- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy +++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy @@ -46,8 +46,8 @@ class AmortizedQueue<T> { front := f;
rear := r;
} else {
- call rr := r.Reverse();
- call ff := f.Concat(rr);
+ var rr := r.Reverse();
+ var ff := f.Concat(rr);
front := ff;
rear := new LinkedList<T>.Init();
@@ -75,7 +75,7 @@ class AmortizedQueue<T> { requires Valid();
ensures r != null && r.Valid() && r.List == List + [item];
{
- call rr := rear.Cons(item);
+ var rr := rear.Cons(item);
r := new AmortizedQueue<T>.InitFromPieces(front, rr);
}
}
@@ -133,8 +133,8 @@ class LinkedList<T> { if (length == 0) {
r := end;
} else {
- call c := tail.Concat(end);
- call r := c.Cons(head);
+ var c := tail.Concat(end);
+ r := c.Cons(head);
}
}
@@ -148,10 +148,10 @@ class LinkedList<T> { if (length == 0) {
r := this;
} else {
- call r := tail.Reverse();
+ r := tail.Reverse();
var e := new LinkedList<T>.Init();
- call e := e.Cons(head);
- call r := r.Concat(e);
+ e := e.Cons(head);
+ r := r.Concat(e);
}
}
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy index cd4a18c2..3bd2bf43 100644 --- a/Test/VSI-Benchmarks/b1.dfy +++ b/Test/VSI-Benchmarks/b1.dfy @@ -35,37 +35,37 @@ method Mul(x: int, y: int) returns (r: int) if (x == 0) {
r := 0;
} else if (x < 0) {
- call r := Mul(-x, y);
+ r := Mul(-x, y);
r := -r;
} else {
- call r := Mul(x-1, y);
- call r := Add(r, y);
+ r := Mul(x-1, y);
+ r := Add(r, y);
}
}
// ---------------------------
method Main() {
- call TestAdd(3, 180);
- call TestAdd(3, -180);
- call TestAdd(0, 1);
+ TestAdd(3, 180);
+ TestAdd(3, -180);
+ TestAdd(0, 1);
- call TestMul(3, 180);
- call TestMul(3, -180);
- call TestMul(180, 3);
- call TestMul(-180, 3);
- call TestMul(0, 1);
- call TestMul(1, 0);
+ TestMul(3, 180);
+ TestMul(3, -180);
+ TestMul(180, 3);
+ TestMul(-180, 3);
+ TestMul(0, 1);
+ TestMul(1, 0);
}
method TestAdd(x: int, y: int) {
print x, " + ", y, " = ";
- call z := Add(x, y);
+ var z := Add(x, y);
print z, "\n";
}
method TestMul(x: int, y: int) {
print x, " * ", y, " = ";
- call z := Mul(x, y);
+ var z := Mul(x, y);
print z, "\n";
}
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index 6c6f11b3..3046621b 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -38,13 +38,13 @@ method Main() { a[2] := -2;
a[3] := 0;
a[4] := 25;
- call TestSearch(a, 4);
- call TestSearch(a, -8);
- call TestSearch(a, -2);
- call TestSearch(a, 0);
- call TestSearch(a, 23);
- call TestSearch(a, 25);
- call TestSearch(a, 27);
+ TestSearch(a, 4);
+ TestSearch(a, -8);
+ TestSearch(a, -2);
+ TestSearch(a, 0);
+ TestSearch(a, 23);
+ TestSearch(a, 25);
+ TestSearch(a, 27);
}
method TestSearch(a: array<int>, key: int)
@@ -52,6 +52,6 @@ method TestSearch(a: array<int>, key: int) requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]);
{
var b := new Benchmark2;
- call r := b.BinarySearch(a, key);
+ var r := b.BinarySearch(a, key);
print "Looking for key=", key, ", result=", r, "\n";
}
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 3f30c4b5..3de94555 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -87,10 +87,10 @@ class Benchmark3 { invariant (forall i :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
invariant (forall i :: 0 <= i && i < |p| ==> q.contents[i] == old(q.contents)[p[i]]);
{
- call m,k := RemoveMin(q);
+ var 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
- call r.Enqueue(m);
+ r.Enqueue(m);
pperm := pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] + [pperm[k]];
}
}
@@ -116,8 +116,8 @@ class Benchmark3 { invariant 0 <= k && k < |old(q.contents)| && old(q.contents)[k] == m;
invariant (forall i :: 0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far
{
- call x:= q.Dequeue();
- call q.Enqueue(x);
+ var x := q.Dequeue();
+ q.Enqueue(x);
if (x < m) { k := j; m := x; }
j := j+1;
}
@@ -127,11 +127,11 @@ class Benchmark3 { invariant j <= k;
invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j];
{
- call x := q.Dequeue();
- call q.Enqueue(x);
+ var x := q.Dequeue();
+ q.Enqueue(x);
j := j+1;
}
- call m:= q.Dequeue();
+ m := q.Dequeue();
}
}
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index 9f7e272e..b70ff4d0 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -54,7 +54,7 @@ class Map<Key,Value> { ensures !present ==> key !in Keys;
ensures present ==> (exists i :: 0 <= i && i < |Keys| && Keys[i] == key && Values[i] == val);
{
- call p, n, prev := FindIndex(key);
+ var p, n, prev := FindIndex(key);
if (p == null) {
present := false;
} else {
@@ -74,7 +74,7 @@ class Map<Key,Value> { Keys[j] == old(Keys)[j] && Values[j] == old(Values)[j]));
ensures key !in old(Keys) ==> Keys == [key] + old(Keys) && Values == [val] + old(Values);
{
- call p, n, prev := FindIndex(key);
+ var p, n, prev := FindIndex(key);
if (p == null) {
var h := new Node<Key,Value>;
h.key := key; h.val := val; h.next := head;
@@ -107,7 +107,7 @@ class Map<Key,Value> { Keys[h..] == old(Keys)[h+1..] &&
Values[h..] == old(Values)[h+1..]);
{
- call p, n, prev := FindIndex(key);
+ var p, n, prev := FindIndex(key);
if (p != null) {
Keys := Keys[..n] + Keys[n+1..];
Values := Values[..n] + Values[n+1..];
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy index d9bd36f5..cd132ef3 100644 --- a/Test/VSI-Benchmarks/b5.dfy +++ b/Test/VSI-Benchmarks/b5.dfy @@ -98,9 +98,9 @@ class Queue<T> { ensures Valid() && fresh(footprint - old(footprint));
ensures contents == old(contents)[1..] + old(contents)[..1];
{
- call t := Front();
- call Dequeue();
- call Enqueue(t);
+ var t := Front();
+ Dequeue();
+ Enqueue(t);
}
method RotateAny()
@@ -112,9 +112,9 @@ class Queue<T> { ensures (exists i :: 0 <= i && i <= |contents| &&
contents == old(contents)[i..] + old(contents)[..i]);
{
- call t := Front();
- call Dequeue();
- call Enqueue(t);
+ var t := Front();
+ Dequeue();
+ Enqueue(t);
}
}
@@ -152,18 +152,18 @@ class Main<U> { var q0 := new Queue<T>.Init();
var q1 := new Queue<T>.Init();
- call q0.Enqueue(t);
- call q0.Enqueue(u);
+ q0.Enqueue(t);
+ q0.Enqueue(u);
- call q1.Enqueue(v);
+ q1.Enqueue(v);
assert |q0.contents| == 2;
- call w := q0.Front();
+ var w := q0.Front();
assert w == t;
- call q0.Dequeue();
+ q0.Dequeue();
- call w := q0.Front();
+ w := q0.Front();
assert w == u;
assert |q0.contents| == 1;
@@ -179,18 +179,18 @@ class Main<U> { ensures fresh(q0.footprint - old(q0.footprint));
ensures fresh(q1.footprint - old(q1.footprint));
{
- call q0.Enqueue(t);
- call q0.Enqueue(u);
+ q0.Enqueue(t);
+ q0.Enqueue(u);
- call q1.Enqueue(v);
+ q1.Enqueue(v);
assert |q0.contents| == 2;
- call w := q0.Front();
+ var w := q0.Front();
assert w == t;
- call q0.Dequeue();
+ q0.Dequeue();
- call w := q0.Front();
+ w := q0.Front();
assert w == u;
assert |q0.contents| == 1;
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy index 13086f28..fda9ca74 100644 --- a/Test/VSI-Benchmarks/b6.dfy +++ b/Test/VSI-Benchmarks/b6.dfy @@ -107,14 +107,14 @@ class Client method Main()
{
var c := new Collection<int>.Init();
- call c.Add(33);
- call c.Add(45);
- call c.Add(78);
+ c.Add(33);
+ c.Add(45);
+ c.Add(78);
var s := [];
- call iter := c.GetIterator();
- call b := iter.MoveNext();
+ var iter := c.GetIterator();
+ var b := iter.MoveNext();
while (b)
invariant iter.Valid() && b == iter.HasCurrent() && fresh(iter.footprint);
@@ -123,13 +123,13 @@ class Client invariant iter.c == c;
decreases |c.elements| - iter.pos;
{
- call x := iter.GetCurrent();
+ var x := iter.GetCurrent();
s := s + [x];
- call b := iter.MoveNext();
+ b := iter.MoveNext();
}
assert s == c.elements; //verifies that the iterator returns the correct things
- call c.Add(100);
+ c.Add(100);
}
}
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index 2304e602..f34f5c00 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -119,33 +119,34 @@ class Client { method Main()
{
var rd := new Stream;
- call rd.Open();
+ rd.Open();
var q := new Queue<int>;
while (true)
invariant rd.Valid() && fresh(rd.footprint) && fresh(q);
decreases |rd.stream|;
{
- call eos := rd.AtEndOfStream();
+ var eos := rd.AtEndOfStream();
if (eos) {
break;
}
- call ch := rd.GetChar();
- call q.Enqueue(ch);
+ var ch := rd.GetChar();
+ q.Enqueue(ch);
}
- call rd.Close();
- call q,perm := Sort(q);
+ rd.Close();
+ var perm;
+ q,perm := Sort(q);
- var wr:= new Stream;
- call wr.Create();
+ var wr := new Stream;
+ wr.Create();
while (0 < |q.contents|)
invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;
{
- call ch := q.Dequeue();
- call wr.PutChar(ch);
+ var ch := q.Dequeue();
+ wr.PutChar(ch);
}
- call wr.Close();
+ wr.Close();
}
}
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index 3438d6e0..0c9d1186 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -46,7 +46,7 @@ class Glossary { method Main()
{
var rs:= new ReaderStream;
- call rs.Open();
+ rs.Open();
var glossary := new Map<Word,seq<Word>>.Init();
var q := new Queue<Word>.Init();
@@ -60,21 +60,22 @@ class Glossary { invariant q.contents == glossary.keys;
decreases *; // we leave out the decreases clause - unbounded stream
{
- call term,definition := readDefinition(rs);
+ var term,definition := readDefinition(rs);
if (term == null) {
break;
}
- call present, d := glossary.Find(term);
+ var present, d := glossary.Find(term);
if (!present) {
- call glossary.Add(term,definition);
- call q.Enqueue(term);
+ glossary.Add(term,definition);
+ q.Enqueue(term);
}
}
- call rs.Close();
- call q,p := Sort(q);
+ rs.Close();
+ var p;
+ q,p := Sort(q);
var wr := new WriterStream;
- call wr.Create();
+ wr.Create();
while (0 < |q.contents|)
invariant wr.Valid() && fresh(wr.footprint);
@@ -84,12 +85,12 @@ class Glossary { invariant q !in wr.footprint;
invariant (forall k :: k in q.contents ==> k in glossary.keys);
{
- call term := q.Dequeue();
- call present,definition := glossary.Find(term);
+ var term := q.Dequeue();
+ var present,definition := glossary.Find(term);
assert present;
// write term with a html anchor
- call wr.PutWordInsideTag(term, term);
+ wr.PutWordInsideTag(term, term);
var i := 0;
var qcon := q.contents;
@@ -103,19 +104,20 @@ class Glossary { invariant (forall k :: k in q.contents ==> k in glossary.keys);
{
var w := definition[i];
- call present, d := glossary.Find(w);
+ var d;
+ present, d := glossary.Find(w);
if (present)
{
- call wr. PutWordInsideHyperlink(w, w);
+ wr. PutWordInsideHyperlink(w, w);
}
else
{
- call wr. PutWord(w);
+ wr. PutWord(w);
}
i:= i +1;
}
}
- call wr.Close();
+ wr.Close();
}
@@ -125,7 +127,7 @@ class Glossary { ensures rs.Valid() && fresh(rs.footprint - old(rs.footprint));
ensures term != null ==> null !in definition;
{
- call term := rs.GetWord();
+ term := rs.GetWord();
if (term != null)
{
definition := [];
@@ -134,7 +136,7 @@ class Glossary { invariant null !in definition;
decreases *; // we leave out the decreases clause - unbounded stream
{
- call w := rs.GetWord();
+ var w := rs.GetWord();
if (w == null)
{
break;
@@ -273,7 +275,7 @@ class Map<Key,Value> { ensures present ==> (exists i :: 0 <= i && i < |keys| &&
keys[i] == key && values[i] == val);
{
- call j := FindIndex(key);
+ var j := FindIndex(key);
if (j == -1) {
present := false;
} else {
@@ -292,7 +294,7 @@ class Map<Key,Value> { (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));
ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];
{
- call j := FindIndex(key);
+ var j := FindIndex(key);
if (j == -1) {
keys := keys + [key];
values := values + [val];
@@ -321,7 +323,7 @@ class Map<Key,Value> { keys[h..] == old(keys)[h+1..] &&
values[h..] == old(values)[h+1..]);
{
- call j := FindIndex(key);
+ var j := FindIndex(key);
if (0 <= j) {
keys := keys[..j] + keys[j+1..];
values := values[..j] + values[j+1..];
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 289a597d..efcfa8bb 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -22,10 +22,10 @@ class MyClass<T, U> { } else {
this.x := x + 0;
}
- call t, u, v := M(true, lotsaObjects);
+ t, u, v := M(true, lotsaObjects);
var to: MyClass<T,U>;
- call to, u, v := M(true, lotsaObjects);
- call to, u, v := to.M(true, lotsaObjects);
+ to, u, v := this.M(true, lotsaObjects);
+ to, u, v := to.M(true, lotsaObjects);
assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
}
}
@@ -70,9 +70,9 @@ TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, g TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)
-TypeTests.dfy(11,4): Error: incorrect type of method in-parameter 0 (expected int, got bool)
-TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 0 (expected int, got C)
-TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C, got int)
+TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed
TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
TypeTests.dfy(55,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
@@ -85,12 +85,12 @@ TypeTests.dfy(80,17): Error: a method called as an initialization method must no TypeTests.dfy(89,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
TypeTests.dfy(90,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
TypeTests.dfy(96,9): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(97,6): Error: sorry, cannot instantiate 'array' type with a subrange type
-TypeTests.dfy(98,6): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(97,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(98,8): Error: sorry, cannot instantiate 'array' type with a subrange type
22 resolution/type errors detected in TypeTests.dfy
-------------------- NatTypes.dfy --------------------
-NatTypes.dfy(7,10): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
NatTypes.dfy(31,5): Error: value assigned to a nat must be non-negative
@@ -119,7 +119,7 @@ Execution trace: (0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
-NatTypes.dfy(89,9): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(89,16): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
@@ -160,11 +160,11 @@ Execution trace: (0,0): anon0
(0,0): anon4_Else
(0,0): anon3
-SmallTests.dfy(129,7): Error: call may violate caller's modifies clause
+SmallTests.dfy(129,9): Error: call may violate caller's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-SmallTests.dfy(131,7): Error: call may violate caller's modifies clause
+SmallTests.dfy(131,9): Error: call may violate caller's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Else
@@ -402,7 +402,7 @@ Execution trace: Dafny program verifier finished with 3 verified, 3 errors
-------------------- ResolutionErrors.dfy --------------------
-ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'class' context
+ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)
@@ -410,9 +410,11 @@ ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got arra ResolutionErrors.dfy(45,14): Error: a field must be selected via an object, not just a class name
ResolutionErrors.dfy(46,7): Error: unresolved identifier: F
ResolutionErrors.dfy(47,14): Error: an instance function must be selected via an object, not just a class name
+ResolutionErrors.dfy(47,7): Error: call to instance function requires an instance
ResolutionErrors.dfy(48,7): Error: unresolved identifier: G
-ResolutionErrors.dfy(50,2): Error: member M does not exist in class _default
-ResolutionErrors.dfy(52,2): Error: member N does not exist in class _default
+ResolutionErrors.dfy(50,7): Error: unresolved identifier: M
+ResolutionErrors.dfy(51,7): Error: call to instance method requires an instance
+ResolutionErrors.dfy(52,7): Error: unresolved identifier: N
ResolutionErrors.dfy(55,8): Error: non-function expression is called with parameters
ResolutionErrors.dfy(56,14): Error: member z does not exist in class Global
ResolutionErrors.dfy(75,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
@@ -420,7 +422,7 @@ ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype construc ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
-18 resolution/type errors detected in ResolutionErrors.dfy
+20 resolution/type errors detected in ResolutionErrors.dfy
-------------------- Array.dfy --------------------
Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause
@@ -512,11 +514,11 @@ Dafny program verifier finished with 7 verified, 1 error Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
Modules0.dfy(13,7): Error: module T named among imports does not exist
Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G
-Modules0.dfy(51,6): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)
-Modules0.dfy(62,6): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
-Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
-Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
-Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts
+Modules0.dfy(51,8): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)
+Modules0.dfy(62,9): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
+Modules0.dfy(72,9): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
+Modules0.dfy(91,6): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
+Modules0.dfy(116,11): Error: ghost variables are allowed only in specification contexts
Modules0.dfy(130,11): Error: old expressions are allowed only in specification and ghost contexts
Modules0.dfy(131,11): Error: fresh expressions are allowed only in specification and ghost contexts
Modules0.dfy(132,11): Error: allocated expressions are allowed only in specification and ghost contexts
@@ -599,57 +601,57 @@ Execution trace: Dafny program verifier finished with 15 verified, 6 errors
-------------------- Termination.dfy --------------------
-Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(103,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
- Termination.dfy(102,3): anon7_LoopHead
+ Termination.dfy(103,3): anon7_LoopHead
(0,0): anon7_LoopBody
- Termination.dfy(102,3): anon8_Else
+ Termination.dfy(103,3): anon8_Else
(0,0): anon3
- Termination.dfy(102,3): anon9_Else
+ Termination.dfy(103,3): anon9_Else
(0,0): anon5
-Termination.dfy(110,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(111,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
- Termination.dfy(110,3): anon9_LoopHead
+ Termination.dfy(111,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(110,3): anon10_Else
+ Termination.dfy(111,3): anon10_Else
(0,0): anon11_Then
(0,0): anon5
- Termination.dfy(110,3): anon12_Else
+ Termination.dfy(111,3): anon12_Else
(0,0): anon7
-Termination.dfy(119,3): Error: decreases expression might not decrease
+Termination.dfy(120,3): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
- Termination.dfy(119,3): anon9_LoopHead
+ Termination.dfy(120,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(119,3): anon10_Else
+ Termination.dfy(120,3): anon10_Else
(0,0): anon11_Then
(0,0): anon5
- Termination.dfy(119,3): anon12_Else
+ Termination.dfy(120,3): anon12_Else
(0,0): anon7
-Termination.dfy(120,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
+Termination.dfy(121,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
Execution trace:
(0,0): anon0
- Termination.dfy(119,3): anon9_LoopHead
+ Termination.dfy(120,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(119,3): anon10_Else
+ Termination.dfy(120,3): anon10_Else
(0,0): anon11_Then
(0,0): anon5
- Termination.dfy(119,3): anon12_Else
+ Termination.dfy(120,3): anon12_Else
(0,0): anon7
-Termination.dfy(248,35): Error: cannot prove termination; try supplying a decreases clause
+Termination.dfy(249,35): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
-Termination.dfy(288,3): Error: decreases expression might not decrease
+Termination.dfy(289,3): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
- Termination.dfy(288,3): anon10_LoopHead
+ Termination.dfy(289,3): anon10_LoopHead
(0,0): anon10_LoopBody
- Termination.dfy(288,3): anon11_Else
- Termination.dfy(288,3): anon12_Else
+ Termination.dfy(289,3): anon11_Else
+ Termination.dfy(289,3): anon12_Else
(0,0): anon13_Else
(0,0): anon8
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 1eeb2d92..e6b9a87d 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -23,19 +23,19 @@ method TestCalls(k: nat) { ghost var r: int;
ghost var s := Global.G(k);
-// call r := Global.N(k);
+// r := Global.N(k);
// assert r == s;
- call r := g.N(k);
+ r := g.N(k);
assert r == s;
- call r := h.N(k);
+ r := h.N(k);
assert r == s;
g := null;
- call r := g.N(k);
+ r := g.N(k);
assert r == s;
-// call r := Global.N(r);
+// r := Global.N(r);
if (k == 0) {
assert r == s;
} else {
diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy index 8629a418..d53fb6a5 100644 --- a/Test/dafny0/Comprehensions.dfy +++ b/Test/dafny0/Comprehensions.dfy @@ -16,14 +16,14 @@ function method Id(x: int): int { x } // for triggering method Main()
{
var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;
- call PrintSet(q);
+ PrintSet(q);
q := set b: bool | true :: if b then 3 else 7;
- call PrintSet(q);
+ PrintSet(q);
var m := set k | k in q :: 2*k;
- call PrintSet(m);
- call PrintSet(set k | k in q && k % 2 == 0);
+ PrintSet(m);
+ PrintSet(set k | k in q && k % 2 == 0);
var sq := [30, 40, 20];
- call PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
+ PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;
}
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index 59052ac2..01e14585 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -38,17 +38,17 @@ module J imports G, M { module X2 imports X1 {
class MyClass2 {
method Down(x1: MyClass1, x0: MyClass0) {
- call x1.Down(x0);
+ x1.Down(x0);
}
method WayDown(x0: MyClass0, g: ClassG) {
- call x0.Down();
- call g.T(); // allowed, because this follows import relation
+ x0.Down();
+ g.T(); // allowed, because this follows import relation
var t := g.TFunc(); // allowed, because this follows import relation
}
method Up() {
}
method Somewhere(y: MyClassY) {
- call y.M(); // error: does not follow import relation
+ y.M(); // error: does not follow import relation
}
}
}
@@ -56,10 +56,10 @@ module X2 imports X1 { module X1 imports X0 {
class MyClass1 {
method Down(x0: MyClass0) {
- call x0.Down();
+ x0.Down();
}
method Up(x2: MyClass2) {
- call x2.Up(); // error: does not follow import relation
+ x2.Up(); // error: does not follow import relation
}
}
}
@@ -69,7 +69,7 @@ module X0 { method Down() {
}
method Up(x1: MyClass1, x2: MyClass2) {
- call x1.Up(x2); // error: does not follow import relation
+ x1.Up(x2); // error: does not follow import relation
}
}
}
@@ -78,7 +78,7 @@ module YY { class MyClassY {
method M() { }
method P(g: ClassG) {
- call g.T(); // allowed, because this follows import relation
+ g.T(); // allowed, because this follows import relation
var t := g.TFunc(); // allowed, because this follows import relation
}
}
@@ -88,20 +88,20 @@ class ClassG { method T() { }
function method TFunc(): int { 10 }
method V(y: MyClassY) {
- call y.M(); // error: does not follow import relation
+ y.M(); // error: does not follow import relation
}
}
method Ping() {
- call Pong(); // allowed: intra-module call
+ Pong(); // allowed: intra-module call
}
method Pong() {
- call Ping(); // allowed: intra-module call
+ Ping(); // allowed: intra-module call
}
method ProcG(g: ClassG) {
- call g.T(); // allowed: intra-module call
+ g.T(); // allowed: intra-module call
var t := g.TFunc(); // allowed: intra-module call
}
@@ -111,11 +111,11 @@ class Ghosty { method Caller() {
var x := 3;
ghost var y := 3;
- call Callee(x, y); // fine
- call Callee(x, x); // fine
- call Callee(y, x); // error: cannot pass in ghost to a physical formal
- call Theorem(x); // fine
- call Theorem(y); // fine, because it's a ghost method
+ Callee(x, y); // fine
+ Callee(x, x); // fine
+ Callee(y, x); // error: cannot pass in ghost to a physical formal
+ Theorem(x); // fine
+ Theorem(y); // fine, because it's a ghost method
}
method Callee(a: int, ghost b: int) { }
ghost method Theorem(a: int) { }
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index cfefa7fa..ff84b84b 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -37,7 +37,7 @@ method Proc0(x: int) decreases x;
{
if (0 <= x) {
- call Proc1(x - 1);
+ Proc1(x - 1);
}
}
@@ -45,18 +45,18 @@ method Proc1(x: int) decreases x;
{
if (0 <= x) {
- call Proc0(x - 1);
+ Proc0(x - 1);
}
}
method Botch0(x: int)
decreases x;
{
- call Botch1(x - 1); // error: failure to keep termination metric bounded
+ Botch1(x - 1); // error: failure to keep termination metric bounded
}
method Botch1(x: int)
decreases x;
{
- call Botch0(x); // error: failure to decrease termination metric
+ Botch0(x); // error: failure to decrease termination metric
}
diff --git a/Test/dafny0/MultiDimArray.dfy b/Test/dafny0/MultiDimArray.dfy index ba5dc9da..ff30ef8a 100644 --- a/Test/dafny0/MultiDimArray.dfy +++ b/Test/dafny0/MultiDimArray.dfy @@ -74,7 +74,7 @@ class A { var s := z[1,2,4]; // first three powers of 2 (tra-la-la)
var some: A;
f[i,j,k] := some;
- call M3(i-1, j, k);
+ M3(i-1, j, k);
assert s == z[1,2,4];
if (*) {
assert f[i,j,k] == some; // error: the recursive call may have modified any element in 'f'
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index 161ac22f..e4d0cbe7 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -3,8 +3,8 @@ method M(n: nat) { }
method Main() {
- call M(25);
- call M(-25); // error: cannot pass -25 as a nat
+ M(25);
+ M(-25); // error: cannot pass -25 as a nat
}
var f: nat;
@@ -34,7 +34,7 @@ method CheckField(x: nat, y: int) method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
if (0 < i) {
var n: nat := 5;
- call j := Generic(i-1, n, -4);
+ var j := Generic(i-1, n, -4);
assert 0 <= j; // error: the result is an int, not a nat
var q := FenEric(n, -4);
assert 0 <= q; // error: the result is an int, not a nat
@@ -65,7 +65,7 @@ method MatchIt(list: List<object>) returns (k: nat) match (list) {
case Nil =>
case Cons(n, extra, tail) =>
- call w := MatchIt(tail);
+ var w := MatchIt(tail);
assert 0 <= w;
assert 0 <= n; // fine
assert 0 <= n - 10; // error: possible assertion failure
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index b33d4d54..56d7575f 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -47,10 +47,10 @@ method TestNameResolution0() { z := Global.F(2); // error: invocation of instance function requires an instance
z := G(2); // error: cannot resolve G
z := Global.G(2);
- call z := M(2); // error: cannot resolve M
-// call z := Global.M(2); // error: call to instance method requires an instance
- call z := N(1); // error: cannot resolve N
-// call z := Global.N(1);
+ z := M(2); // error: cannot resolve M
+ z := Global.M(2); // error: call to instance method requires an instance
+ z := N(1); // error: cannot resolve N
+ z := Global.N(1);
z := z(5); // error: using local as if it were a function
z := Global.z; // error: class Global does not have a member z
@@ -59,7 +59,7 @@ method TestNameResolution0() { z := Global.X; // this means the instance field X of the object stored in the local variable 'Global'
var gg: Global := null;
var y := gg.G(5);
- call y := gg.N(5);
+ y := gg.N(5);
}
datatype Abc = Abel | Benny | Cecilia(y: int) | David(x: int) | Eleanor;
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index 930c4253..e1416094 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -20,10 +20,10 @@ class MyClass<T,U> { } else {
this.x := x + 0;
}
- call t, u, v := M(true, lotsaObjects);
+ t, u, v := M(true, lotsaObjects);
var to: MyClass<T,U>;
- call to, u, v := this.M(true, lotsaObjects);
- call to, u, v := to.M(true, lotsaObjects);
+ to, u, v := this.M(true, lotsaObjects);
+ to, u, v := to.M(true, lotsaObjects);
assert v[x] != null ==> null !in v[2..x][1..][5 := v[this.x]][..10];
}
}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 3359cff1..fcc764aa 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -109,11 +109,11 @@ class Modifies { method B(p: Modifies)
modifies this;
{
- call A(this);
+ A(this);
if (p == this) {
- call p.A(p);
+ p.A(p);
}
- call A(p); // error: may violate modifies clause
+ A(p); // error: may violate modifies clause
}
method C(b: bool)
@@ -126,9 +126,9 @@ class Modifies { requires p != null;
{
if (y == 3) {
- call p.C(true); // error: may violate modifies clause
+ p.C(true); // error: may violate modifies clause
} else {
- call p.C(false); // error: may violation modifies clause (the check is done without regard
+ p.C(false); // error: may violation modifies clause (the check is done without regard
// for the postcondition, which also makes sense, since there may, in
// principle, be other fields of the object that are not constrained by the
// postcondition)
@@ -138,7 +138,7 @@ class Modifies { method E()
modifies this;
{
- call A(null); // allowed
+ A(null); // allowed
}
method F(s: set<Modifies>)
@@ -164,7 +164,7 @@ class Modifies { foreach (m in s) {
m.x := m.x + 1;
}
- call F(s);
+ F(s);
}
foreach (m in s) {
assert m.x < m.x + 10; // nothing wrong with asserting something
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 5d411eb3..155fbaef 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -28,8 +28,8 @@ class Termination { }
method Lex() {
- call x := Update();
- call y := Update();
+ var x := Update();
+ var y := Update();
while (!(x == 0 && y == 0))
invariant 0 <= x && 0 <= y;
decreases x, y;
@@ -38,7 +38,7 @@ class Termination { y := y - 1;
} else {
x := x - 1;
- call y := Update();
+ y := Update();
}
}
}
@@ -82,7 +82,8 @@ class Termination { while (l != List.Nil)
decreases l;
{
- call x, l := Traverse(l);
+ var x;
+ x, l := Traverse(l);
}
}
@@ -204,7 +205,7 @@ method OuterOld(a: int) decreases a, true;
{
count := count + 1;
- call InnerOld(a, count);
+ InnerOld(a, count);
}
method InnerOld(a: int, b: int)
@@ -213,9 +214,9 @@ method InnerOld(a: int, b: int) {
count := count + 1;
if (b == 0 && 1 <= a) {
- call OuterOld(a - 1);
+ OuterOld(a - 1);
} else if (1 <= b) {
- call InnerOld(a, b - 1);
+ InnerOld(a, b - 1);
}
}
@@ -225,7 +226,7 @@ method Outer(a: int) modifies this;
{
count := count + 1;
- call Inner(a, count);
+ Inner(a, count);
}
method Inner(a: int, b: int)
@@ -233,9 +234,9 @@ method Inner(a: int, b: int) {
count := count + 1;
if (b == 0 && 1 <= a) {
- call Outer(a - 1);
+ Outer(a - 1);
} else if (1 <= b) {
- call Inner(a, b - 1);
+ Inner(a, b - 1);
}
}
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy index a932eccf..38050b88 100644 --- a/Test/dafny0/TypeAntecedents.dfy +++ b/Test/dafny0/TypeAntecedents.dfy @@ -35,7 +35,7 @@ method BadLemma(c0: Color, c1: Color) }
method Main() {
- call BadLemma(Color.Yellow, Color.Blue);
+ BadLemma(Color.Yellow, Color.Blue);
assert false; // this shows how things can really go wrong if BadLemma verified successfully
}
@@ -68,7 +68,7 @@ method M(list: List, S: set<MyClass>) returns (ret: int) assert false; // error
}
}
- call k := N();
+ var k := N();
assert k.H() == 5;
ghost var l := NF();
assert l != null ==> l.H() == 5;
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index a044341e..a3698dc0 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -13,7 +13,7 @@ class C<U> { method Main(u: U)
{
var t := F(3,u) && F(this,u);
- call kz := M(t,u);
+ var kz := M(t,u);
assert kz && (G() || !G());
}
@@ -30,14 +30,14 @@ class SetTest { method Good()
{
var s := {2, 5, 3};
- call t := Add(s, 7);
+ var t := Add(s, 7);
assert {5,7,2,3} == t;
}
method Bad()
{
var s := {2, 50, 3};
- call t := Add(s, 7);
+ var t := Add(s, 7);
assert {5,7,2,3} == t; // error
}
}
@@ -52,14 +52,14 @@ class SequenceTest { method Good()
{
var s := [2, 5, 3];
- call t := Add(s, 7);
+ var t := Add(s, 7);
assert [2,5,3,7] == t;
}
method Bad()
{
var s := [2, 5, 3];
- call t := Add(s, 7);
+ var t := Add(s, 7);
assert [2,5,7,3] == t || [2,5,3] == t; // error
}
}
@@ -92,7 +92,7 @@ class CClient { }
c.x := 5;
c.x := c.x;
- call z := c.M(c, 17);
+ var z := c.M(c, 17);
assert z == c.x;
}
}
@@ -170,7 +170,7 @@ method TyKn_Main(k0: TyKn_K) { assert c.x != null ==> c.x.F() == 176; // the Dafny encoding needs the canCall mechanism to verify this
assert c.G() != null ==> c.G().F() == 176; // ditto
- call k2 := c.M();
+ var k2 := c.M();
assert k2 != null ==> k2.F() == 176; // the canCall mechanism does the trick here, but so does the encoding
// via k2's where clause
}
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 7deeb0a1..21f0dda8 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -8,8 +8,8 @@ class C { method Caller()
{
- call m,n := M(true); // error on in-parameter
- call n,m := M(m); // 2 errors on out-parameters
+ var m,n := M(true); // error on in-parameter
+ n,m := M(m); // 2 errors on out-parameters
}
}
diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy index b4980d4b..88b06605 100644 --- a/Test/dafny1/BinaryTree.dfy +++ b/Test/dafny1/BinaryTree.dfy @@ -32,7 +32,7 @@ class IntSet { if (root == null) {
present := false;
} else {
- call present := root.Find(x);
+ present := root.Find(x);
}
}
@@ -42,7 +42,7 @@ class IntSet { ensures Valid() && fresh(Repr - old(Repr));
ensures Contents == old(Contents) + {x};
{
- call t := InsertHelper(x, root);
+ var t := InsertHelper(x, root);
root := t;
Contents := root.Contents;
Repr := root.Repr + {this};
@@ -64,12 +64,12 @@ class IntSet { } else {
if (x < n.data) {
assert n.right == null || n.right.Valid();
- call t := InsertHelper(x, n.left);
+ var t := InsertHelper(x, n.left);
n.left := t;
n.Repr := n.Repr + n.left.Repr;
} else {
assert n.left == null || n.left.Valid();
- call t := InsertHelper(x, n.right);
+ var t := InsertHelper(x, n.right);
n.right := t;
n.Repr := n.Repr + n.right.Repr;
}
@@ -85,7 +85,7 @@ class IntSet { ensures Contents == old(Contents) - {x};
{
if (root != null) {
- call newRoot := root.Remove(x);
+ var newRoot := root.Remove(x);
root := newRoot;
if (root == null) {
Contents := {};
@@ -152,9 +152,9 @@ class Node { if (x == data) {
present := true;
} else if (left != null && x < data) {
- call present := left.Find(x);
+ present := left.Find(x);
} else if (right != null && data < x) {
- call present := right.Find(x);
+ present := right.Find(x);
} else {
present := false;
}
@@ -171,12 +171,12 @@ class Node { {
node := this;
if (left != null && x < data) {
- call t := left.Remove(x);
+ var t := left.Remove(x);
left := t;
Contents := Contents - {x};
if (left != null) { Repr := Repr + left.Repr; }
} else if (right != null && data < x) {
- call t := right.Remove(x);
+ var t := right.Remove(x);
right := t;
Contents := Contents - {x};
if (right != null) { Repr := Repr + right.Repr; }
@@ -189,7 +189,7 @@ class Node { node := left;
} else {
// rotate
- call min, r := right.RemoveMin();
+ var min, r := right.RemoveMin();
data := min; right := r;
Contents := Contents - {x};
if (right != null) { Repr := Repr + right.Repr; }
@@ -211,7 +211,8 @@ class Node { min := data;
node := right;
} else {
- call min, t := left.RemoveMin();
+ var t;
+ min, t := left.RemoveMin();
left := t;
node := this;
Contents := Contents - {min};
@@ -225,9 +226,9 @@ class Main { {
var s := new IntSet.Init();
- call s.Insert(12);
- call s.Insert(24);
- call present := s.Find(x);
+ s.Insert(12);
+ s.Insert(24);
+ var present := s.Find(x);
assert present <==> x == 12 || x == 24;
}
@@ -235,8 +236,8 @@ class Main { requires s != null && s.Valid();
modifies s.Repr;
{
- call s.Insert(x);
- call s.Insert(24);
+ s.Insert(x);
+ s.Insert(24);
assert old(s.Contents) - {x,24} == s.Contents - {x,24};
}
}
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy index 089a72c4..2dc49cd9 100644 --- a/Test/dafny1/ExtensibleArray.dfy +++ b/Test/dafny1/ExtensibleArray.dfy @@ -57,7 +57,7 @@ class ExtensibleArray<T> { if (M <= i) {
t := elements[i - M];
} else {
- call arr := more.Get(i / 256);
+ var arr := more.Get(i / 256);
t := arr[i % 256];
}
}
@@ -72,7 +72,7 @@ class ExtensibleArray<T> { if (M <= i) {
elements[i - M] := t;
} else {
- call arr := more.Get(i / 256);
+ var arr := more.Get(i / 256);
arr[i % 256] := t;
}
Contents := Contents[i := t];
@@ -94,7 +94,7 @@ class ExtensibleArray<T> { Repr := Repr + {more} + more.Repr;
}
// "elements" is full, so move it into "more" and allocate a new array
- call more.Append(elements);
+ more.Append(elements);
Repr := Repr + more.Repr;
M := M + 256;
elements := new T[256];
@@ -113,14 +113,14 @@ method Main() { invariant a.Valid() && fresh(a.Repr);
invariant |a.Contents| == n;
{
- call a.Append(n);
+ a.Append(n);
n := n + 1;
}
- call k := a.Get(570); print k, "\n";
- call k := a.Get(0); print k, "\n";
- call k := a.Get(1000); print k, "\n";
- call a.Set(1000, 23);
- call k := a.Get(0); print k, "\n";
- call k := a.Get(1000); print k, "\n";
- call k := a.Get(66000); print k, "\n";
+ var k := a.Get(570); print k, "\n";
+ k := a.Get(0); print k, "\n";
+ k := a.Get(1000); print k, "\n";
+ a.Set(1000, 23);
+ k := a.Get(0); print k, "\n";
+ k := a.Get(1000); print k, "\n";
+ k := a.Get(66000); print k, "\n";
}
diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy index cff8b934..76e67205 100644 --- a/Test/dafny1/FindZero.dfy +++ b/Test/dafny1/FindZero.dfy @@ -9,7 +9,7 @@ method FindZero(a: array<int>) returns (r: int) invariant forall i :: 0 <= i && i < n && i < a.Length ==> a[i] != 0;
{
if (a[n] == 0) { r := n; return; }
- call Lemma(a, n, a[n]);
+ Lemma(a, n, a[n]);
n := n + a[n];
}
r := -1;
@@ -25,6 +25,6 @@ ghost method Lemma(a: array<int>, k: int, m: int) {
if (0 < m && k < a.Length) {
assert a[k] != 0;
- call Lemma(a, k+1, m-1);
+ Lemma(a, k+1, m-1);
}
}
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index 0e4c58e0..2c90769b 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -24,8 +24,8 @@ class IntegerInduction { ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
{
if (n != 0) {
- call Theorem0(n-1);
- call Lemma(n-1);
+ Theorem0(n-1);
+ Lemma(n-1);
}
}
@@ -33,7 +33,7 @@ class IntegerInduction { requires 0 <= n;
ensures 2 * Gauss(n) == n*(n+1);
{
- if (n != 0) { call Lemma(n-1); }
+ if (n != 0) { Lemma(n-1); }
}
// Here is another proof. It states the lemma as part of the theorem, and
@@ -45,7 +45,7 @@ class IntegerInduction { ensures 2 * Gauss(n) == n*(n+1);
{
if (n != 0) {
- call Theorem1(n-1);
+ Theorem1(n-1);
}
}
@@ -64,7 +64,7 @@ class IntegerInduction { ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
{
if (n != 0) {
- call Theorem2(n-1);
+ Theorem2(n-1);
assert (forall m :: 0 <= m ==> 2 * Gauss(m) == m*(m+1));
}
@@ -84,7 +84,7 @@ class IntegerInduction { ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
{
if (n != 0) {
- call Theorem3(n-1);
+ Theorem3(n-1);
}
}
@@ -112,7 +112,7 @@ class IntegerInduction { if (*) {
assert (forall m :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m));
} else {
- call Theorem4();
+ Theorem4();
}
}
diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy index 86ad451d..81b3f4c9 100644 --- a/Test/dafny1/MatrixFun.dfy +++ b/Test/dafny1/MatrixFun.dfy @@ -64,20 +64,20 @@ method Main() B[0,0] := true; B[0,1] := false; B[0,2] := false; B[0,3] := true; B[0,4] := false;
B[1,0] := true; B[1,1] := true; B[1,2] := true; B[1,3] := true; B[1,4] := false;
print "Before:\n";
- call PrintMatrix(B);
- call MirrorImage(B);
+ PrintMatrix(B);
+ MirrorImage(B);
print "Mirror image:\n";
- call PrintMatrix(B);
+ PrintMatrix(B);
var A := new int[3,3];
A[0,0] := 5; A[0,1] := 7; A[0,2] := 9;
A[1,0] := 6; A[1,1] := 2; A[1,2] := 3;
A[2,0] := 7; A[2,1] := 1; A[2,2] := 0;
print "Before:\n";
- call PrintMatrix(A);
- call Flip(A);
+ PrintMatrix(A);
+ Flip(A);
print "Flip:\n";
- call PrintMatrix(A);
+ PrintMatrix(A);
}
method PrintMatrix<T>(m: array2<T>)
diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy index db1c60fa..6e19ab8f 100644 --- a/Test/dafny1/PriorityQueue.dfy +++ b/Test/dafny1/PriorityQueue.dfy @@ -41,7 +41,7 @@ class PriorityQueue { {
n := n + 1;
a[n] := x;
- call SiftUp(n);
+ SiftUp(n);
}
method SiftUp(k: int)
@@ -76,7 +76,7 @@ class PriorityQueue { x := a[1];
a[1] := a[n];
n := n - 1;
- call SiftDown(1);
+ SiftDown(1);
}
method SiftDown(k: int)
@@ -156,7 +156,7 @@ class PriorityQueue_Alternative { {
n := n + 1;
a[n] := x;
- call SiftUp();
+ SiftUp();
}
method SiftUp()
@@ -189,7 +189,7 @@ class PriorityQueue_Alternative { x := a[1];
a[1] := a[n];
n := n - 1;
- call SiftDown();
+ SiftDown();
}
method SiftDown()
diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy index 0ee953e1..bfb588be 100644 --- a/Test/dafny1/Queue.dfy +++ b/Test/dafny1/Queue.dfy @@ -48,9 +48,9 @@ class Queue<T> { ensures Valid() && fresh(footprint - old(footprint));
ensures contents == old(contents)[1..] + old(contents)[..1];
{
- call t := Front();
- call Dequeue();
- call Enqueue(t);
+ var t := Front();
+ Dequeue();
+ Enqueue(t);
}
method RotateAny()
@@ -62,9 +62,9 @@ class Queue<T> { ensures (exists i :: 0 <= i && i <= |contents| &&
contents == old(contents)[i..] + old(contents)[..i]);
{
- call t := Front();
- call Dequeue();
- call Enqueue(t);
+ var t := Front();
+ Dequeue();
+ Enqueue(t);
}
method IsEmpty() returns (isEmpty: bool)
@@ -152,18 +152,18 @@ class Main<U> { var q0 := new Queue<T>.Init();
var q1 := new Queue<T>.Init();
- call q0.Enqueue(t);
- call q0.Enqueue(u);
+ q0.Enqueue(t);
+ q0.Enqueue(u);
- call q1.Enqueue(v);
+ q1.Enqueue(v);
assert |q0.contents| == 2;
- call w := q0.Front();
+ var w := q0.Front();
assert w == t;
- call q0.Dequeue();
+ q0.Dequeue();
- call w := q0.Front();
+ w := q0.Front();
assert w == u;
assert |q0.contents| == 1;
@@ -179,18 +179,18 @@ class Main<U> { ensures fresh(q0.footprint - old(q0.footprint));
ensures fresh(q1.footprint - old(q1.footprint));
{
- call q0.Enqueue(t);
- call q0.Enqueue(u);
+ q0.Enqueue(t);
+ q0.Enqueue(u);
- call q1.Enqueue(v);
+ q1.Enqueue(v);
assert |q0.contents| == 2;
- call w := q0.Front();
+ var w := q0.Front();
assert w == t;
- call q0.Dequeue();
+ q0.Dequeue();
- call w := q0.Front();
+ w := q0.Front();
assert w == u;
assert |q0.contents| == 1;
diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index 33442219..95cdab89 100644 --- a/Test/dafny1/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy @@ -26,7 +26,7 @@ class Main { n.childrenVisited == old(n.childrenVisited) &&
n.children == old(n.children));
{
- call RecursiveMarkWorker(root, S, {});
+ RecursiveMarkWorker(root, S, {});
}
method RecursiveMarkWorker(root: Node, ghost S: set<Node>, ghost stackNodes: set<Node>)
@@ -67,7 +67,7 @@ class Main { {
var c := root.children[i];
if (c != null) {
- call RecursiveMarkWorker(c, S, stackNodes + {root});
+ RecursiveMarkWorker(c, S, stackNodes + {root});
}
i := i + 1;
}
diff --git a/Test/dafny1/SeparationLogicList.dfy b/Test/dafny1/SeparationLogicList.dfy index 7828a54e..56a64bd6 100644 --- a/Test/dafny1/SeparationLogicList.dfy +++ b/Test/dafny1/SeparationLogicList.dfy @@ -28,7 +28,7 @@ class Node<T> { l.next := null;
S := {l};
} else {
- call l, S := Cons(x, null, [], {});
+ l, S := Cons(x, null, [], {});
}
}
@@ -75,7 +75,7 @@ class ListNode<T> { l.Repr := {l};
l.Contents := [x];
} else {
- call l := Cons(x, null);
+ l := Cons(x, null);
}
}
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index 5cee5f6a..d3e0e82e 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -31,7 +31,7 @@ static ghost method Theorem(e: Expr, v: int, val: int) case Const(c) =>
case Var(x) =>
case Nary(op, args) =>
- call Lemma(args, v, val);
+ Lemma(args, v, val);
}
}
@@ -41,8 +41,8 @@ static ghost method Lemma(l: List, v: int, val: int) match l {
case Nil =>
case Cons(e, tail) =>
- call Theorem(e, v, val);
- call Lemma(tail, v, val);
+ Theorem(e, v, val);
+ Lemma(tail, v, val);
}
}
@@ -80,11 +80,11 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) case Var(x) =>
case Nary(op, args) =>
ghost var seArgs := SubstSeq(e, args, v, val);
- call LemmaSeq(e, args, v, val);
+ LemmaSeq(e, args, v, val);
ghost var se := Substitute(e, v, val);
ghost var seArgs2 := SubstSeq(se, seArgs, v, val);
- call LemmaSeq(se, seArgs, v, val);
+ LemmaSeq(se, seArgs, v, val);
var N := |args|;
var j := 0;
@@ -92,7 +92,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) invariant j <= N;
invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]);
{
- call TheoremSeq(args[j], v, val);
+ TheoremSeq(args[j], v, val);
j := j + 1;
}
assert seArgs == seArgs2;
@@ -107,6 +107,6 @@ static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>, {
if (q == []) {
} else {
- call LemmaSeq(parent, q[..|q|-1], v, val);
+ LemmaSeq(parent, q[..|q|-1], v, val);
}
}
diff --git a/Test/dafny1/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy index 2fecaee5..7ed7ce9b 100644 --- a/Test/dafny1/SumOfCubes.dfy +++ b/Test/dafny1/SumOfCubes.dfy @@ -10,19 +10,19 @@ class SumOfCubes { requires 0 <= n && n <= m;
ensures r == SumEmUp(n, m);
{
- call a := SocuFromZero(m);
- call b := SocuFromZero(n);
+ var a := SocuFromZero(m);
+ var b := SocuFromZero(n);
r := a - b;
- call Lemma0(n, m);
+ Lemma0(n, m);
}
static method SocuFromZero(k: int) returns (r: int)
requires 0 <= k;
ensures r == SumEmUp(0, k);
{
- call g := Gauss(k);
+ var g := Gauss(k);
r := g * g;
- call Lemma1(k);
+ Lemma1(k);
}
ghost static method Lemma0(n: int, m: int)
@@ -36,9 +36,9 @@ class SumOfCubes { {
k := k + 1;
}
- call Lemma3(0, n);
- call Lemma3(n, k);
- call Lemma3(0, k);
+ Lemma3(0, n);
+ Lemma3(n, k);
+ Lemma3(0, k);
}
static function GSum(k: int): int
@@ -52,7 +52,7 @@ class SumOfCubes { ensures r == GSum(k);
{
r := k * (k - 1) / 2;
- call Lemma2(k);
+ Lemma2(k);
}
ghost static method Lemma1(k: int)
@@ -64,10 +64,10 @@ class SumOfCubes { invariant i <= k;
invariant SumEmDown(0, i) == GSum(i) * GSum(i);
{
- call Lemma2(i);
+ Lemma2(i);
i := i + 1;
}
- call Lemma3(0, k);
+ Lemma3(0, k);
}
ghost static method Lemma2(k: int)
diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy index 49f5a075..0aa36a10 100644 --- a/Test/dafny1/TerminationDemos.dfy +++ b/Test/dafny1/TerminationDemos.dfy @@ -58,10 +58,10 @@ class Ackermann { if (m == 0) {
r := n + 1;
} else if (n == 0) {
- call r := ComputeAck(m - 1, 1);
+ r := ComputeAck(m - 1, 1);
} else {
- call s := ComputeAck(m, n - 1);
- call r := ComputeAck(m - 1, s);
+ var s := ComputeAck(m, n - 1);
+ r := ComputeAck(m - 1, s);
}
}
}
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index 61e86836..189ff2b5 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -22,9 +22,9 @@ class UltraFilter<G> { {
if (M !in f) {
// instantiate 'g' with the following 'h'
- call h := H(f, S, M);
- call Lemma_HIsFilter(h, f, S, M);
- call Lemma_FHOrdering0(h, f, S, M);
+ var h := H(f, S, M);
+ Lemma_HIsFilter(h, f, S, M);
+ Lemma_FHOrdering0(h, f, S, M);
}
}
@@ -44,9 +44,9 @@ class UltraFilter<G> { // call Lemma_H1(h, f, S, M, *, *);
assume (forall C, D :: C in h && D in h ==> C * D in h);
- call Lemma_H2(h, f, S, M);
+ Lemma_H2(h, f, S, M);
- call Lemma_H3(h, f, S, M);
+ Lemma_H3(h, f, S, M);
}
method Lemma_H0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, A: set<G>, B: set<G>)
diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy index 52cddaac..c7e4bc63 100644 --- a/Test/dafny1/pow2.dfy +++ b/Test/dafny1/pow2.dfy @@ -36,7 +36,7 @@ ghost method Lemma(n: int) ensures pow2_slow(n) == Square(pow2_slow(n/2));
{
if (n != 0) {
- call Lemma(n-2);
+ Lemma(n-2);
}
}
@@ -46,9 +46,9 @@ ghost method Theorem(n: int) {
if (n == 0) {
} else if (IsEven(n)) {
- call Lemma(n);
- call Theorem(n/2);
+ Lemma(n);
+ Theorem(n/2);
} else {
- call Theorem(n-1);
+ Theorem(n-1);
}
}
diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy index 95ad12fa..ed376931 100644 --- a/Test/vacid0/Composite.dfy +++ b/Test/vacid0/Composite.dfy @@ -44,7 +44,7 @@ class Composite { {
var delta := x - val;
val := x;
- call Adjust(delta, S, S);
+ Adjust(delta, S, S);
}
method Add(ghost S: set<Composite>, child: Composite, ghost U: set<Composite>)
@@ -73,7 +73,7 @@ class Composite { right := child;
}
child.parent := this;
- call Adjust(child.sum, S, S+U);
+ Adjust(child.sum, S, S+U);
}
method Dislodge(ghost S: set<Composite>)
@@ -97,7 +97,7 @@ class Composite { p.right := null;
}
var delta := -sum;
- call p.Adjust(delta, S - {this}, S);
+ p.Adjust(delta, S - {this}, S);
}
}
@@ -138,35 +138,35 @@ method Main() var c0 := new Composite.Init(57);
var c1 := new Composite.Init(12);
- call c0.Add({c0}, c1, {c1});
+ c0.Add({c0}, c1, {c1});
var c2 := new Composite.Init(48);
var c3 := new Composite.Init(48);
- call c2.Add({c2}, c3, {c3});
- call c0.Add({c0,c1}, c2, {c2,c3});
+ c2.Add({c2}, c3, {c3});
+ c0.Add({c0,c1}, c2, {c2,c3});
ghost var S := {c0, c1, c2, c3};
- call c1.Update(100, S);
- call c2.Update(102, S);
+ c1.Update(100, S);
+ c2.Update(102, S);
- call c2.Dislodge(S);
- call c2.Update(496, S);
- call c0.Update(0, S);
+ c2.Dislodge(S);
+ c2.Update(496, S);
+ c0.Update(0, S);
}
method Harness() {
var a := new Composite.Init(5);
var b := new Composite.Init(7);
- call a.Add({a}, b, {b});
+ a.Add({a}, b, {b});
assert a.sum == 12;
- call b.Update(17, {a,b});
+ b.Update(17, {a,b});
assert a.sum == 22;
var c := new Composite.Init(10);
- call b.Add({a,b}, c, {c});
- call b.Dislodge({a,b,c});
+ b.Add({a,b}, c, {c});
+ b.Dislodge({a,b,c});
assert b.sum == 27;
}
diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy index 2c217264..989ddfc6 100644 --- a/Test/vacid0/SparseArray.dfy +++ b/Test/vacid0/SparseArray.dfy @@ -37,11 +37,9 @@ class SparseArray<T> { ensures |Contents| == N && this.zero == zero;
ensures (forall x :: x in Contents ==> x == zero);
{
- var aa;
- var ii;
- call aa := AllocateArray(N); this.a := aa;
- call ii := AllocateArray(N); this.b := ii;
- call ii := AllocateArray(N); this.c := ii;
+ var aa := AllocateArray(N); this.a := aa;
+ var bb := AllocateArray(N); this.b := bb;
+ bb := AllocateArray(N); this.c := bb;
this.n := 0;
// initialize ghost variable Contents to a sequence of length N containing only zero's,
|