diff options
Diffstat (limited to 'Chalice/refinements/Counter.chalice')
| -rw-r--r-- | Chalice/refinements/Counter.chalice | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/Chalice/refinements/Counter.chalice b/Chalice/refinements/Counter.chalice index f2184a2d..d1efae76 100644 --- a/Chalice/refinements/Counter.chalice +++ b/Chalice/refinements/Counter.chalice @@ -24,7 +24,7 @@ class Counter0 { method magic() returns (c: Cell) requires acc(x); - ensures acc(x) && acc(c.n) + ensures acc(x) && acc(c.n) && x == old(x); { var c [acc(c.n)] } @@ -85,7 +85,9 @@ class Counter2 refines Counter0 { refines dec() { - this.b.n := this.b.n + 1; + var i := this.b.n + 1; + this.b := new Cell; + this.b.n := i; } refines magic() returns (c: Cell) @@ -102,6 +104,8 @@ class Client { call c.inc(); call c.inc(); call c.dec(); + call d := c.magic(); + d.n := 100; assert c.x == 1; } } |