summaryrefslogtreecommitdiff
path: root/Chalice/refinements/TestTransform.chalice
diff options
context:
space:
mode:
Diffstat (limited to 'Chalice/refinements/TestTransform.chalice')
-rw-r--r--Chalice/refinements/TestTransform.chalice38
1 files changed, 38 insertions, 0 deletions
diff --git a/Chalice/refinements/TestTransform.chalice b/Chalice/refinements/TestTransform.chalice
new file mode 100644
index 00000000..2c18907f
--- /dev/null
+++ b/Chalice/refinements/TestTransform.chalice
@@ -0,0 +1,38 @@
+class A {
+ method m(i: int) returns (x: int)
+ ensures x == i;
+ {
+ var j := 0;
+ var v [v == i + j];
+ x := v;
+ }
+
+ method n() {
+ var x := 0;
+ var y := 1;
+ var z := 2;
+ }
+}
+
+class B refines A {
+ transforms m(i: int) returns (x: int, y: int)
+ ensures y == 0;
+ {
+ var t := 0;
+ _
+ replaces v by {
+ var v := i + j;
+ call t, j := m(0);
+ y := j;
+ }
+ _
+ }
+
+ transforms n() {
+ replaces * by {
+ var x := 0;
+ var y := x + 1;
+ var z := 2*y;
+ }
+ }
+}