diff options
author | Rustan Leino <leino@microsoft.com> | 2012-09-26 00:09:04 -0700 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2012-09-26 00:09:04 -0700 |
commit | 225930765d1f6c11dcf6c523ce0730457c07ec47 (patch) | |
tree | 5ea7ecbd4e5a972ea27c64dc5a6f1004647603fc /Test/dafny0 | |
parent | 3aac24b3f84b0c969e08a13aee01c75457c43851 (diff) |
Dafny: compile iterators
Diffstat (limited to 'Test/dafny0')
-rw-r--r-- | Test/dafny0/Answer | 7 | ||||
-rw-r--r-- | Test/dafny0/IteratorResolution.dfy | 2 | ||||
-rw-r--r-- | Test/dafny0/Iterators.dfy | 30 | ||||
-rw-r--r-- | Test/dafny0/runtest.bat | 2 |
4 files changed, 39 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 9025e206..bde6a07c 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1620,7 +1620,12 @@ IteratorResolution.dfy(56,11): Error: LHS of assignment does not denote a mutabl 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
+IteratorResolution.dfy(76,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called
+5 resolution/type errors detected in IteratorResolution.dfy
+
+-------------------- Iterators.dfy --------------------
+
+Dafny program verifier finished with 8 verified, 0 errors
-------------------- Superposition.dfy --------------------
diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy index f45dd764..fe9e2563 100644 --- a/Test/dafny0/IteratorResolution.dfy +++ b/Test/dafny0/IteratorResolution.dfy @@ -72,6 +72,8 @@ module Mx { } else {
var x: int := h1.t; // error: h1 would have to be a GenericIteratorResult<int>
}
+
+ var h2 := new GenericIteratorResult; // error: constructor is not mentioned
}
}
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy new file mode 100644 index 00000000..76a30330 --- /dev/null +++ b/Test/dafny0/Iterators.dfy @@ -0,0 +1,30 @@ +iterator MyIter<T>(q: T) yields (x: T, y: T)
+{
+}
+
+iterator MyIntIter() yields (x: int, y: int)
+{
+ x, y := 0, 0;
+ yield;
+ yield 2, 3;
+ x, y := y, x;
+ yield;
+}
+
+method Main() {
+ var m := new MyIter.MyIter(12);
+ var a := m.x;
+ // assert !a; // error: type mismatch
+ if (a <= 13) {
+ print "-- ", m.x, " --\n";
+ }
+
+ var n := new MyIntIter.MyIntIter();
+ var patience := 10;
+ while (patience != 0) {
+ var more := n.MoveNext();
+ if (!more) { break; }
+ print n.x, ", ", n.y, "\n";
+ patience := patience - 1;
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index b602f089..9789e7d7 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -24,7 +24,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy
RefinementModificationChecking.dfy TailCalls.dfy
- IteratorResolution.dfy) do (
+ IteratorResolution.dfy Iterators.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
|