package calc;

/** Negation of a register
 * @author Gary T. Leavens
 */
public class Negate implements FormulaType {
    
    private /*@ spec_public @*/ int reg;
    
    /** Initialize this negation formula to refer
     * to the given register. */
    /*@ requires 0 <= reg && reg < Registers.NUM_REGS;
      @ ensures this.reg == reg;
      @*/
    public Negate(int reg) {
        this.reg = reg;
    }

    /**
     * @see calc.FormulaType#evaluate()
     */
    public double evaluate() {
        return - Registers.get(reg);
    }

    /**
     * @see calc.FormulaType#isPositive()
     */
    public boolean isPositive() {
        return evaluate() > 0;
    }
}