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

#include <vcc.h>
#include <stdlib.h>

typedef
/*D_tag node */
struct node {
  int key;
  struct node * next;
} Node;

/*D_defs 
define pred list^(x): 
  ( ((x l= nil) & emp) 
  | ((x |-> loc next: nxt; int key: ky) * list^(nxt))  )
  axiom: (lseg^(x, x) * (((x l= nil) & (keys^(x) s= emptyset)) | ((~ (x l= nil)) & (~ (keys^(x) s= emptyset)))));
  
define set-fun keys^(x):
  (case (x l= nil): emptyset;
   case ((x |-> loc next: nxt; int key: ky) * true): ((singleton ky) union keys^(nxt));
   default: emptyset) ;

define relation lseg^(head, tail): 
  ( ((head l= tail) & emp) 
  | ((head |-> loc next: nxt; int key: ky) * (lseg^(nxt, tail) & (ky le-set lseg-keys^(nxt, tail))))) 
  axiom: ( (((head l= tail) => (emp & (lseg-keys^(head, tail) s= emptyset))) & ((tail l= nil) => (list^(head) & (keys^(head) s= lseg-keys^(head, tail))))) &
  ( (list^(tail) -* (list^(head) & (keys^(head) s= (lseg-keys^(head, tail) union keys^(tail))))) &
    (((tail |-> loc next: virtual tn; int key: virtual tk) * list^(tn)) -* ((lseg^(head, tn) & (lseg-keys^(head, tn) s= (lseg-keys^(head, tail) union (singleton tk)))) * list^(tn))) ) ) ;

define bin-set-fun lseg-keys^(head, tail):
  (case (head l= tail) : emptyset;
   case ((head |-> loc next: nxt; int key: ky) * true): ((singleton ky) union lseg-keys^(nxt, tail));
   default: emptyset ) ;
*/

_(dryad)
int list_find(Node * list, int k)
  /*D_requires list^(list) */
  /*D_ensures (list^(list)  & (((ret i= 1) &    (k i-in old(keys^(list))))
                             | ((ret i= 0) & (~ (k i-in old(keys^(list))))))) */
{
  Node * curr = list;
	while(curr != NULL)
    /*D_invariant (list^(list) & ((lseg(list, curr) & (~ (k i-in lseg-keys^(old(list), curr)))) * list^(curr))) */
  {
    if(curr->key == k) {
      return 1;
    }
    curr = curr->next;
  }
  return 0;
}

 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

#include <vcc.h>
#include <stdlib.h>

typedef struct Node {
  struct Node *nxt;
  int data;
} Node;

typedef _(dynamic_owns) struct List {
  Node *head;
  _(ghost \bool val[int];)
  _(ghost Node *find[int];)
  _(invariant head != NULL ==> \mine(head))
  _(invariant \forall Node *n; \mine(n) && n->nxt ==> \mine(n->nxt))
  _(invariant \forall Node *n; \mine(n) ==> val[n->data])
  _(invariant \forall int v; val[v] ==> \mine(find[v]) && find[v]->data == v)
  _(ghost \natural idx[Node *])
  _(invariant head ==> idx[head] == 0)
  _(invariant \forall Node *n, *m; \mine(n) && \mine(m) ==>
      head  
      && (idx[n] == 0 ==> n==head)
      && (n->nxt ==> idx[n->nxt] == idx[n] + 1)
      && (idx[m] == idx[n] + 1 ==> m == n->nxt)
      && (idx[m] > idx[n] ==> n->nxt)
  )
} List;

int list_find(List *l, int k)
  _(requires \wrapped(l))
  _(ensures \result == l->val[k])
{
  Node *n;
  _(assert \inv(l))
  for (n = l->head; n; n = n->nxt) 
    _(invariant n ==> n \in l->\owns && n \in \domain(l))
    _(invariant  \forall Node *m; m \in l->\owns && m->data == k 
      ==> m==n || (n && l->idx[m] > l->idx[n]))
  {
	if (n->data == k) return 1;
  }
  _(assert l->val[k] ==> l->find[k] \in l->\owns)
  return 0;
}