1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// 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;
}
}
}
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;
list := list.Cons(0, list);
list := list.Cons(5, list);
list := list.Cons(0, list);
list := list.Cons(8, list);
var r := Search(list);
print "Search returns ", r, "\n";
assert r == 1;
}
|
