Assignment_4 02 TEMPERATURE.e

note
    description: "Temperature."

class
    TEMPERATURE

create
    make_celsius, make_kelvin

feature -- Initialization

    make_celsius (v: INTEGER)
            -- Create with Celsius value `v'.
        require
            v >= -273
        do
            celsius := v
        ensure
            celsius = v
            celsius >= -273
        end

    make_kelvin (v: INTEGER)
            -- Create with Kelvin value `v'.
        require
            v >= 0
        do
            celsius := v - 273
        ensure
            celsius >= -273
            kelvin >= 0
            kelvin = celsius + 273
        end

feature -- Access

    celsius: INTEGER
            -- Value in Celsius scale.

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

    fahrenheit: INTEGER
            -- Value in Fahrenheit scale.
        require
            celsius >= -273
        do
            Result := ((celsius * 1.8) + 32).rounded
        ensure
            fahrenheit >= -460
        end

feature -- Measurement

    average (other: TEMPERATURE): TEMPERATURE
            -- Average temperature between `Current' and `other'.
        require
            other /= void
        do
            create Result.make_celsius ((other.celsius + current.celsius) // 2)
        ensure
            ((other.celsius <= celsius) and (celsius <= current.celsius)) or ((current.celsius <= celsius) and (celsius <= other.celsius))
        end

invariant
    kelvin_never_below_zero: kelvin >= 0
    celsius_never_below_min: celsius >= -273
    fahrenheit_never_below_min: fahrenheit >= -460

end