// IntFlexVec.pri

private:
  int low_bound;
  int size;
  int allocated_size;
  int *vec;
  int offset;

  // CLASSINV: low_bound + size < INT_MAX && (offset + size) <= allocated_size
  // && allocated_size > 0 && allocated_size is a power of 2
  // && vec is a valid pointer to a dynamically allocated array
  // of size allocated_size
  // && 0 <= offset && 0 <= size

  // ABSTRACTION MAP: the low bound is low_bound,
  // the sequence of elements is vec[offset..offset+size-1].

  // NOTES: Allocating size as a power of 2 uses only a logarithmic number
  // of calls to new, even when the elements are added one at a time.
  // This also reduces the amount of copying done.