Test/dafny0/DirtyLoops.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
31
32
33
34
35
36

// RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"
// RUN: %dafny /noVerify /compile:1 "%t.dprint.dfy" >> "%t"
// RUN: %diff "%s.expect" "%t"

class MyClass {
  method M0(S: set<int>) {
    forall s | s in S ensures s < 0;
  }

  method M1(x: int)
  {
    var i := x;
    while (0 < i)
      invariant i <= x;
  }

  method M2(x: int)
  {
    var i := x;
    while (0 < i)
      invariant i <= x;
      decreases i;
  }

  var f: int;

  method M3(x: int)
    requires f <= x;
    modifies `f;
  {
    while (0 < f)
      invariant f <= x;
      decreases f;
      modifies `f;
  }
}