// a simple example of checking sequence contracts 
class Port implements IPort {

    private int values[]; 

    private int ptr = -1; 

    Port(int values[]) { this.values = values; }
    // -------------------------------------------------------------------------

    public void open() { 
        ptr = 0; 
    }

    public int read() {
        sequence("read"); 
        int r = values[ptr]; 
        ptr++; 
        return r; 
    }

    public int read() {
        sequence("read"); 
        preRead(); 
        int r = values[ptr]; 
        ptr++; 
        return r; 
    }

    public boolean out_of_intsP() {
        sequence("out of intsP");  
        return (ptr >= values.length); 
    }

    public void close() {
        sequence("close"); 
        ptr = -1; 
    }

    // checking the sequence contract  
    private boolean sequence(String msg) {
        if (ptr >= 0)
            return true; 
        System.out.println("contract violation: " + msg); 
        System.exit(-1);
        return false; 
    }

    // checking the precondition for read
    private boolean preRead() { 
        if (ptr < values.length)
            return true; 
        System.out.println("precondition violation"); 
        System.exit(-1); 
        return false; 
    }

}