diff --git a/spec.html b/spec.html index 9f07527651..63b4af2164 100644 --- a/spec.html +++ b/spec.html @@ -32072,92 +32072,283 @@

Time Values and Time Range

A Number can exactly represent all integers from -9,007,199,254,740,992 to 9,007,199,254,740,992 ( and ). A time value supports a slightly smaller range of -8,640,000,000,000,000 to 8,640,000,000,000,000 milliseconds. This yields a supported time value range of exactly -100,000,000 days to 100,000,000 days relative to midnight at the beginning of 1 January 1970 UTC.

The exact moment of midnight at the beginning of 1 January 1970 UTC is represented by the time value *+0*𝔽.

+

In the proleptic Gregorian calendar, leap years are precisely those which are both divisible by 4 and either divisible by 400 or not divisible by 100.

The 400 year cycle of the proleptic Gregorian calendar contains 97 leap years. This yields an average of 365.2425 days per year, which is 31,556,952,000 milliseconds. Therefore, the maximum range a Number could represent exactly with millisecond precision is approximately -285,426 to 285,426 years relative to 1970. The smaller range supported by a time value as specified in this section is approximately -273,790 to 273,790 years relative to 1970.

 - -

Day Number and Time within Day

-

A given time value _t_ belongs to day number

- Day(_t_) = 𝔽(floor(ℝ(_t_ / msPerDay))) -

where the number of milliseconds per day is

- msPerDay = *86400000*𝔽 -

The remainder is called the time within the day:

- TimeWithinDay(_t_) = 𝔽(ℝ(_t_) modulo ℝ(msPerDay)) - - - -

Year Number

-

ECMAScript uses a proleptic Gregorian calendar to map a day number to a year number and to determine the month and date within that year. In this calendar, leap years are precisely those which are (divisible by 4) and ((not divisible by 100) or (divisible by 400)). The number of days in year number _y_ is therefore defined by

- - DaysInYear(_y_) - = *365*𝔽 if (ℝ(_y_) modulo 4) ≠ 0 - = *366*𝔽 if (ℝ(_y_) modulo 4) = 0 and (ℝ(_y_) modulo 100) ≠ 0 - = *365*𝔽 if (ℝ(_y_) modulo 100) = 0 and (ℝ(_y_) modulo 400) ≠ 0 - = *366*𝔽 if (ℝ(_y_) modulo 400) = 0 - -

All non-leap years have 365 days with the usual number of days per month and leap years have an extra day in February. The day number of the first day of year _y_ is given by:

- DayFromYear(_y_) = 𝔽(365 × (ℝ(_y_) - 1970) + floor((ℝ(_y_) - 1969) / 4) - floor((ℝ(_y_) - 1901) / 100) + floor((ℝ(_y_) - 1601) / 400)) -

The time value of the start of a year is:

- TimeFromYear(_y_) = msPerDay × DayFromYear(_y_) -

A time value determines a year by:

- YearFromTime(_t_) = the largest integral Number _y_ (closest to +∞) such that TimeFromYear(_y_) ≤ _t_ -

The leap-year function is *1*𝔽 for a time within a leap year and otherwise is *+0*𝔽:

- - InLeapYear(_t_) - = *+0*𝔽 if DaysInYear(YearFromTime(_t_)) is *365*𝔽 - = *1*𝔽 if DaysInYear(YearFromTime(_t_)) is *366*𝔽 - - - - -

Month Number

-

Months are identified by an integral Number in the inclusive interval from *+0*𝔽 to *11*𝔽. The mapping MonthFromTime(_t_) from a time value _t_ to a month number is defined by:

