[Zope3-dev] RE: [Python-Dev] Holes in time

[Tim Peters]

[Guido, on astimezone() assumptions]

Most of these assumptions aren't needed by the current implementation.  The
crucial assumption (used in every step) is that

    tz.utcoffset(d) - tz.dst(d)

is invariant across all d with d.tzinfo == tz.  Apart from that, only one
other assumption is made, at the end:

> ...
> It can assume that the DST correction is >= 0 and probably less than
> 10 hours or so,

Those aren't needed (or used).

> and that DST changes don't occur more frequently than twice a year
> (once on and once off),

Ditto -- although you'll grow another unspellable hour each time DST ends.

> and that the DST correction is constant during the DST period,

A weaker form of that is needed at the end.  I didn't get around to writing
the end of the proof yet.  At that point, we've got a guess z'.  The missing
part of the proof is that z' is UTC-equivalent to the input datetime if and
only if

    (z' + z'.dst()).dst() == z'.dst()

Intuitively, and because we know that z'.dst() != 0 at this point in the
algorithm, it's saying the result is correct iff "moving a little farther
into DST still leaves us in DST".  For a class like Eastern, it fails to
hold iff we start with the unspellable hour at the end of daylight time:
6:MM UTC maps to z' == 1:MM Eastern, which appears to be dayight time.
z'.dst() returns 60 minutes then, but

   (z' + z'.dst()).dst() == (1:MM Eastern + 1 hour).dst() ==
   (2:MM Eastern).dst() == 0 != 60

then.  Another way this *could* hypothetically fail is if .dst() returned
different non-zero values at different times.  But the assumption is only
needed in that specific expression, so it should be OK if distinct daylight
periods have distinct dst() offsets (although maintaining the utcoffset() -
dst() is-a-constant invariant appears unlikely then).

> and that the only variation in UTC offset is due to DST.

That's not used either -- although, again, the assumption that "the standard
offset" (utcoffset-dst) is a constant is hard to maintain in a wacky time
zone.