Anonymous Anonymous - 2 months ago
204 0

No description

C

122 stuff

#use <conio>

int count_vocab(string[] vocab, int[] freq, int v, string tweetfile, bool fast)
//@requires v == \length(vocab) && v == \length(freq);
//@requires is_sorted(vocab, 0, v);
//@ensures \length(vocab) == v && \length(freq) == v;
//@ensures \result >= 0;
{
    string_bundle str = read_words(tweetfile);
    string[] words = string_bundle_array(str);
    int wordsL = string_bundle_length(str);
    int notWords = 0;
    for(int i = 0; i < wordsL; i++)
    //@loop_invariant i <= wordsL;
    {
        int wordsN = -1;
        if(!fast)
        {
            wordsN = linsearch(words[i], vocab, v); 
        }
        else
        {
            //@assert fast;
            wordsN = binsearch(words[i], vocab, v);  
        }
        if(wordsN == -1)
        {
            notWords++;
        }
        else
        {
            //@assert wordsN >= 0;
            freq[wordsN]++;
        }
    }
    return notWords;
}



void merge(int[] A, string[] vocab, int lower, int mid, int upper)
//@requires 0 <= lower && lower < mid && mid < upper && upper <= \length(A);
//@requires is_sorted_int(A, lower, mid) && is_sorted_int(A, mid, upper);
//@ensures is_sorted_int(A, lower, upper);
{ 
  int[] B = alloc_array(int, upper - lower);
  string[] Bw = alloc_array(string, upper - lower);
  int i = lower; 
  int j = mid; 
  int k = 0;
  while (i < mid && j < upper)
  //@loop_invariant lower <= i && i <= mid;
  //@loop_invariant mid <= j && j <= upper;
  //@loop_invariant k == (i - lower) + (j - mid);
  {
    if (A[i] <= A[j]) {
      B[k] = A[i];
      Bw[k] = vocab[i]; i++; 
    } else {
      B[k] = A[j];
      Bw[k] = vocab[j]; j++;
    }
    k++;
  }

  //@assert i == mid || j == upper;
  // Warning, loop invariants for these loops have been omitted!
  while (i < mid) { B[k] = A[i]; Bw[k] = vocab[i]; i++; k++;}
  while (j < upper) { B[k] = A[j]; Bw[k] = vocab[j]; j++; k++; }
  for (k = 0; k < upper - lower; k++)
  { A[lower + k] = B[k]; vocab[lower + k] = Bw[k]; }
}


void sort(int[] A, string[] vocab, int lower, int upper)
//@requires 0 <= lower && lower <= upper && upper <= \length(A);
//@ensures is_sorted_int(A, lower, upper);
{
  if (upper-lower <= 1) return;
  int mid = lower + (upper - lower) / 2; 
  sort(A, vocab, lower, mid);//@assert is_sorted_int(A, lower, mid);
  sort(A, vocab, mid, upper);//@assert is_sorted_int(A, mid, upper);
  merge(A, vocab, lower, mid, upper);
  return;
}

void sort_by_freq(string[] vocab, int[] freq, int v)
//@requires v == \length(vocab) && v == \length(freq);
//@ensures is_sorted_int(freq, 0, v);
{
    sort(freq, vocab, 0, v);
}
Comments