Reading material

Pages 99-112.

Additional material

public interface TextModel
{
    public int length();
    public void write(int position, char character);
    public char read(int position);
    public char[] text();
}

Question

Give a pre- and postcondition for read(p) for the following two situations. Does the second situation refine the first one?