summaryrefslogtreecommitdiff
path: root/Test/dafny0/Skeletons.dfy
blob: e9fef946be31ad97e644226e0fe716a13ab1eb87 (plain)
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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
module A {
  method M(p: int) returns (y: int)
    requires p <= 30;
  {
    assume p < 100;
    var x;
    assume x == p + 20;
    x := x + 1;
    while (*)
      invariant x <= 120;
      decreases 120 - x;
    {
      if (x == 120) { break; }
      x := x + 1;
    }
    y := x;
  }
}

module B refines A {
  method M ...
  {
    assert p < 50;
    assert ...;
    var x := p + 20;
    assert ...;
    var k := x + 1;
    ...;
    while ...
      invariant k == x;
    {
      k := k + 1;
    }
    assert k == x || k == x + 1;  // there are two exits from the loop
  }
}


module C0 refines B {
  method M ...
    ensures y == 120;  // error: this holds only if the loop does not end early
  {
  }
}

module C1 refines B {
  method M ...
    ensures y <= 120;
  {
  }
}

module C2 refines B {
  method M ...
    ensures y == 120;
  {
    ...;
    while (true)
      ...
    assert k == x + 1;  // only one loop exit remains
    ...;
  }
}