[Python-checkins] python/nondist/sandbox/datetime datetime.py,1.137,1.138
tim_one@users.sourceforge.net
tim_one@users.sourceforge.net
Thu, 02 Jan 2003 09:47:08 -0800
Update of /cvsroot/python/python/nondist/sandbox/datetime
In directory sc8-pr-cvs1:/tmp/cvs-serv31255
Modified Files:
datetime.py
Log Message:
The astimezone() correctness proof endured much pain to prove what
turned out to be 3 special cases of a single more-general result.
Proving the latter instead is a real simplification.
Index: datetime.py
===================================================================
RCS file: /cvsroot/python/python/nondist/sandbox/datetime/datetime.py,v
retrieving revision 1.137
retrieving revision 1.138
diff -C2 -d -r1.137 -r1.138
*** datetime.py 2 Jan 2003 16:16:27 -0000 1.137
--- datetime.py 2 Jan 2003 17:47:06 -0000 1.138
***************
*** 1898,1902 ****
This follows from the definition of x.s.
! 2. If x and y have the same tzinfo member, x.s == y.s.
This is actually a requirement, an assumption we need to make about
sane tzinfo classes.
--- 1898,1902 ----
This follows from the definition of x.s.
! 2. If x and y have the same tzinfo member, x.s = y.s.
This is actually a requirement, an assumption we need to make about
sane tzinfo classes.
***************
*** 1908,1912 ****
This follows from #2, and that datimetimetz+timedelta preserves tzinfo.
! 5. (y+k).n = y.n + k
Again follows from how arithmetic is defined.
--- 1908,1912 ----
This follows from #2, and that datimetimetz+timedelta preserves tzinfo.
! 5. (x+k).n = x.n + k
Again follows from how arithmetic is defined.
***************
*** 1948,1957 ****
In any case, the new value is
! z.n = y.n + y.o - y.d - x.o
! If
! z.n - z.o = x.n - x.o [4]
! then, we have an equivalent time, and are almost done. The insecurity here is
at the start of daylight time. Picture US Eastern for concreteness. The wall
time jumps from 1:59 to 3:00, and wall hours of the form 2:MM don't make good
--- 1948,1967 ----
In any case, the new value is
! z = y + y.o - y.d - x.o [4]
! It's helpful to step back at look at [4] from a higher level: rewrite it as
! z = (y - x.o) + (y.o - y.d)
!
! (y - x.o).n = [by #5] y.n - x.o = [since y.n=x.n] x.n - x.o = [by #3] x's
! UTC equivalent time. So the y-x.o part essentially converts x to UTC. Then
! the y.o-y.d part essentially converts x's UTC equivalent into tz's standard
! time (y.o-y.d=y.s by #1).
!
! At this point, if
!
! z.n - z.o = x.n - x.o [5]
!
! we have an equivalent time, and are almost done. The insecurity here is
at the start of daylight time. Picture US Eastern for concreteness. The wall
time jumps from 1:59 to 3:00, and wall hours of the form 2:MM don't make good
***************
*** 1961,2037 ****
the only spelling that makes sense on the local wall clock.
! Claim: When [4] is true, we have "the right" spelling in this endcase. No
! further adjustment is necessary.
!
! Proof: The right spelling has z.d = 0, and the wrong spelling has z.d != 0
! (for US Eastern, the wrong spelling has z.d = 60 minutes, but we can't assume
! that all time zones work this way -- we can assume a time zone is in daylight
! time iff dst() doesn't return 0). By [4], and recalling that z.o = z.s + z.d,
!
! z.n - z.s - z.d = x.n - x.o [5]
!
! Also
!
! z.n = (y + y.o - y.d - x.o).n by the construction of z, which equals
! y.n + y.o - y.d - x.o by #5.
!
! Plugging that into [5],
!
! y.n + y.o - y.d - x.o - z.s - z.d = x.n - x.o; cancelling the x.o terms,
! y.n + y.o - y.d - z.s - z.d = x.n; but x.n = y.n too, so they also cancel,
! y.o - y.d - z.s - z.d = 0; then y.o = y.s + y.d, so
! y.s + y.d - y.d - z.s - z.d = 0; then the y.d terms cancel,
! y.s - z.s - z.d = 0; but y and z are in the same timezone, so by #2
! y.s = z.s, and they also cancel, leaving
! - z.d = 0; or,
! z.d = 0
!
! Therefore z is the standard-time spelling, and there's nothing left to do in
! 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
--- 1971,2010 ----
the only spelling that makes sense on the local wall clock.
! In fact, if [5] holds at this point, we do have the standard-time spelling,
! but that takes a bit of proof. We first prove a stronger result. What's the
! difference between the LHS and RHS of [5]? Let
! diff = (x.n - x.o) - (z.n - z.o) [6]
! Now
! z.n = by [4]
! (y + y.o - y.d - x.o).n = by #5
! y.n + y.o - y.d - x.o = since y.n = x.n
! x.n + y.o - y.d - x.o = since y.o = y.s + y.d by #1
! x.n + (y.s + y.d) - y.d - x.o = cancelling the y.d terms
! x.n + y.s - x.o = since z and y are have the same tzinfo member,
! y.s = z.s by #2
! x.n + z.s - x.o
! Plugging that back into [6] gives
! diff =
! (x.n - x.o) - ((x.n + z.s - x.o) - z.o) = expanding
! x.n - x.o - x.n - z.s + x.o + z.o = cancelling
! - z.s + z.o = by #2
! z.d
! So diff = z.d.
! If [5] is true now, diff = 0, so z.d = 0 too, and we have the standard-time
! spelling we wanted in the endcase described above. We're done.
! If [5] is not true now, diff = z.d != 0, and z.d is the offset we need to
! add to z (in effect, z is in tz's standard time, and we need to shift the
! offset into tz's daylight time).
! Let
! z' = z + z.d = z + diff
we can again ask whether