diff options
| author |  rustanleino <unknown> | 2010-09-01 02:18:50 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-09-01 02:18:50 +0000 |
| commit | 9fe20e5de05378f3d570df17a80ad0cbe32e5e54 (patch) | |
| tree | a7afcf833e013c0b96f2b61fe8f65f3021cb4cec /Test/VSComp2010/Problem3-FindZero.dfy | |
| parent | f2acf182c42f371b1075c0fd71885eb9cecb870c (diff) | |
Dafny: Added Dafny solutions to the VSComp 2010 problems
Diffstat (limited to 'Test/VSComp2010/Problem3-FindZero.dfy')
| -rw-r--r-- | Test/VSComp2010/Problem3-FindZero.dfy | 92 |
1 files changed, 92 insertions, 0 deletions
diff --git a/Test/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy new file mode 100644 index 00000000..03e6bdfe --- /dev/null +++ b/Test/VSComp2010/Problem3-FindZero.dfy @@ -0,0 +1,92 @@ +// VSComp 2010, problem 3, find a 0 in a linked list and return how many nodes were skipped
+// until the first 0 (or end-of-list) was found.
+// Rustan Leino, 18 August 2010.
+//
+// The difficulty in this problem lies in specifying what the return value 'r' denotes and in
+// proving that the program terminates. Both of these are addressed by declaring a ghost
+// field 'List' in each linked-list node, abstractly representing the linked-list elements
+// from the node to the end of the linked list. The specification can now talk about that
+// sequence of elements and can use 'r' as an index into the sequence, and termination can
+// be proved from the fact that all sequences in Dafny are finite.
+//
+// We only want to deal with linked lists whose 'List' field is properly filled in (which
+// can only happen in an acyclic list, for example). To that avail, the standard idiom in
+// Dafny is to declare a predicate 'Valid()' that is true of an object when the data structure
+// representing object's abstract value is properly formed. The definition of 'Valid()'
+// is what one intuitively would think of as the ''object invariant'', and it is mentioned
+// explicitly in method pre- and postconditions. As part of this standard idiom, one also
+// declared a ghost variable 'Repr' that is maintained as the set of objects that make up
+// the representation of the aggregate object--in this case, the Node itself and all its
+// successors.
+
+class Node {
+ ghost var List: seq<int>;
+ ghost var Repr: set<Node>;
+ var head: int;
+ var next: Node;
+
+ function Valid(): bool
+ reads this, Repr;
+ {
+ this in Repr &&
+ 1 <= |List| && List[0] == head &&
+ (next == null ==> |List| == 1) &&
+ (next != null ==>
+ next in Repr && next.Repr <= Repr && this !in next.Repr && next.Valid() && next.List == List[1..])
+ }
+
+ static method Cons(x: int, tail: Node) returns (n: Node)
+ requires tail == null || tail.Valid();
+ ensures n != null && n.Valid();
+ ensures if tail == null then n.List == [x] else n.List == [x] + tail.List;
+ {
+ n := new Node;
+ n.head := x;
+ n.next := tail;
+ if (tail == null) {
+ n.List := [x];
+ n.Repr := {n};
+ } else {
+ n.List := [x] + tail.List;
+ n.Repr := {n} + tail.Repr;
+ }
+ }
+}
+
+static method Search(ll: Node) returns (r: int)
+ requires ll == null || ll.Valid();
+ ensures ll == null ==> r == 0;
+ ensures ll != null ==>
+ 0 <= r && r <= |ll.List| &&
+ (r < |ll.List| ==> ll.List[r] == 0 && 0 !in ll.List[..r]) &&
+ (r == |ll.List| ==> 0 !in ll.List);
+{
+ if (ll == null) {
+ r := 0;
+ } else {
+ var jj := ll;
+ var i := 0;
+ while (jj != null && jj.head != 0)
+ invariant jj != null ==> jj.Valid() && i + |jj.List| == |ll.List| && ll.List[i..] == jj.List;
+ invariant jj == null ==> i == |ll.List|;
+ invariant 0 !in ll.List[..i];
+ decreases |ll.List| - i;
+ {
+ jj := jj.next;
+ i := i + 1;
+ }
+ r := i;
+ }
+}
+
+method Main()
+{
+ var list: Node := null;
+ call list := list.Cons(0, list);
+ call list := list.Cons(5, list);
+ call list := list.Cons(0, list);
+ call list := list.Cons(8, list);
+ call r := Search(list);
+ print "Search returns ", r, "\n";
+ assert r == 1;
+}
|