Поправка, написанная под деление с усечением, применённая к делению вниз, срабатывает дважды — и календарь до нашей эры уезжает на год
Формула Хиннанта (days_from_civil / civil_from_days) написана на C++, где целочисленное деление усекает к нулю. Строка era = (y >= 0 ? y : y-399) / 400 — это не свойство календаря, а эмуляция пола через усечение: вычитание 399 нужно ровно затем, чтобы усечение дало тот же ответ, что дал бы пол.
Если перенести формулу в язык, где деление уже пол, поправка сработает второй раз: на отрицательных годах эра уезжает на единицу вниз, «год эры» выходит за свои [0, 399], и календарь до нашей эры считается неверно.
Чем подтверждено. flang/stdlib/datetime.flang, ветка vypusk/utv-hashmap, основание github/main df055a6b. Нашло это не чтение кода, а постусловие «високосный год — тот, в котором 366 дней», прогнанное по сетке из девятисот дат и по всем годам от −9999 до 9999:
| год | дней насчитал модуль | по правилу четырёх, ста и четырёхсот |
|---|---|---|
| −401 | 366 | не високосный |
| −400 | 365 | високосный (делится на 400) |
| −4 | 366 | високосный, а «Високосный год» отвечает «нет» |
| −1 | 366 | не високосный |
Обратная функция сломана тем же местом (сдвиг − 146096 при делении вниз на 146097): круг «день → дата → день» держится подряд от −719162 (это 0001-01-01) и выше — проверено подряд до −718000, шагом 1009 до 3652425, четырьмя тысячами случайных дней и всем верхним хвостом, — а подряд от −720200 до −719163 краснеет, первый пойманный −719834.
Лечение — две строки: снять поправку целиком, потому что делитель уже пол: эра равно («Деление вниз» от сдвинутый и 400) и эра равно («Деление вниз» от сдвиг и 146097). В дереве не сделано: работа была про утверждения, а это правка ПОВЕДЕНИЯ; граница названа оговорками при утверждениях, и когда счёт починят, оговорки станут лишними.
Почему это класс, а не случай. Признак, по которому третий случай ищется заранее: всякая формула, перенесённая из C, C++, Go, Java или Rust и содержащая рядом с делением слагаемое-поправку, обязана быть перепроверена на отрицательных входах — там деление усекает, здесь «Деление вниз» полит, и поправка из чужого языка становится ошибкой. Обычные примеры этого не показывают: все примеры datetime.flang стоят на датах от 1969 года и выше, и все они зелёные.
Отдельно, и это другой корень. «Високосный год» врёт на −4, −100, −400 ещё и потому, что год остаток от 4 даёт там минус ноль, а −0 равен 0 в языке ложь. Это пятый случай класса minus-zero-is-a-class.
Связано: minus-zero-is-a-class, proven-is-not-correct, double-has-no-laws