Test/dafny4/ClassRefinement.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
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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83

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

abstract module M0 {
  class Cell {
    var data: int;
    constructor (d: int)
      modifies this;
      ensures data == d;
    { data := d; }
  }
  class Counter {
    ghost var N: int;
    ghost var Repr: set<object>;
    protected predicate Valid()
      reads this, Repr;
    {
      this in Repr
    }

    constructor Init()
      modifies this;
      ensures N == 0;
      ensures Valid() && fresh(Repr - {this});
    {
      Repr := {};
      ghost var repr :| {this} <= repr && fresh(repr - {this});
      N, Repr := 0, repr;
    }

    method Inc()
      requires Valid();
      modifies Repr;
      ensures N == old(N) + 1;
      ensures Valid() && fresh(Repr - old(Repr));
    {
      N := N + 1;
      modify Repr - {this};
    }

    method Get() returns (n: int)
      requires Valid();
      ensures n == N;
    {
      n :| assume n == N;
    }
  }
}

module M1 refines M0 {
  class Counter {
    var c: Cell;
    var d: Cell;
    protected predicate Valid...
    {
      c != null && c in Repr &&
      d != null && d in Repr &&
      c != d &&
      N == c.data - d.data
    }

    constructor Init...
    {
      c := new Cell(0);
      d := new Cell(0);
      ...;
      ghost var repr := Repr + {this} + {c,d};
    }

    method Inc...
    {
      ...;
      modify ... {
        c.data := c.data + 1;
      }
    }

    method Get...
    {
      n := c.data - d.data;
    }
  }
}