diff options
| author |  Unknown <Alex@Mehldau.ethz.ch> | 2012-05-21 16:39:34 +0200 |
|---|---|---|
| committer | Unknown <Alex@Mehldau.ethz.ch> | 2012-05-21 16:39:34 +0200 |
| commit | c7e55e700397fdf1fb164006c88f96d0710ae3bf (patch) | |
| tree | 3ced0e9f72deeaec4ea9afaee0ec64e17be6d534 /Chalice/tests | |
| parent | a4f7fb313defb8bfef531e6ccf66f56e53bf5b16 (diff) | |
Chalice: Added list reversal example, along with variants with extra unfold/fold pairs which currently confuse the encoding.
Diffstat (limited to 'Chalice/tests')
| -rw-r--r-- | Chalice/tests/predicates/list-reverse.chalice | 158 | ||||
| -rw-r--r-- | Chalice/tests/predicates/list-reverse.output.txt | 4 |
2 files changed, 162 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/list-reverse.chalice b/Chalice/tests/predicates/list-reverse.chalice new file mode 100644 index 00000000..5a596409 --- /dev/null +++ b/Chalice/tests/predicates/list-reverse.chalice @@ -0,0 +1,158 @@ +// this would be nice in the "examples" folder (at least, the version without the commented blocks), once the problem with old(..) is fixed
+
+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 true;
+ {
+ var l : Node := this;
+ r := null;
+
+ var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant rev == (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;
+ }
+ assert r.vals() == rev; // should be the post-condition
+ }
+
+
+ method reverse_in_place_01() returns (r:Node)
+ requires list;
+ ensures true;
+ {
+ var l : Node := this;
+ r := null;
+
+ var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant rev == (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;
+ }
+ assert r.vals() == rev; // should be the post-condition
+ }
+
+
+
+ method reverse_in_place_10() returns (r:Node)
+ requires list;
+ ensures true;
+ {
+ var l : Node := this;
+ r := null;
+
+ var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant rev == (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;
+ }
+ assert r.vals() == rev; // should be the post-condition
+ }
+
+
+
+
+ method reverse_in_place_11() returns (r:Node)
+ requires list;
+ ensures true;
+ {
+ var l : Node := this;
+ r := null;
+
+ var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant rev == (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;
+ }
+ assert r.vals() == rev; // should be the post-condition
+ }
+
+
+}
\ No newline at end of file diff --git a/Chalice/tests/predicates/list-reverse.output.txt b/Chalice/tests/predicates/list-reverse.output.txt new file mode 100644 index 00000000..d8e19122 --- /dev/null +++ b/Chalice/tests/predicates/list-reverse.output.txt @@ -0,0 +1,4 @@ +Verification of list-reverse.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings.
|