A quicker astimezone() implementation, rehabilitating an earlier
suggestion from Guido, along with a formal correctness proof of the
trickiest bit. The intricacy of the proof reveals how delicate this
is, but also how robust the conclusion: correctness doesn't rely on
dst() returning +- one hour (not all real time zones do!), it only
relies on:
1. That dst() returns a (any) non-zero value if and only if daylight
time is in effect.
and
2. That the tzinfo subclass implements a consistent notion of time zone.
The meaning of "consistent" was a hidden assumption, which is now an
explicit requirement in the docs. Alas, it's an unverifiable (by the
datetime implementation) requirement, but so it goes.
3 files changed