diff options
| author |  Unknown <Alex@Mingus> | 2012-07-26 10:45:17 +0200 |
|---|---|---|
| committer | Unknown <Alex@Mingus> | 2012-07-26 10:45:17 +0200 |
| commit | 666d6e85b0142dbc9ecc9cee9d92032054d71ec9 (patch) | |
| tree | 11fbc6daf77199603fdc29af9ec3428d5ea562a5 | |
| parent | 9e10d0edb20de0a5599f65fac26b0c4889cd070e (diff) | |
Added variant of list reverse example (see tests/examples/list-reverse.chalice) with extra unfold/fold pairs (this used to break an intermediate version of the functions encoding).
| -rw-r--r-- | Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice | 51 | ||||
| -rw-r--r-- | Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt | 4 |
2 files changed, 55 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice new file mode 100644 index 00000000..8467ce4c --- /dev/null +++ b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.chalice @@ -0,0 +1,51 @@ +class Node {
+ var next : Node;
+ var val : int;
+
+ predicate list {
+ acc(next) && acc(val) && (next!=null ==> next.list)
+ }
+
+ function vals() : seq<int>
+ requires list
+ {
+ unfolding list in (next == null ? [val] : [val] ++ next.vals())
+ }
+
+ function reverse_vals() : seq<int>
+ requires list
+ {
+ unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])
+ }
+
+ method reverse_in_place() returns (r:Node)
+ requires list;
+ ensures r != null && r.list;
+ ensures r.vals() == old(this.reverse_vals());
+ {
+ var l : Node := this;
+ r := null;
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant old(this.reverse_vals()) == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+ {
+ var y: Node;
+ if (r != null) {
+ unfold r.list; fold r.list;
+ }
+ unfold l.list;
+ if (l.next != null) {
+ unfold l.next.list; fold l.next.list;
+ }
+
+
+ y := l.next;
+ l.next := r;
+ r := l;
+ fold r.list;
+ l := y;
+ }
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt new file mode 100644 index 00000000..fc4d63fa --- /dev/null +++ b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt @@ -0,0 +1,4 @@ +Verification of list-reverse-extra-unfold-fold.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings.
|