package calc;

/** Subtraction formulas for the calculator.
 * @author Gary T. Leavens
 */
public class Diff extends BinaryFormula {
    
    /**Initialize this Diff object to be the difference of subtracting the right
     * register from the left.
     * @param left, the left register's number.
     * @param right, the right register's number.
     */
    //@ requires 0 <= left && left < Registers.NUM_REGS;
    //@ requires 0 <= right && right < Registers.NUM_REGS;
    //@ assignable this.left, this.right;
    //@ ensures this.left == left && this.right == right;
    public Diff(int left, int right) {
        super(left, right);
    }
    
    // doc comment inherited
    /*@ also
      @   assignable \nothing;
      @   ensures \result == Registers.get(left) - Registers.get(right); @*/
    public double evaluate() {
        return leftValue() - rightValue();
    }
    
    // doc comment and specification inherited
    protected String opString() {
        return "-";
    }
}