// String.pri

private: 
  int length;
  char *theString;

  // REP INVARIANT: theString is a valid pointer
  // && length >= 0
  // && theString points to an array of characters of size length.

  // ABSTRACTION MAP: the sequence is theString[0..length-1]

String(int len);
  // PRE: length >= 0
  // MODIFIES: self
  // POST: length == len && theString points to an array of len characters
  // which has not been initialized.