diff options
author | kyessenov <unknown> | 2010-08-22 06:43:51 +0000 |
---|---|---|
committer | kyessenov <unknown> | 2010-08-22 06:43:51 +0000 |
commit | 747f201231e03caee7289d03b1e2a29dacae7635 (patch) | |
tree | 44cf955af674583affc0a9b320b79add5a3d6828 /Chalice/refinements | |
parent | 801a3e92beeb731a776ea2986c5a4477882d7a61 (diff) |
Chalice:
* coupling invariants work (with certain restrictions as described in TODO comments)
Diffstat (limited to 'Chalice/refinements')
-rw-r--r-- | Chalice/refinements/Answer | 6 | ||||
-rw-r--r-- | Chalice/refinements/Counter.chalice | 125 | ||||
-rw-r--r-- | Chalice/refinements/TestCoupling.chalice | 74 | ||||
-rw-r--r-- | Chalice/refinements/test.sh | 1 |
4 files changed, 206 insertions, 0 deletions
diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer index b513e041..6db2a988 100644 --- a/Chalice/refinements/Answer +++ b/Chalice/refinements/Answer @@ -29,3 +29,9 @@ Processing Pick.chalice 26.25: Sequence index might be larger than or equal to the length of the sequence.
Boogie program verifier finished with 11 verified, 1 error
+Processing TestCoupling.chalice + 35.13: The postcondition at 35.13 might not hold. Insufficient fraction at 35.13 for A1.y.
+ 62.38: Location might not be readable.
+ 66.5: Location might not be writable
+
+Boogie program verifier finished with 17 verified, 3 errors
diff --git a/Chalice/refinements/Counter.chalice b/Chalice/refinements/Counter.chalice new file mode 100644 index 00000000..c9576a13 --- /dev/null +++ b/Chalice/refinements/Counter.chalice @@ -0,0 +1,125 @@ +class Counter0 { + var x: int; + + method init() + requires acc(x); + ensures acc(x) && x == 0; + { + x := 0; + } + + method inc() + requires acc(x); + ensures acc(x) && x == old(x) + 1; + { + x := x + 1; + } + + method dec() + requires acc(x); + ensures acc(x) && x == old(x) - 1; + { + x := x - 1; + } + + /** Interesting issues */ + + /* We can expose representation here */ + method magic1() returns (c: Cell) + requires acc(x) + ensures acc(c.n) && x == old(x); + { + var c [acc(c.n)]; + } + + /* This should prevent us from exposing representation */ + method magic2() returns (c: Cell) + requires acc(x); + ensures acc(x) && x == old(x) && acc(c.n); + { + var c [acc(c.n)]; + } +} + +class Counter1 refines Counter0 { + var y: int; + var z: int; + replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0; + + transforms init() + { + replaces * by {this.y := 0; this.z := 0;} + } + + transforms inc() + { + replaces * by {this.y := this.y + 1;} + } + + transforms dec() + { + replaces * by {this.z := this.z + 1;} + } + + /** This violates abstraction of x -- we must hold all permissions to x to update it */ + method magic3() + requires acc(y); + { + y := y + 1; + } + + /** This does also -- but it also prohibits us from reading part of the state across refinement */ + method magic4() returns (i) + requires acc(y); + { + i := y; + } +} + +class Cell {var n: int} +/* +class Counter2 refines Counter1 { + var a: Cell; + var b: Cell; + replaces y, z by acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n; + + transforms init() + { + replaces * by { + this.a := new Cell {n := 0}; + this.b := new Cell {n := 0}; + } + } + + transforms inc() + { + replaces * by {this.a.n := this.a.n + 1;} + } + + transforms dec() + { + replaces * by {this.b.n := this.b.n + 1;} + } + + transforms magic1() returns (c: Cell) + { + replaces * by {c := this.a;} + } + + transforms magic2() returns (c: Cell) + { + replaces * by {c := this.a;} + } + + transforms magic3() + { + replaces * by {this.a.n := this.a.n + 1;} + } + + transforms magic4() returns (i) + { + replaces * by {i := this.a.n;} + } +} +*/ + diff --git a/Chalice/refinements/TestCoupling.chalice b/Chalice/refinements/TestCoupling.chalice new file mode 100644 index 00000000..a178c9b4 --- /dev/null +++ b/Chalice/refinements/TestCoupling.chalice @@ -0,0 +1,74 @@ +class A0 { + var x: int; + var n: int; + var k: int; + + method inc() + requires acc(x) && acc(n); + ensures acc(x) && x == old(x) + 1; + { + x := x + 1; + n := n + 1; + } + + method error() + requires acc(x) + ensures acc(x) + { + x := x + 1; + } +} + +class A1 refines A0 { + var y: int; + var z: int; + replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0; + + refines inc() + ensures y == old(y) + 1 + { + this.y := 1 + this.y; + this.n := this.n + 1; + } + + refines error() + ensures acc(y) + { + this.y := 1 + this.y; + } +} + +class B0 { + var x: int; + var y: int; + + method error() + requires acc(x); + ensures acc(x); + { + x := x + 1; + } + + method inc() + requires acc(x) && acc(y); + ensures acc(x) && acc(y); + { + x := x + 1; + } +} + +class B1 refines B0 { + var z: int; + replaces x,y by acc(z) && z == x + y; + + refines error() + { + this.z := this.z + 1; + } + + refines inc() + { + this.z := this.z + 1; + } +} + diff --git a/Chalice/refinements/test.sh b/Chalice/refinements/test.sh index 73ede390..24dbd6e5 100644 --- a/Chalice/refinements/test.sh +++ b/Chalice/refinements/test.sh @@ -13,6 +13,7 @@ TESTS=" RecFiniteDiff.chalice LoopFiniteDiff.chalice Pick.chalice + TestCoupling.chalice " # Switch to test directory |