package calc;

/** Sum three registers.
 * @author Gary T. Leavens
 */
public class Sum3 extends Sum {
    
    /** The third register to sum. */
    private /*@ spec_public @*/ int reg3;
    
    /**Initialize this Sum object to calculate 
     * the sum of the given registers.
     */
    //@ requires 0 <= reg1 && reg1 < Registers.NUM_REGS;
    //@ requires 0 <= reg2 && reg2 < Registers.NUM_REGS;
    //@ requires 0 <= reg3 && reg3 < Registers.NUM_REGS;
    //@ assignable this.left, this.right, this.reg3;
    //@ ensures this.left == reg1 && this.right == reg2;
    //@ ensures this.reg3 == reg3;
    public Sum3(int reg1, int reg2, int reg3) {
        super(reg1, reg2);
        this.reg3 = reg3;
    }
    
    // doc comment inherited
    /*@ also
      @   ensures (* \result is the sum of the value of
      @              all the register's values. *); @*/
    public double evaluate() {
        return leftValue() + rightValue() + Registers.get(reg3);
    }
     
    // documentation comment and specification inherited    
    public int hashCode() {
        return super.hashCode() + reg3;
    }

    // documentation comment inherited
    //@ also
    //@   ensures \result ==> o instanceof Sum3;
    //@   ensures \result ==> ((Sum3)o).reg3 == this.reg3;
    public boolean equals(Object o) {
        return super.equals(o) && o instanceof Sum3
            && ((Sum3)o).reg3 == this.reg3;
    }
      
    // doc comment and specification inherited
    public String toString() {
        return super.toString() + " + r" + reg3;
    }
}