Verification
The date transformations and calculations are verified relative to a intuitive specification of next_date.
It is proved that the following diagrams commute:
| GregorianDate | Transformation | OrdinaleDate | Transformation | Modified Julian Day |
|---|---|---|---|---|
| dt | => dateToOrdinalDate => | odt | => fromOrdinalDate => | mjd |
| ⇓ next_date | proof | ⇓ next_date | proof | ⇓ add 1 |
| dt | <= ordinalDateToDate <= | odt | <= toOrdinalDate <= | mjd |