Immutable strings: contract (1)
Possible contract expressed as an outline class declaration:
public interface StringADT {
// Each String value is an immutable string of characters, // of any length, with indices starting at 0.
/////////////// Constructor ///////////////
// public String (char[] cs); // Construct a string consisting of all the chars in cs.