diff options
| author |  Rustan Leino <unknown> | 2014-04-04 10:11:10 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-04 10:11:10 -0700 |
| commit | 0abbaee631e42479bba3cf98cb9a41fdf0f9358d (patch) | |
| tree | f9886c2f1ecd889739954b78e54f5ef977180818 /Test/dafny4/ClassRefinement.dfy | |
| parent | d6efe85276f21ab3ea2b04d7e6b3c2bfb1acd22e (diff) | |
Support the transition from "modify Frame;" to "modify Frame { Body }" by refinement.
Diffstat (limited to 'Test/dafny4/ClassRefinement.dfy')
| -rw-r--r-- | Test/dafny4/ClassRefinement.dfy | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/Test/dafny4/ClassRefinement.dfy b/Test/dafny4/ClassRefinement.dfy new file mode 100644 index 00000000..4fc29122 --- /dev/null +++ b/Test/dafny4/ClassRefinement.dfy @@ -0,0 +1,77 @@ +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>;
+ predicate Valid()
+ reads this, Repr;
+ {
+ this in Repr
+ }
+
+ constructor Init()
+ modifies this;
+ ensures N == 0;
+ ensures Valid() && fresh(Repr - {this});
+ {
+ Repr := {};
+ assert {this} <= {this} && fresh({this} - {this});
+ 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;
+ }
+
+ 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;
+ 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...
+ {
+ c.data := c.data + 1;
+ }
+
+ method Get...
+ {
+ n := c.data - d.data;
+ }
+ }
+}
|