diff options
author | kyessenov <unknown> | 2010-08-23 22:27:06 +0000 |
---|---|---|
committer | kyessenov <unknown> | 2010-08-23 22:27:06 +0000 |
commit | 65da7c1240c91692ae873dda6a1138887ae7d41a (patch) | |
tree | e5eaf3d60f7c59060b7467ffe76c23e6643b00b0 /Chalice/refinements | |
parent | 5c779b7e1542cdedccf00ba0cd056d6de6435d6c (diff) |
Chalice: exhale spec statement post condition in refinement block translation; tag global coupling assertions (bug fix)
Diffstat (limited to 'Chalice/refinements')
-rw-r--r-- | Chalice/refinements/Counter.chalice | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/Chalice/refinements/Counter.chalice b/Chalice/refinements/Counter.chalice index 16cd8473..f2184a2d 100644 --- a/Chalice/refinements/Counter.chalice +++ b/Chalice/refinements/Counter.chalice @@ -49,7 +49,12 @@ class Counter1 refines Counter0 { refines dec() { this.z := this.z + 1; - } + } + + refines magic() returns (c: Cell) + { + c := new Cell; + } } class Cell {var n: int} @@ -82,6 +87,11 @@ class Counter2 refines Counter0 { { this.b.n := this.b.n + 1; } + + refines magic() returns (c: Cell) + { + c := a; + } } class Client { |