diff options
Diffstat (limited to 'Chalice/tests/predicates/test8.chalice')
-rw-r--r-- | Chalice/tests/predicates/test8.chalice | 55 |
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 |