- - MonthFromTime(_t_) - = *+0*𝔽 if *+0*𝔽 ≤ DayWithinYear(_t_) < *31*𝔽 - = *1*𝔽 if *31*𝔽 ≤ DayWithinYear(_t_) < *59*𝔽 + InLeapYear(_t_) - = *2*𝔽 if *59*𝔽 + InLeapYear(_t_) ≤ DayWithinYear(_t_) < *90*𝔽 + InLeapYear(_t_) - = *3*𝔽 if *90*𝔽 + InLeapYear(_t_) ≤ DayWithinYear(_t_) < *120*𝔽 + InLeapYear(_t_) - = *4*𝔽 if *120*𝔽 + InLeapYear(_t_) ≤ DayWithinYear(_t_) < *151*𝔽 + InLeapYear(_t_) - = *5*𝔽 if *151*𝔽 + InLeapYear(_t_) ≤ DayWithinYear(_t_) < *181*𝔽 + InLeapYear(_t_) - = *6*𝔽 if *181*𝔽 + InLeapYear(_t_) ≤ DayWithinYear(_t_) < *212*𝔽 + InLeapYear(_t_) - = *7*𝔽 if *212*𝔽 + InLeapYear(_t_) ≤ DayWithinYear(_t_) < *243*𝔽 + InLeapYear(_t_) - = *8*𝔽 if *243*𝔽 + InLeapYear(_t_) ≤ DayWithinYear(_t_) < *273*𝔽 + InLeapYear(_t_) - = *9*𝔽 if *273*𝔽 + InLeapYear(_t_) ≤ DayWithinYear(_t_) < *304*𝔽 + InLeapYear(_t_) - = *10*𝔽 if *304*𝔽 + InLeapYear(_t_) ≤ DayWithinYear(_t_) < *334*𝔽 + InLeapYear(_t_) - = *11*𝔽 if *334*𝔽 + InLeapYear(_t_) ≤ DayWithinYear(_t_) < *365*𝔽 + InLeapYear(_t_) - -

where

- DayWithinYear(_t_) = Day(_t_) - DayFromYear(YearFromTime(_t_)) -

A month value of *+0*𝔽 specifies January; *1*𝔽 specifies February; *2*𝔽 specifies March; *3*𝔽 specifies April; *4*𝔽 specifies May; *5*𝔽 specifies June; *6*𝔽 specifies July; *7*𝔽 specifies August; *8*𝔽 specifies September; *9*𝔽 specifies October; *10*𝔽 specifies November; and *11*𝔽 specifies December. Note that MonthFromTime(*+0*𝔽) = *+0*𝔽, corresponding to Thursday, 1 January 1970.

- - - -

Date Number

-

A date number is identified by an integral Number in the inclusive interval from *1*𝔽 to *31*𝔽. The mapping DateFromTime(_t_) from a time value _t_ to a date number is defined by:

- - DateFromTime(_t_) - = DayWithinYear(_t_) + *1*𝔽 if MonthFromTime(_t_) is *+0*𝔽 - = DayWithinYear(_t_) - *30*𝔽 if MonthFromTime(_t_) is *1*𝔽 - = DayWithinYear(_t_) - *58*𝔽 - InLeapYear(_t_) if MonthFromTime(_t_) is *2*𝔽 - = DayWithinYear(_t_) - *89*𝔽 - InLeapYear(_t_) if MonthFromTime(_t_) is *3*𝔽 - = DayWithinYear(_t_) - *119*𝔽 - InLeapYear(_t_) if MonthFromTime(_t_) is *4*𝔽 - = DayWithinYear(_t_) - *150*𝔽 - InLeapYear(_t_) if MonthFromTime(_t_) is *5*𝔽 - = DayWithinYear(_t_) - *180*𝔽 - InLeapYear(_t_) if MonthFromTime(_t_) is *6*𝔽 - = DayWithinYear(_t_) - *211*𝔽 - InLeapYear(_t_) if MonthFromTime(_t_) is *7*𝔽 - = DayWithinYear(_t_) - *242*𝔽 - InLeapYear(_t_) if MonthFromTime(_t_) is *8*𝔽 - = DayWithinYear(_t_) - *272*𝔽 - InLeapYear(_t_) if MonthFromTime(_t_) is *9*𝔽 - = DayWithinYear(_t_) - *303*𝔽 - InLeapYear(_t_) if MonthFromTime(_t_) is *10*𝔽 - = DayWithinYear(_t_) - *333*𝔽 - InLeapYear(_t_) if MonthFromTime(_t_) is *11*𝔽 - - - - -

