HashfunFunctional model of hash tables

This C program, hash.c, implements a hash table with external chaining. See https://www.cs.princeton.edu/~appel/HashTables.pdf for an introduction to hash tables.

    /* First, access a few standard-library functions */
    #include <stddef.h>
    extern void * malloc (size_t n);
    extern void exit(int n);
    extern size_t strlen(const char *str);
    extern char *strcpy(char *dest, const char *src);
    extern int strcmp(const char *str1, const char *str2);

    /* A function to turn a character-string into an integer */
    unsigned int hash (char *s) {
      unsigned int n=0;
      unsigned int i=0;
      int c=s[i];
      while (c) {
        n = n*65599u+(unsigned)c;
        i++;
        c=s[i];
      }
      return n;
    }

    /* Each "bucket" is a linked list of these cells: */
    struct cell {
      char *key;
      unsigned int count;
      struct cell *next;
    };

    /* How many buckets in the hash table */
    enum {N = 109};

    /* A hash table is an array of buckets */
    struct hashtable {
      struct cell *buckets[N];
    };

    /* first malloc space for a new copy of a string, then copy it. */
    char *copy_string (char *s) {
      int i,n = strlen(s)+1;
      char *p = malloc(n);
      if (!p) exit(1);
      strcpy(p,s);
      return p;
    }

    /* create an empty table */
    struct hashtable *new_table (void) {
      int i;
      struct hashtable *p = 
           (struct hashtable * )malloc(sizeof(struct hashtable));
      if (!p) exit(1);
      for (i=0; i<N; i++) p->buckets[i]=NULL;
      return p;
    }  

    /* allocate and initialize a new linked-list cell */
    struct cell *new_cell (char *key, int count, struct cell *next) {
      struct cell *p = (struct cell * )malloc(sizeof(struct cell));
      if (!p) exit(1);
      p->key = copy_string(key);
      p->count = count;
      p->next = next;
      return p;
    }

    /* lookup up a string in the hash table, getting its occurrence count */
    unsigned int get (struct hashtable *table, char *s) {
      unsigned int h = hash(s);
      unsigned int b = h % N;
      struct cell *p = table->buckets[b];
      while (p) {
        if (strcmp(p->key, s)==0)
          return p->count;
        p=p->next;
      }
      return 0;
    }

    /* increment to the occurrence count of the string s in bucket *r0 */
    void incr_list (struct cell **r0, char *s) {
      struct cell *p, **r;
      for(r=r0; ; r=&p->next) {
        p = *r;
        if (!p) {
          *r = new_cell(s,1,NULL);
          return;
        }
        if (strcmp(p->key, s)==0) {
          p->count++;
          return;
        }
      }
    }  

    /* increment to the occurrence count of the string s the whole hash table */
    void incr (struct hashtable *table, char *s) {
      unsigned int h = hash(s);
      unsigned int b = h % N;
      incr_list (& table->buckets[b], s);
    }

A functional model

Before we prove the C program correct, we write a functional program that models its behavior as closely as possible. The functional program won't be (average) constant time per access, like the C program, because it takes linear time to get the nth element of a list, while the C program can subscript an array in constant time. But we are not worried about the execution time of the functional program; only that it serve as a model for specifying the C program.

Exercise: 2 stars, standard (hashfun_inrange)

Exercise: 1 star, standard (hashfun_get_unfold)

Exercise: 2 stars, standard (Zlength_hashtable_incr)

Exercise: 3 stars, standard (hashfun_snoc)

Use Int_repr_eq_mod in the proof of hashfun_aux_snoc.

Functional model satisfies the high-level specification

The purpose of a hash table is to implement a finite mapping, (a finite function) from keys to values. We claim that the functional model (empty_table, hashtable_get, hashtable_incr) correctly implements the appropriate operations on the abstract data type of finite functions. We formalize that statement by defining a Module Type:

This means: in any Module that satisfies this Module Type, there's a type table of count-tables, and operators empty, get, set that satisfy the axioms gempty, gss, and gso.

A "reference" implementation of COUNT_TABLE

Exercise: 2 stars, standard (FunTable)

It's easy to make a slow implementation of COUNT_TABLE, using functions.

Demonstration that hash tables implement COUNT_TABLE

Exercise: 3 stars, standard (IntHashTable)

Now we make a "fast" implementation using hash tables. We put "fast" in quotes because, unlike the imperative implementation, the purely functional implementation takes linear time, not constant time, to select the the i'th bucket. That is, Znth i al takes time proportional to i. But that is no problem, because we are not using hashtable_get and hashtable_incr as our real implementation; they are serving as the functional model of the fast implementation in C.