•
requires, ensures
•
maxSet
–
highest index that can be safely written to
•
maxRead
–
highest index that can be safely read
•
char buffer[100];
–
ensures maxSet(buffer) == 99
