Update of /cvsroot/python/python/nondist/sandbox/datetime
In directory sc8-pr-cvs1:/tmp/cvs-serv8239
Modified Files:
datetime.py
Log Message:
Completed astimezone's correctness proof. That doesn't mean it's
correct by your lights, it means that-- barring coding errors --it
implements what it intended to implement.
Index: datetime.py
===================================================================
RCS file: /cvsroot/python/python/nondist/sandbox/datetime/datetime.py,v
retrieving revision 1.134
retrieving revision 1.135
diff -C2 -d -r1.134 -r1.135
*** datetime.py 1 Jan 2003 20:57:53 -0000 1.134
--- datetime.py 2 Jan 2003 03:06:39 -0000 1.135
***************
*** 1941,1945 ****
In any case, the new value is
! z = y + y.o - y.d - x.o
If
--- 1941,1945 ----
In any case, the new value is
! z.n = y.n + y.o - y.d - x.o
If
***************
*** 1983,1991 ****
this case.
! Note that we actually proved something stronger: when [4] is true, it must
! also be true that z.dst() returns 0.
! XXX Flesh out the rest of the algorithm.
"""
def _test():
import test_datetime
--- 1983,2039 ----
this case.
! QED
! Note that we actually proved something stronger: [4] is true if and only if
! z.dst() returns 0. The "only if" part was proved directly. The "if" part
! is proved by starting with z.d = 0 and reading the proof bottom-up; all the
! steps are "iff", so are reversible.
!
! Next: if [4] isn't true, we're not done. It's helpful to step back and look
! at
!
! z.n = y.n + y.o - y.d - x.o = y.n-x.o + y.o-y.d
!
! from a higher level. Since y.n = x.n, the y.n-x.o part gives x's UTC
! equivalent hour. Then since y.s=y.o-y.d, the y.o-y.d part converts x's UTC
! equivalent into tz's standard time. IOW, z is the correct spelling of x in
! tz's standard time.
! If
! z.n - z.o != x.n - x.o
! despite that, then either (1) x is in the "unspellable hour" at the end
! of tz's daylight period; or, (2) z.n needs to be shifted into tz's daylight
! time.
!
! Assuming #2, that would be easy if we could ask the tzinfo object what the
! daylight offset would be if DST were in effect. And we could compute z.d,
! but we already have enough info to compute it from the quantities we know:
!
! Claim: The adjustment needed is adding (x.n-x.o)-(z.n-z.o) to z.n.
!
! Proof: By the comment following the last proof, z.d is not 0 now, and z.d
! is what we need to add to z.n (it's the "missing part" of the conversion from
! x's UTC equivalent to z's daylight time).
!
! z.d = z.o - z.s by #1; z.s = y.s since they're in the same time zone, so
! z.d = z.o - y.s; then y.s = y.o - y.d by #1, so
! z.d = z.o - (y.o - y.d); then since z.n = y.n+y.o-y.d-x.o, y.o-y.d=
! z.n-y.n+x.o, so
! z.d = z.o - (z.n - y.n + x.o); then x.n = y.n, so
! z.d = z.o - (z.n - x.n + x.o)
! and simple rearranging gives the desired
! z.d = (x.n - x.o) - (z.n - z.o)
!
! The code actually optimizes this some more, in a straightforward way. Letting
!
! z'.n = z.n + (x.n - x.o) - (z.n - z.o)
!
! we can again ask whether
!
! z'.n - z'.o = x.n - x.o
!
! If so, we're done. If not, the tzinfo class is insane, or we're trying to
! convert to the hour that can't be spelled in tz.
"""
+
def _test():
import test_datetime