package calc;

/** Multiplication formulas for the calculator.
 * @author Gary T. Leavens
 */
public class Mult extends BinaryFormula {
    
    /** Initialize this Mult object to be the product of the given registers.
     * @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 Mult(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 "*";
    }

}