diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-09-25 21:54:16 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-09-25 21:54:16 -0700 |
| commit | 8e3eccb18beeb045ff0bb6908854b5f966aab69c (patch) | |
| tree | 6e7e07db1929cd1a16ee452499d10bb96ddfea85 | |
| parent | b07e9cbb6bf486f789eeee0bbe34dc7c10ef159a (diff) | |
Dafny: added test cases for resolving iterators
| -rw-r--r-- | Test/dafny0/Answer | 7 | ||||
| -rw-r--r-- | Test/dafny0/IteratorResolution.dfy | 98 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 3 |
3 files changed, 107 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 0dfb0be4..9025e206 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1615,6 +1615,13 @@ TailCalls.dfy(42,12): Error: 'decreases *' is allowed only on tail-recursive met TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive methods
5 resolution/type errors detected in TailCalls.dfy
+-------------------- IteratorResolution.dfy --------------------
+IteratorResolution.dfy(56,11): Error: LHS of assignment does not denote a mutable field
+IteratorResolution.dfy(57,11): Error: LHS of assignment does not denote a mutable field
+IteratorResolution.dfy(61,18): Error: arguments must have the same type (got _T0 and int)
+IteratorResolution.dfy(73,19): Error: RHS (of type bool) not assignable to LHS (of type int)
+4 resolution/type errors detected in IteratorResolution.dfy
+
-------------------- Superposition.dfy --------------------
Verifying CheckWellformed$$_0_M0.C.M ...
diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy new file mode 100644 index 00000000..f45dd764 --- /dev/null +++ b/Test/dafny0/IteratorResolution.dfy @@ -0,0 +1,98 @@ +iterator MyIter()
+
+module Mx {
+
+ iterator ExampleIterator(k: int) yields (x: int, y: int)
+ {
+ var i := k;
+ while (true) {
+ if (i % 77 == 0) { yield; }
+ yield i, -i;
+ i := i + 1;
+ }
+ }
+
+ method IteratorUser() {
+ var iter := new ExampleIterator.ExampleIterator(15);
+ var j := 0;
+ while (j < 100) {
+ var more := iter.MoveNext();
+ if (!more) {
+ break;
+ }
+ print iter.x, iter.y;
+ j := j + 1;
+ }
+ }
+
+ static method StaticM(k: nat) returns (m: int)
+ {
+ m := k;
+ }
+
+ module Inner {
+ iterator YetAnother(x: int, y: int, z: int) yields (a: bool, b: bool)
+ requires true;
+ }
+
+ class Client {
+ method M() {
+ var m := StaticM(5);
+ var it := new ExampleIterator.ExampleIterator(100);
+ var a, b := Worker(it);
+ }
+ method Worker(xi: ExampleIterator) returns (k: int, m: int) {
+ k, m := xi.k + xi.x, xi.y;
+ var mr := xi.MoveNext();
+ if (mr) {
+ k := xi.x;
+ } else {
+ assert k == xi.k + xi.x && m == xi.y;
+ }
+ }
+ method GenericTester(g0: GenericIterator<bool>, g2: GenericIterator)
+ requires g0.u;
+ {
+ g0.t := true; // error: not allowed to assign to .t
+ g0.u := true; // error: not allowed to assign to .u
+ var g1 := new GenericIterator.GenericIterator(20);
+ assert g1.u < 200; // .u is an integer
+
+ assert g2.u == 200; // error: the type parameter of g2 is unknown
+
+ var h0 := new GenericIteratorResult.GenericIteratorResult();
+ // so far, the instantiated type of h0 is unknown
+ var k := h0.t;
+ assert k < 87;
+
+ var h1 := new GenericIteratorResult.GenericIteratorResult();
+ // so far, the instantiated type of h1 is unknown
+ if (*) {
+ var b: bool := h1.t; // this determines h1 to be of type GenericIteratorResult<bool>
+ } else {
+ var x: int := h1.t; // error: h1 would have to be a GenericIteratorResult<int>
+ }
+ }
+ }
+
+ iterator GenericIterator<T>(t: T) yields (u: T)
+ {
+ while (true) {
+ yield t;
+ }
+ }
+
+ iterator GenericIteratorResult<T>() yields (t: T)
+ {
+ while (*) { yield; }
+ }
+
+ class AnotherClient {
+ method StaticM(b: bool) // [sic]
+ {
+ }
+ method Q() {
+ StaticM(true); // this is supposed to resolve to AnotherClient.StaticM, not _default.StaticM
+ }
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 2055e283..b602f089 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -23,7 +23,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy
- RefinementModificationChecking.dfy TailCalls.dfy) do (
+ RefinementModificationChecking.dfy TailCalls.dfy
+ IteratorResolution.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
|