[Zope3-checkins] CVS: Zope3/src/datetime - _datetime.py:1.15
Tim Peters
tim.one@comcast.net
Thu, 2 Jan 2003 12:48:46 -0500
Update of /cvs-repository/Zope3/src/datetime
In directory cvs.zope.org:/tmp/cvs-serv23786/src/datetime
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.
=== Zope3/src/datetime/_datetime.py 1.14 => 1.15 ===
--- Zope3/src/datetime/_datetime.py:1.14 Thu Jan 2 11:19:07 2003
+++ Zope3/src/datetime/_datetime.py Thu Jan 2 12:48:44 2003
@@ -1890,7 +1890,7 @@
1. x.o = x.s + x.d
This follows from the definition of x.s.
-2. If x and y have the same tzinfo member, x.s == y.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.
@@ -1900,7 +1900,7 @@
4. (x+k).s = x.s
This follows from #2, and that datimetimetz+timedelta preserves tzinfo.
-5. (y+k).n = y.n + k
+5. (x+k).n = x.n + k
Again follows from how arithmetic is defined.
Now we can explain x.astimezone(tz). Let's assume it's an interesting case
@@ -1940,12 +1940,22 @@
In any case, the new value is
- z.n = y.n + y.o - y.d - x.o
+ z = y + y.o - y.d - x.o [4]
-If
- z.n - z.o = x.n - x.o [4]
+It's helpful to step back at look at [4] from a higher level: rewrite it as
-then, we have an equivalent time, and are almost done. The insecurity here is
+ 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
sense then. A sensible Eastern tzinfo class will consider such a time to be
@@ -1953,79 +1963,42 @@
day DST starts. We want to return the 1:MM EST spelling because that's
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)
+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).
-The code actually optimizes this some more, in a straightforward way. Letting
+Let
- z'.n = z.n + (x.n - x.o) - (z.n - z.o)
+ z' = z + z.d = z + diff
we can again ask whether