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

[Tim Peters]

[Guido]
> If anyone is interested, I have a geometric proof that the
> astimezone() method is correct.  I personally find the geometric proof
> easier to understand than Tim's analytic proof.

I hope so <wink>.  Diagrams give insight, algebra gives certainty and
usually teases out assumptions better.

> It's also shorter -- except it needs drawings.  Should I bother
> writing it down?

Sure!  Include it with the analytic proof in the source file.  Half the
words there are explaining the edge cases and what we want to do when we see
one, and so are resuable.  BTW, the analytic proof is about three times as
long as it needs to be, because it explains each tiny step in detail.  More
typical would be something like

Let y = x but in tz's time zone.
Let z = y - x.o + y.s.

Then diff = (x.n - x.o) - (z.n - z.o) =
            x.n - x.o - y.n + x.o - y.s + z.o =
            z.o - y.s =
            z.d

We're done iff z.d = 0, and if it is then we have the std time spelling we
want in the start-of-DST case.

Else let z' = z + z.d.

Then diff' = (x.n - x.o) - (z'.n - z'.o) =
             x.n - x.o - z.n - x.n + x.o + z.n - z.o + z'.o =
             z'.o - z.o =
             z'.d - z.d

So now we're done iff z'.d = z.d.  If not, we must be in the end-of-DST case
(there is no UTC equivalent to x in tz's local time), so we want z (in
daylight time) instead of z' (in std time for most realistic time zones, but
perhaps in a different branch of double-daylight time -- figuring out
exactly how it can be that z'.d != z.d at this point is an example of the
analytic method forcing assumptions into the open).