summaryrefslogtreecommitdiff
path: root/Chalice/tests/refinements/TestRefines.chalice
diff options
context:
space:
mode:
Diffstat (limited to 'Chalice/tests/refinements/TestRefines.chalice')
-rw-r--r--Chalice/tests/refinements/TestRefines.chalice56
1 files changed, 0 insertions, 56 deletions
diff --git a/Chalice/tests/refinements/TestRefines.chalice b/Chalice/tests/refinements/TestRefines.chalice
deleted file mode 100644
index 40f21cea..00000000
--- a/Chalice/tests/refinements/TestRefines.chalice
+++ /dev/null
@@ -1,56 +0,0 @@
-// Simple refinements
-class A {
- var x:int;
- function f():int {1}
- method m(i:int) returns (j:int) {
- var j [j > 0];
- }
-
- method n() returns (c: bool)
- {
- c := true;
- }
-
- method o() returns ()
- {
- var k := 1;
- var j := 0;
- spec j [j > 0];
- }
-
- method p(b: bool) returns ()
- {
- var k := 1;
- if (b) {
- } else {
- }
- }
-}
-
-class B refines A {
- // correct
- transforms m(i:int) returns (j:int, k:int)
- {
- *
- }
-
- // broken: c
- refines n() returns (c: bool)
- {
- c := false;
- }
-
- // broken: spec stmt frame, k
- transforms o() returns () {
- _
- replaces j by { j := 1; k := 0 }
- }
-
- // broken: k
- transforms p(b: bool) returns () {
- _
- if {k := 2} else {*}
- }
-}
-
-