Verification

Implementations of ADTs usually have some relationships between their elements. Checking that these relationships are maintained i.e. the data structure is internally consistent can greatly accelerate bug isolation. For this reason, every ADT should have a verify_ function.

In the case of the int_stack ADT, there are only 4 invariants that can be checked:

• len_int_stack() is never negative
• len_int_stack() is never larger than max_int_stack()
• max_int_stack() is always greater than or equal to the initial size, 16
• max_int_stack() is always a multiple of its increments, 16, plus its initial size, also 16.

These invariants are encapsulated in the verify_int_stack() function

	void
	verify_int_stack(
		const int_stack	stack
		)
	{
	  assert( len_int_stack(stack) >= 0 );
	  assert( len_int_stack(stack) <= max_int_stack() );
	  assert( max_int_stack(stack) >= 16 );
	  assert( ((max_int_stack(stack) - 16)%16) == 0 );
	}

If we add a call of verify_int_stack() at the beginning and entry of each function, we verify that the following facts are true:

• The int_stack argument to the function satisfies the invariants of an int_stack; there is a smaller chance that it was of some other type (or just plain garbage, because of an uninitialized or free'd pointer).
• The fields are internally consistent; there is a smaller chance that some field was (erroneously) overwritten by some other function.
• When the function completes, the data structure is still internally consistent; there are some bugs that will be caught this way.

For example, the code for push_int_stack() will look like:

	void
	push_int_stack(
		int_stack	stack,
		int		val
		)
	{
	  int	len = len_int_stack(stack);
	  int	max = max_int_stack(stack);
	  int	nmax;
	  int *	vals;
	  int *	nvals;
	  int	i;

	  verify_int_stack(stack)

	  if( len == max ) {
	    nmax = max + 16;
	    nvals = xnalloc(int, nmax);
	    if( nvals == 0 ) {
	      PANIC("out of memory");
	    }
	    vals = vals_int_stack(stack);
	    for( i = 0; i < len; i++ ) {
	      nvals[i] = vals[i];
	    }
	    x_max_int_stack(stack) = nmax;
	    x_vals_int_stack(stack) = nvals;
	    xnfree(int, max, vals);
	  }

	  vals_int_stack(stack)[len] = val;
	  x_len_int_stack(stack) = len+1;

	  verify_int_stack(stack);
	}