summaryrefslogtreecommitdiff
path: root/Chalice/tests/predicates/test8.chalice
diff options
context:
space:
mode:
Diffstat (limited to 'Chalice/tests/predicates/test8.chalice')
-rw-r--r--Chalice/tests/predicates/test8.chalice55
1 files changed, 0 insertions, 55 deletions
diff --git a/Chalice/tests/predicates/test8.chalice b/Chalice/tests/predicates/test8.chalice
deleted file mode 100644
index e824f161..00000000
--- a/Chalice/tests/predicates/test8.chalice
+++ /dev/null
@@ -1,55 +0,0 @@
-// 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