public class RatRep1 implements RatRepIF {

    protected int n, d;
    //@ invariant d != 0;

    public RatRep1(int given_n, int given_d)
    //@ requires given_d != 0;
    {
        n = given_n;
        d = given_d;
    }

    public int numer() { return n; }
    public int denom() { return d; }
}