Chalice: more regression tests; cosmetic changes to code

1 files changed, 28 insertions, 0 deletions

diff --git a/Chalice/refinements/Pick.chalice b/Chalice/refinements/Pick.chalice
new file mode 100644
index 00000000..7df2f90d
--- /dev/null
+++ b/Chalice/refinements/Pick.chalice
@@ -0,0 +1,28 @@
+class Pick0 {
+  method pick(s: seq<int>) returns (x)
+    requires |s| > 0;
+  {
+    var x [x in s]
+  }
+}
+
+class Pick1 refines Pick0 {
+  transforms pick(s: seq<int>) returns (x)
+  {
+    replaces x by {x := s[0]}
+  }
+}
+
+class Pick2 refines Pick0 {
+  transforms pick(s: seq<int>) returns (x)
+  {
+    replaces * by {x := s[|s|-1]}
+  }
+}
+
+class Pick3 refines Pick0 {
+  transforms pick(s: seq<int>) returns (x)
+  {
+    replaces x by {x := s[1]}
+  }
+}