Test/dafny0/Iterators.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
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;
  }
}