TEMPERATURE

note
    description: "Temperature."

class
    TEMPERATURE

create
    make_celsius, make_kelvin

feature -- Initialization

    make_celsius (v: INTEGER)
            -- Create with Celsius value `v'.
        require
                temperature_is_valid : v >= -273 --Greater then or equal to absolute zero.
        do
            -- Create a temperature object encapsulating value 'v' intended in Celsius.
            celsius := v

        ensure
            temperature_is_set: celsius = v
        end

    make_kelvin (v: INTEGER)
            -- Create with Kelvin value `v'.
        require
            temperature_is_valid: v >= 0  --Greater then or equal to absolute zero.
        do
            -- Create a temperature object encapsulating value 'v' intended in Kelvin.
            Current.make_celsius (v - 273)

        ensure
            temperature_is_correctly_set: celsius = v - 273
        end

feature -- Access

    celsius: INTEGER
            -- Value in Celsius scale.

    kelvin: INTEGER
            -- Value in Kelvin scale.
        do
            Result := celsius + 273
        end

feature -- Measurement
    less_or_equal alias "<=" (other : TEMPERATURE) : BOOLEAN
    require
        other_not_void: other /= Void
    do
        Result := Current.celsius <= other.celsius
    ensure
            result_correct: (Result and Current.celsius <= other.celsius) or (not Result and Current.celsius > other.celsius)
    end

    greater_or_equal alias ">=" (other : TEMPERATURE) : BOOLEAN
    require
            other_not_void: other /= Void
    do
        Result := Current.celsius >= other.celsius
    ensure
            result_correct: (Result and Current.celsius >= other.celsius) or (not Result and Current.celsius < other.celsius)
    end

    less_then alias "<" (other : TEMPERATURE) : BOOLEAN
    require
            other_not_void: other /= Void
    do
        Result := Current.celsius < other.celsius
    ensure
            result_correct: (Result and Current.celsius < other.celsius) or (not Result and Current.celsius >= other.celsius)
    end

    greater_then alias ">" (other : TEMPERATURE) : BOOLEAN
    require
            other_not_void: other /= Void
    do
        Result := Current.celsius > other.celsius
    ensure
            result_correct: (Result and Current.celsius > other.celsius) or (not Result and Current.celsius <= other.celsius)
    end

    average (other: TEMPERATURE): TEMPERATURE
            -- Average temperature between `Current' and `other'.

        require
            other_not_void: other /= Void

        local
            new_temperature_object : TEMPERATURE
            new_temperature_value : INTEGER

        do
            -- Compute the average of two temperature. One is given by the current object,
            -- the other is passed as an argument.

            new_temperature_value := ((other.celsius + Current.celsius)/2 + 0.5).floor
            create new_temperature_object.make_celsius(new_temperature_value)
            Result := new_temperature_object
        ensure
            result_correct: (Result >= Current and Result <= other) or (result <= Current and result >= other)
        end

invariant
    temperature_is_valid: Current.kelvin >= 0

end