bloomFilter/bloom-expensive.c0 at master · shback0708/bloomFilter · GitHub

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
/*
 * Interface for bloom filters (sets)
 * Expensive implementaiton with no false negatives (sorted linked list)
 *
 * 15-122 Principles of Imperative Computation */

#use <string>

/*** Interface to bloom filters ***/

// typedef ______* bloom_t;
typedef struct bloom_header* bloom_t;

bloom_t bloom_new(int table_size)
  /*@requires table_size > 0; @*/
  /*@ensures \result != NULL; @*/ ;

bool bloom_contains(bloom_t B, string x)
  /*@requires B != NULL; @*/ ;

void bloom_add(bloom_t B, string x)
  /*@requires B != NULL; @*/
  /*@ensures bloom_contains(B, x); @*/ ;

/*** Implementation of bloom filters ***/

typedef struct list_node list;
struct list_node {
  string data;
  list* next;
};

typedef struct bloom_header bloom;
struct bloom_header {
  list* chain;
};

bool is_bloom(bloom* B) {
  if (B == NULL) return false;
  if (B->chain == NULL) return true;

  string last = B->chain->data;
  for (list* l = B->chain->next; l != NULL; l = l->next) {
    if (string_compare(last, l->data) >= 0) return false;
    last = l->data;
  }

  return true;
}

bloom* bloom_new(int table_size)
//@requires table_size > 0;
//@ensures is_bloom(\result);
{
  return alloc(bloom);
}

bool bloom_contains(bloom* B, string x)
//@requires is_bloom(B);
{
  for (list* l = B->chain; l != NULL; l = l->next) {
    int cmp = string_compare(l->data, x);
    if (cmp == 0) return true;
    if (cmp > 0) return false;
  }

  return false;
}

void bloom_add(bloom* B, string x)
//@requires is_bloom(B);
//@ensures is_bloom(B);
//@ensures bloom_contains(B, x);
{
  if (B->chain == NULL || string_compare(x, B->chain->data) < 0) {
    list* new = alloc(list);
    new->data = x;
    new->next = B->chain;
    B->chain = new;

  } else if (string_compare(x, B->chain->data) == 0) {
    return;

  } else {
    list* l;
    for (l = B->chain; l->next != NULL; l = l->next)
    //@loop_invariant l != NULL;
    //@loop_invariant string_compare(x, l->data) > 0;
    {
      int cmp = string_compare(x, l->next->data);
      if (cmp == 0) return; // Already present
      if (cmp < 0) { // New element belongs here
        list* new = alloc(list);
        new->data = x;
        new->next = l->next;
        l->next = new;
        return;
      }
    }

    // Exit for loop: new list node belongs at end of chain
    l->next = alloc(list);
    l->next->data = x;
  }
}