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