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

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

typedef
/*D_tag b_node */
struct b_node {
  struct b_node * left;
  struct b_node * right;
  int key;
} BNode;

/*D_defs 
define pred bst^(x): 
  ( ((x l= nil) & emp) |
    ((x |-> loc left: lft; loc right: rgt; int key: ky) * ((bst^(lft) & (keys^(lft) set-lt ky)) * (bst^(rgt) & (ky lt-set keys^(rgt)))))  
  );

define set-fun keys^(x):
  (case (x l= nil): emptyset;
   case ((x |-> loc left: lft; loc right: rgt; int key: ky) * true): 
    ((singleton ky) union (keys^(lft) union keys^(rgt)));
   default: emptyset
  ) ;
*/

_(dryad)
BNode * bst_insert_rec(BNode * x, int k)
  /*D_requires (bst^(x) & (~ (k i-in keys^(x)))) */
  /*D_ensures  (bst^(ret) & (keys^(ret) s= (old(keys^(x)) union (singleton k)))) */
{
  if (x == NULL) {
    BNode * leaf = (BNode *) malloc(sizeof(BNode));
    _(assume leaf != NULL)

    leaf->key   = k;
    leaf->left  = NULL;
    leaf->right = NULL;

    return leaf;
  } else if (k < x->key) {
    BNode * l = x->left;
    BNode * r = x->right;
    BNode * tmp = bst_insert_rec(l, k);

    x->left = tmp;

    return x;
  } else {
    BNode * l = x->left;
    BNode * r = x->right;
    BNode * tmp = bst_insert_rec(r, k);
   
    x->right = tmp;

    return x;
  } 
}

  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
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146

#include "stdlib.h"
#include "assert.h"

struct tree{
  int key;
  struct tree *left;
  struct tree *right;
};

/*@
predicate tree(struct tree *t,bintree b)
  requires switch(b){
    case empty: return t==0;
    case tree(a,bl,br): return t->key |-> ?v &*& t->left |-> ?l &*& t->right |-> ?r 
			&*& malloc_block_tree(t) &*& tree(l,bl) &*& tree(r,br) &*& t!=0 &*& a==v ;
  }&*& inorder(b)==true;

inductive bintree = |empty |tree(int,bintree,bintree);

fixpoint bool t_contains(bintree b, int v) {
  switch (b) {
    case empty: return false;
    case tree(a,l,r): return a==v || (v < a? t_contains(l,v):t_contains(r,v));
  }
}
fixpoint bintree tree_add(bintree b, int x) {
  switch (b) {
    case empty: return tree(x,empty,empty);
    case tree(v,l,r): return x < v? tree(v,tree_add(l,x),r):
			(x==v? tree(v,l,r):tree(v,l,tree_add(r,x)));
  }
}
fixpoint int max(bintree b){
  switch(b){
    case tree(a,bl,br): return (br==empty? a:max(br));
    case empty: return 0;
  }
}
fixpoint int min(bintree b){
  switch(b){
    case tree(a,bl,br): return (bl==empty? a:min(bl));
    case empty: return 0;
  }
}
fixpoint bool inorder(bintree b){
  switch(b){
	case empty: return true;
	case tree(a,bl,br): return (bl==empty? true:max(bl)<a)&& (br==empty? true: a < min(br))
		&& inorder(bl) && inorder(br);
  }
}
lemma void max_conj_add(bintree l,int v,int x)
  requires x < v &*& (max(l)<v||l==empty) &*& inorder(l)==true;
  ensures max(tree_add(l,x))<v &*& inorder(l)==true;
{
  switch(l){
	case empty:
	case tree(a,b,c):if(x < a){
                          /* Needed by Redux. */ if (b == empty) {} else {}
			  max_conj_add(b,a,x);
			 }
			 if(a < x){
                          /* Needed by Redux. */ if (c == empty) {} else {}
			  max_conj_add(c,v,x);
			 }
                         /* Needed by Redux. */ if ((x < a) == true) {} else { if (x == a) {} else {} }
                         /* Needed by Redux. */ if (c == empty) {} else {}
                         /* Needed by Redux. */ if (x == a) {} else {}
                         /* Needed by Redux. */ if (tree_add(c, x) == empty) {} else {}
  }
}
lemma void min_conj_add(bintree r,int v,int x)
  requires v < x &*& (v < min(r)||r==empty) &*& inorder(r)==true;
  ensures v < min(tree_add(r,x)) &*& inorder(r)==true;
{
  switch(r){
	case empty:
	case tree(a,b,c):if(a < x){
			  min_conj_add(c,a,x);
			 }
			 if(x < a){
			  min_conj_add(b,v,x);
			 }
  }
}
lemma void tree_add_inorder(bintree b, int x)
    requires inorder(b)==true &*& t_contains(b,x)==false;
    ensures inorder(tree_add(b,x))==true &*& t_contains(tree_add(b,x),x)==true;
{
    switch (b) {
        case empty:
        case tree(v,l,r):if(x < v){
			  max_conj_add(l,v,x);
			  tree_add_inorder(l,x);
			 }
			 if(v < x){
			  min_conj_add(r,v,x);
			  tree_add_inorder(r,x);
		  	 }
    }
}
@*/


struct tree * bst_insert(struct tree *x, int k)
  //@ requires tree(x,?b) &*& false==t_contains(b,k) &*& inorder(b)==true;
  //@ ensures tree(result,tree_add(b,k)) &*& inorder(tree_add(b,k))==true;
 {
  //@ open tree(x,b);
  if (x == 0) {
    struct tree *leaf = malloc(sizeof(struct tree));
    if (leaf == 0) abort();
    leaf->key=k;
    leaf->left=0;
    leaf->right=0;
    //@ struct tree *l = leaf->left;
    //@ close tree(l,empty);
    //@ struct tree *r = leaf->right;
    //@ close tree(r,empty);
    //@ int v = leaf->key;
    //@ close tree(leaf,tree(k,empty,empty));
    return leaf;

  } else {
    int v=x->key;
    struct tree *l=x->left;
    //@ open tree(l,?bl);
    //@ close tree(l,bl);
    struct tree *r=x->right;
    //@ open tree(r,?br);
    //@ close tree(r,br);
    if(k < v){
      struct tree *tmp = bst_insert(l,k);
      x->left = tmp;
      //@ tree_add_inorder(b,k);
      //@ close tree(x,tree(v,tree_add(bl,k),br));
      return x;
    } else{
      struct tree *tmp = bst_insert(r,k);
      x->right=tmp;
      //@ tree_add_inorder(b,k);
      //@ close tree(x,tree(v,bl,tree_add(br,k)));	
      return x;
    }
  }
}