diff options
author | Tim Peters <tim.peters@gmail.com> | 2003-01-02 03:14:59 (GMT) |
---|---|---|
committer | Tim Peters <tim.peters@gmail.com> | 2003-01-02 03:14:59 (GMT) |
commit | c3bb26a099249ae267905a200451011c229ba00b (patch) | |
tree | e9bb552775ccc8f8e95746f17e662b057a44a5c5 /Modules/datetimemodule.c | |
parent | 4cedc1e84ee174cebaa59295690cfd5c6f10a0b7 (diff) | |
download | cpython-c3bb26a099249ae267905a200451011c229ba00b.zip cpython-c3bb26a099249ae267905a200451011c229ba00b.tar.gz cpython-c3bb26a099249ae267905a200451011c229ba00b.tar.bz2 |
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.
Diffstat (limited to 'Modules/datetimemodule.c')
-rw-r--r-- | Modules/datetimemodule.c | 55 |
1 files changed, 51 insertions, 4 deletions
diff --git a/Modules/datetimemodule.c b/Modules/datetimemodule.c index 8211a10..2755f72 100644 --- a/Modules/datetimemodule.c +++ b/Modules/datetimemodule.c @@ -5537,7 +5537,7 @@ magnitude less than 24 hours. For that reason, if y is firmly in std time, In any case, the new value is - z = y + y.o - y.d - x.o + z.n = y.n + y.o - y.d - x.o If z.n - z.o = x.n - x.o [4] @@ -5579,8 +5579,55 @@ Plugging that into [5], Therefore z is the standard-time spelling, and there's nothing left to do in this case. -Note that we actually proved something stronger: when [4] is true, it must -also be true that z.dst() returns 0. +QED -XXX Flesh out the rest of the algorithm. +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. --------------------------------------------------------------------------- */ |