bloomFilter/bloom1.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
#use <string>


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

typedef struct bloom_filter* bloom_t;

bloom_t bloom_new(int m)
  /*@requires m > 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 ***/

int hash_string(string s){
    char[] char_arr = string_to_chararray(s);
    int len = string_length(s);
    int count = 0;
    int hash_result = 0;
    while (count < len) {
    hash_result = hash_result * 31 + char_ord(char_arr[count]);
    count++;
    }
    if (hash_result < 0){
        return -1 * (hash_result + 1);
    }
    return hash_result ;
}

typedef struct bloom_filter bloom;
struct bloom_filter {
  bool[] data;
  int capacity; // capacity == \length(data);
};

bool is_bloom(bloom_t B)
{
  if (B == NULL) return false;
  //@assert B -> capacity == \length(B->data);
  return true;
}

bloom* bloom_new(int m)
//@requires m > 0;
//@ensures is_bloom(\result);
{
  bloom_t B = alloc(bloom);
  B->data = alloc_array(bool,m);
  for (int i = 0; i < m; i++){
    B -> data[i] = false;
  }
  B -> capacity = m;
  return B;
}

bool bloom_contains(bloom* B, string x)
//@requires is_bloom(B);
{
  return B->data[hash_string(x) % (B -> capacity)];
}

void bloom_add(bloom* B, string x)
//@requires is_bloom(B);
//@ensures is_bloom(B);
//@ensures bloom_contains(B, x);
{
    B->data[hash_string(x) % (B -> capacity)] = true;
}