Week Day

-

The weekday for a particular time value _t_ is defined as

- WeekDay(_t_) = 𝔽(ℝ(Day(_t_) + *4*𝔽) modulo 7) -

A weekday value of *+0*𝔽 specifies Sunday; *1*𝔽 specifies Monday; *2*𝔽 specifies Tuesday; *3*𝔽 specifies Wednesday; *4*𝔽 specifies Thursday; *5*𝔽 specifies Friday; and *6*𝔽 specifies Saturday. Note that WeekDay(*+0*𝔽) = *4*𝔽, corresponding to Thursday, 1 January 1970.

+ +

Time-related Constants

+

These constants are referenced by algorithms in the following sections.

+ HoursPerDay = 24 + MinutesPerHour = 60 + SecondsPerMinute = 60 + msPerSecond = *1000*𝔽 + msPerMinute = *60000*𝔽 = msPerSecond × 𝔽(SecondsPerMinute) + msPerHour = *3600000*𝔽 = msPerMinute × 𝔽(MinutesPerHour) + msPerDay = *86400000*𝔽 = msPerHour × 𝔽(HoursPerDay) + + + +

+ Day ( + _t_: a finite time value, + ): an integral Number +

+
+
description
+
It returns the day number of the day in which _t_ falls.
+
+ + 1. Return 𝔽(floor(ℝ(_t_ / msPerDay))). + + + + +

+ TimeWithinDay ( + _t_: a finite time value, + ): an integral Number in the interval from *+0*𝔽 (inclusive) to msPerDay (exclusive) +

+
+
description
+
It returns the number of milliseconds since the start of the day in which _t_ falls.
+
+ + 1. Return 𝔽(ℝ(_t_) modulo ℝ(msPerDay)). + + + + +

+ DaysInYear ( + _y_: an integral Number, + ): *365*𝔽 or *366*𝔽 +

+
+
description
+
It returns the number of days in year _y_. Leap years have 366 days; all other years have 365.
+
+ + 1. Let _ry_ be ℝ(_y_). + 1. If (_ry_ modulo 400) = 0, return *366*𝔽. + 1. If (_ry_ modulo 100) = 0, return *365*𝔽. + 1. If (_ry_ modulo 4) = 0, return *366*𝔽. + 1. Return *365*𝔽. + + + + +

+ DayFromYear ( + _y_: an integral Number, + ): an integral Number +

+
+
description
+
It returns the day number of the first day of year _y_.
+
+ + 1. Let _ry_ be ℝ(_y_). + 1. NOTE: In the following steps, each `_numYearsN_` is the number of years divisible by N that occur between the epoch and the start of year _y_. (The number is negative if _y_ is before the epoch.) + 1. Let _numYears1_ be (_ry_ - 1970). + 1. Let _numYears4_ be floor((_ry_ - 1969) / 4). + 1. Let _numYears100_ be floor((_ry_ - 1901) / 100). + 1. Let _numYears400_ be floor((_ry_ - 1601) / 400). + 1. Return 𝔽(365 × _numYears1_ + _numYears4_ - _numYears100_ + _numYears400_). + + + + +

+ TimeFromYear ( + _y_: an integral Number, + ): a time value +

+
+
description
+
It returns the time value of the start of year _y_.
+
+ + 1. Return msPerDay × DayFromYear(_y_). + + + + +

+ YearFromTime ( + _t_: a finite time value, + ): an integral Number +

+
+
description
+
It returns the year in which _t_ falls.
+
+ + 1. [declared="y"] Return the largest integral Number _y_ (closest to +∞) such that TimeFromYear(_y_) ≤ _t_. + + + + +

