package calc;

/** Unary formulas for the calculator.
 * @author Gary T. Leavens
 */
public abstract class UnaryFormula implements FormulaType {
    /** The register.  This is called "left" in deference to
     *  the binary formula subclass. */
    private /*@ spec_public @*/ int left;
    
    /**Initialize this formula object to contain the given register.
     * @param left, the register's number.
     */
    //@ requires 0 <= left && left < Registers.NUM_REGS;
    //@ assignable this.left;
    //@ ensures this.left == left ;
    public UnaryFormula(int left) {
        this.left = left;
    }
    
    /** Return the value of the register.
     * @return the register's value
     */
    //@ assignable \nothing;
    //@ ensures \result == Registers.get(left);
    protected /*@ pure @*/ double leftValue() {
        return Registers.get(left);
    }
    
    // documentation comment and specification inherited
    public /*@ pure @*/ boolean isPositive() {
        return evaluate() > 0.0;
    }
    
    // documentation comment and specification inherited 
    public int hashCode() {
        return left;
    }

    // documentation comment inherited
    //@ also
    //@   ensures_redundantly o == null ==> !\result;
    //@   ensures \result ==> o instanceof UnaryFormula;
    //@   ensures \result ==> this.getClass() == o.getClass();
    //@   ensures \result ==> ((UnaryFormula)o).left == this.left;
    public /*@ pure @*/ boolean equals(Object o) {
        return o != null && o instanceof UnaryFormula
            && o.getClass() == this.getClass()
            && ((UnaryFormula)o).left == this.left;
    }
    
    public String toString() {
        return "r" + left;
    }
}