/* $Id$
 */
package calc;

/** Binary formulas.
 * @author Gary T. Leavens
 */
public abstract class BinaryFormula extends Formula {
    
	/** The number of the left register. */
	//@ public model int left; //@ in reg;
	/** The number of the right register. */
	//@ public model int right;
	 
	//@ private represents left <- reg;
	//@ private represents right <- reg2;
	
    /** the second register */
    private int reg2; //@ in right;
    
    /**
     * Initialize this Formula object with the given registers.
     * @param reg1 the left register's number.
     * @param reg2 the reg2 register's number
     */
    //@ requires 0 <= reg1 && reg1 < Registers.NUM_REGS;
    //@ requires 0 <= reg2 && reg2 < Registers.NUM_REGS;
    //@ ensures left == reg1 && right == reg2; 
    public BinaryFormula(int reg1, int reg2) {
        super(reg1);
        this.reg2 = reg2;
    }

	/** Return the value of the second register. */
    protected /*@ pure @*/ double reg2Value() {
        return get(reg2);
    }
}