+ DayWithinYear ( + _t_: a finite time value, + ): an integral Number in the inclusive interval from *+0*𝔽 to *365*𝔽 +

+
+
+ + 1. Return Day(_t_) - DayFromYear(YearFromTime(_t_)). + + + + +

+ InLeapYear ( + _t_: a finite time value, + ): *+0*𝔽 or *1*𝔽 +

+
+
description
+
It returns *1*𝔽 if _t_ is within a leap year and *+0*𝔽 otherwise.
+
+ + 1. If DaysInYear(YearFromTime(_t_)) is *366*𝔽, return *1*𝔽; else return *+0*𝔽. + + + + +

+ MonthFromTime ( + _t_: a finite time value, + ): an integral Number in the inclusive interval from *+0*𝔽 to *11*𝔽 +

+
+
description
+
It returns a Number identifying the month in which _t_ falls. A month value of *+0*𝔽 specifies January; *1*𝔽 specifies February; *2*𝔽 specifies March; *3*𝔽 specifies April; *4*𝔽 specifies May; *5*𝔽 specifies June; *6*𝔽 specifies July; *7*𝔽 specifies August; *8*𝔽 specifies September; *9*𝔽 specifies October; *10*𝔽 specifies November; and *11*𝔽 specifies December. Note that MonthFromTime(*+0*𝔽) = *+0*𝔽, corresponding to Thursday, 1 January 1970.
+
+ + 1. Let _inLeapYear_ be InLeapYear(_t_). + 1. Let _dayWithinYear_ be DayWithinYear(_t_). + 1. If _dayWithinYear_ < *31*𝔽, return *+0*𝔽. + 1. If _dayWithinYear_ < *59*𝔽 + _inLeapYear_, return *1*𝔽. + 1. If _dayWithinYear_ < *90*𝔽 + _inLeapYear_, return *2*𝔽. + 1. If _dayWithinYear_ < *120*𝔽 + _inLeapYear_, return *3*𝔽. + 1. If _dayWithinYear_ < *151*𝔽 + _inLeapYear_, return *4*𝔽. + 1. If _dayWithinYear_ < *181*𝔽 + _inLeapYear_, return *5*𝔽. + 1. If _dayWithinYear_ < *212*𝔽 + _inLeapYear_, return *6*𝔽. + 1. If _dayWithinYear_ < *243*𝔽 + _inLeapYear_, return *7*𝔽. + 1. If _dayWithinYear_ < *273*𝔽 + _inLeapYear_, return *8*𝔽. + 1. If _dayWithinYear_ < *304*𝔽 + _inLeapYear_, return *9*𝔽. + 1. If _dayWithinYear_ < *334*𝔽 + _inLeapYear_, return *10*𝔽. + 1. Assert: _dayWithinYear_ < *365*𝔽 + _inLeapYear_. + 1. Return *11*𝔽. + + + + +

+ DateFromTime ( + _t_: a finite time value, + ): an integral Number in the inclusive interval from *1*𝔽 to *31*𝔽 +

+
+
description
+
It returns the day of the month in which _t_ falls.
+
+ + 1. Let _inLeapYear_ be InLeapYear(_t_). + 1. Let _dayWithinYear_ be DayWithinYear(_t_). + 1. Let _month_ be MonthFromTime(_t_). + 1. If _month_ is *+0*𝔽, return _dayWithinYear_ + *1*𝔽. + 1. If _month_ is *1*𝔽, return _dayWithinYear_ - *30*𝔽. + 1. If _month_ is *2*𝔽, return _dayWithinYear_ - *58*𝔽 - _inLeapYear_. + 1. If _month_ is *3*𝔽, return _dayWithinYear_ - *89*𝔽 - _inLeapYear_. + 1. If _month_ is *4*𝔽, return _dayWithinYear_ - *119*𝔽 - _inLeapYear_. + 1. If _month_ is *5*𝔽, return _dayWithinYear_ - *150*𝔽 - _inLeapYear_. + 1. If _month_ is *6*𝔽, return _dayWithinYear_ - *180*𝔽 - _inLeapYear_. + 1. If _month_ is *7*𝔽, return _dayWithinYear_ - *211*𝔽 - _inLeapYear_. + 1. If _month_ is *8*𝔽, return _dayWithinYear_ - *242*𝔽 - _inLeapYear_. + 1. If _month_ is *9*𝔽, return _dayWithinYear_ - *272*𝔽 - _inLeapYear_. + 1. If _month_ is *10*𝔽, return _dayWithinYear_ - *303*𝔽 - _inLeapYear_. + 1. Assert: _month_ is *11*𝔽. + 1. Return _dayWithinYear_ - *333*𝔽 - _inLeapYear_. + + + + +

