From 43e00a07c7b28d7f51081b4cac736af0f3481600 Mon Sep 17 00:00:00 2001
From: stefanheule <unknown>
Date: Sat, 25 Feb 2012 03:33:46 -0800
Subject: Chalice: New test case for predicates.

---
 Chalice/tests/predicates/test8.chalice | 55 ++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100644 Chalice/tests/predicates/test8.chalice

(limited to 'Chalice/tests/predicates/test8.chalice')

diff --git a/Chalice/tests/predicates/test8.chalice b/Chalice/tests/predicates/test8.chalice
new file mode 100644
index 00000000..e824f161
--- /dev/null
+++ b/Chalice/tests/predicates/test8.chalice
@@ -0,0 +1,55 @@
+// fold/unfold in various combinations
+class FUFU
+{
+  var value:int;
+  var next:FUFU;
+  
+  predicate inv { acc(value) }
+  
+  predicate tinv { acc(value) && acc(next) && (next!=null ==> next.tinv) }
+  
+  function get():int
+    requires tinv;
+  { unfolding tinv in value }
+
+  method fufu()
+    requires acc(value);
+  {
+    fold inv;
+    unfold inv;
+    fold inv;
+    unfold inv;
+  }
+  
+  method fuf()
+    requires acc(value);
+  {
+    fold inv;
+    unfold inv;
+    fold inv;
+  }  
+  
+  method uf()
+    requires inv;
+  {
+    unfold inv;
+    fold inv;
+  }
+  
+  method fu()
+    requires acc(value);
+  {
+    fold inv;
+    unfold inv;
+  }
+  
+  method t()
+    requires tinv && unfolding tinv in next!=null;
+    ensures tinv && unfolding tinv in next!=null;
+  {
+    unfold tinv;
+    unfold next.tinv;
+    fold next.tinv;
+    fold tinv;
+  }
+}
\ No newline at end of file
-- 
cgit v1.2.3