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

[Eric B. <er...@go...>]

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.

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

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

-- 
Eric Bezault
mailto:er...@go...
http://www.gobosoft.com