+ WeekDay ( + _t_: a finite time value, + ): an integral Number in the inclusive interval from *+0*𝔽 to *6*𝔽 +

+
+
description
+
It returns a Number identifying the day of the week in which _t_ falls. A weekday value of *+0*𝔽 specifies Sunday; *1*𝔽 specifies Monday; *2*𝔽 specifies Tuesday; *3*𝔽 specifies Wednesday; *4*𝔽 specifies Thursday; *5*𝔽 specifies Friday; and *6*𝔽 specifies Saturday. Note that WeekDay(*+0*𝔽) = *4*𝔽, corresponding to Thursday, 1 January 1970.
+
+ + 1. Return 𝔽(ℝ(Day(_t_) + *4*𝔽) modulo 7). + + + + +

+ HourFromTime ( + _t_: a finite time value, + ): an integral Number in the inclusive interval from *+0*𝔽 to *23*𝔽 +

+
+
description
+
It returns the hour of the day in which _t_ falls.
+
+ + 1. Return 𝔽(floor(ℝ(_t_ / msPerHour)) modulo HoursPerDay). + + + + +

+ MinFromTime ( + _t_: a finite time value, + ): an integral Number in the inclusive interval from *+0*𝔽 to *59*𝔽 +

+
+
description
+
It returns the minute of the hour in which _t_ falls.
+
+ + 1. Return 𝔽(floor(ℝ(_t_ / msPerMinute)) modulo MinutesPerHour). + + + + +

+ SecFromTime ( + _t_: a finite time value, + ): an integral Number in the inclusive interval from *+0*𝔽 to *59*𝔽 +

+
+
description
+
It returns the second of the minute in which _t_ falls.
+
+ + 1. Return 𝔽(floor(ℝ(_t_ / msPerSecond)) modulo SecondsPerMinute). + + + + +

+ msFromTime ( + _t_: a finite time value, + ): an integral Number in the inclusive interval from *+0*𝔽 to *999*𝔽 +

+
+
description
+
It returns the millisecond of the second in which _t_ falls.
+
+ + 1. Return 𝔽(ℝ(_t_) modulo ℝ(msPerSecond)). + @@ -32443,22 +32634,6 @@

- -

Hours, Minutes, Second, and Milliseconds

-

The following abstract operations are useful in decomposing time values:

- HourFromTime(_t_) = 𝔽(floor(ℝ(_t_ / msPerHour)) modulo HoursPerDay) - MinFromTime(_t_) = 𝔽(floor(ℝ(_t_ / msPerMinute)) modulo MinutesPerHour) - SecFromTime(_t_) = 𝔽(floor(ℝ(_t_ / msPerSecond)) modulo SecondsPerMinute) - msFromTime(_t_) = 𝔽(ℝ(_t_) modulo ℝ(msPerSecond)) -

where

- HoursPerDay = 24 - MinutesPerHour = 60 - SecondsPerMinute = 60 - msPerSecond = *1000*𝔽 - msPerMinute = *60000*𝔽 = msPerSecond × 𝔽(SecondsPerMinute) - msPerHour = *3600000*𝔽 = msPerMinute × 𝔽(MinutesPerHour) - -

MakeTime (