Re: [gobo-eiffel-develop] Preconditions in creation procedures of DT_FIXED_OFFSET_TIME_ZONE

[Colin P. A. <co...@co...>]

>>>>> "Eric" == Eric Bezault <er...@go...> writes:

    Eric> Colin Paul Adams wrote:
    >> I have changed the m_small_enough precondition in the creation
    >> procedures from h <= 0 to h < 0, as otherwise it was impossible
    >> to create offsets of zero hours and a few minutes.

    Eric> I understand the problem, but I don't think that the fix is
    Eric> correct. Indeed, now it will not be possible anymore to have
    Eric> offsets of zero hours and minus a few minutes. In case of
    Eric> `make_hours_minutes' for example I think that we should
    Eric> rather have:

    Eric>   h_large_enough: h > -Hours_in_day h_small_enough: h <
    Eric> Hours_in_day m_large_enough_positive: h > 0 implies m >= 0
    Eric> m_small_enough_positive: h > 0 implies m < Minutes_in_hour
    Eric> m_large_enough_negative: h < 0 implies m > -Minutes_in_hour
    Eric> m_small_enough_negative: h < 0 implies m <= 0
    Eric> m_large_enough_null: h = 0 implies m > -Minutes_in_hour
    Eric> m_small_enough_null: h = 0 implies m < Minutes_in_hour

OK. I have made that change, and similar in others.
-- 
Colin Adams
Preston Lancashire