diff options
Diffstat (limited to 'Chalice/refinements/TestTransform.chalice')
-rw-r--r-- | Chalice/refinements/TestTransform.chalice | 38 |
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; + } + } +} |