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:

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:

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);
	}


Next Prev Main Top Feedback