/*
A model of dates, times, intervals and durations. Intended as a core library for use by
higher level models that require dates and/or times and/or intervals and/or durations.
The model is based on the ISO 8601 standard for representation of dates and times using
the Gregorian calendar:
https://en.wikipedia.org/wiki/ISO_8601
For dates and times, this model largely conforms to the RFC 3339 profile:
https://tools.ietf.org/html/rfc3339
Exceptions to RFC 3339 are:
- A seconds value of 60 (leap second) is not supported;
- ISO 8601/RFC 3339 impose no limitation on the resolution of times; the finest granularity
of this model is milliseconds.
The model additionally supports a subset of the specification of time intervals and
durations from ISO 8601. Those aspects supported are:
- a duration is expressed as a number of milliseconds;
- an interval is expressed as a start/end date/time value.
All functions are explicit and executable. Where a non-executable condition adds value, it
is included as a comment.
*/
module ISO8601
imports from Numeric all,
from Set all,
from Seq all
exports types struct Year;
struct Month;
struct Day;
struct Hour;
struct Minute;
struct Second;
struct Millisecond;
struct Date;
struct Time;
struct TimeInZone;
struct Offset;
struct DTG;
struct DTGInZone;
struct Interval;
Duration
values MILLIS_PER_SECOND, SECONDS_PER_MINUTE, MINUTES_PER_HOUR, HOURS_PER_DAY, FIRST_YEAR, LAST_YEAR: nat;
DAYS_PER_MONTH, DAYS_PER_MONTH_LEAP: map nat1 to nat1;
MAX_DAYS_PER_MONTH, MONTHS_PER_YEAR, DAYS_PER_YEAR, DAYS_PER_LEAP_YEAR: nat1;
FIRST_DATE, LAST_DATE: Date;
FIRST_TIME, LAST_TIME: Time;
FIRST_DTG, LAST_DTG: DTG;
NO_DURATION, ONE_MILLISECOND, ONE_SECOND, ONE_MINUTE, ONE_HOUR, ONE_DAY, ONE_YEAR, ONE_LEAP_YEAR: Duration
functions isLeap: Year +> bool;
daysInMonth: Year * Month +> nat1;
daysInYear: Year +> nat1;
dtgInRange: DTG * DTG * DTG +> bool;
inInterval: DTG * Interval +> bool;
dtgWithin: DTG * Duration * DTG +> bool;
overlap: Interval * Interval +> bool;
within: Interval * Interval +> bool;
add: DTG * Duration +> DTG;
subtract: DTG * Duration +> DTG;
diff: DTG * DTG +> Duration;
durAdd: Duration * Duration +> Duration;
durSubtract: Duration * Duration +> Duration;
durMultiply: Duration * nat +> Duration;
durDivide: Duration * nat +> Duration;
durDiff: Duration * Duration +> Duration;
durToMillis: Duration +> nat;
durFromMillis: nat +> Duration;
durToSeconds: Duration +> nat;
durFromSeconds: nat +> Duration;
durToMinutes: Duration +> nat;
durFromMinutes: nat +> Duration;
durModMinutes : Duration +> Duration;
durToHours: Duration +> nat;
durFromHours: nat +> Duration;
durModHours : Duration +> Duration;
durToDays: Duration +> nat;
durFromDays : nat +> Duration;
durModDays : Duration +> Duration;
durToMonth: Duration * Year +> nat;
durFromMonth: Year * Month +> Duration;
durUptoMonth: Year * Month +> Duration;
durToYear : Duration * Year +> nat;
durFromYear: Year +> Duration;
durUptoYear: Year +> Duration;
durToDTG: Duration +> DTG;
durFromDTG: DTG +> Duration;
durToDate: Duration +> Date;
durFromDate: Date +> Duration;
durToTime: Duration +> Time;
durFromTime: Time +> Duration;
durFromTimeInZone: TimeInZone +> Duration;
durFromInterval: Interval +> Duration;
finestGranularity: DTG * Duration +> bool;
finestGranularityI: Interval * Duration +> bool;
minDTG: set1 of DTG +> DTG;
maxDTG: set1 of DTG +> DTG;
minDate: set1 of Date +> Date;
maxDate: set1 of Date +> Date;
minTime: set1 of Time +> Time;
maxTime: set1 of Time +> Time;
minDuration: set1 of Duration +> Duration;
maxDuration: set1 of Duration +> Duration;
sumDuration: seq of Duration +> Duration;
instant: DTG +> Interval;
nextDateForYM: Date +> Date;
nextDateForDay: Date * Day +> Date;
previousDateForYM: Date +> Date;
previousDateForDay: Date * Day +> Date;
normalise: DTGInZone +> DTG;
normaliseTime: TimeInZone +> Time * [PlusOrMinus];
formatDTG: DTG +> seq of char;
formatDTGInZone: DTGInZone +> seq of char;
formatDate: Date +> seq of char;
formatTime: Time +> seq of char;
formatTimeInZone: TimeInZone +> seq of char;
formatInterval: Interval +> seq of char;
formatDuration: Duration +> seq of char
definitions
types
-- A year: 0 = 0AD (or 1BC).
Year = nat
inv year == FIRST_YEAR <= year and year <= LAST_YEAR;
-- A month in a year (January is numbered 1).
Month = nat1
inv month == month <= MONTHS_PER_YEAR;
-- A day in a month.
Day = nat1
inv day == day <= MAX_DAYS_PER_MONTH;
-- An hour in a day.
Hour = nat
inv hour == hour < HOURS_PER_DAY;
-- A minute in an hour.
Minute = nat
inv minute == minute < MINUTES_PER_HOUR;
-- A second in a minute.
Second = nat
inv second == second < SECONDS_PER_MINUTE;
-- A millisecond in a second.
Millisecond = nat
inv milli == milli < MILLIS_PER_SECOND;
-- A date is a triple (year/month/day).
-- Day of month must be consistent with respect to year.
Date :: year : Year
month: Month
day : Day
inv mk_Date(y,m,d) == d <= daysInMonth(y,m)
ord mk_Date(y1,m1,d1) < mk_Date(y2,m2,d2) ==
Seq`lexicographic[nat]([y1,m1,d1], [y2,m2,d2]);
-- A Time consists of four elements (hours/minutes/seconds/milliseconds).
Time :: hour : Hour
minute: Minute
second: Second
milli : Millisecond
ord mk_Time(h1,m1,s1,l1) < mk_Time(h2,m2,s2,l2) ==
Seq`lexicographic[nat]([h1,m1,s1,l1], [h2,m2,s2,l2]);
-- A time in a zone consists of a time and a time zone offset.
TimeInZone :: time : Time
offset: Offset
eq t1 = t2 == normaliseTime(t1).#1 = normaliseTime(t2).#1
ord t1 < t2 == normaliseTime(t1).#1 < normaliseTime(t2).#1;
-- The timezone offset
Offset :: delta: Duration
pm : PlusOrMinus
inv os == -- Offset must be less than one day and an integral number of minutes.
os.delta < ONE_DAY and durModMinutes(os.delta) = NO_DURATION
eq mk_Offset(d1,o1) = mk_Offset(d2,o2) ==
d1 = d2 and o1 = o2 or d1 = NO_DURATION and d2 = NO_DURATION;
-- The direction of a time zone offset.
PlusOrMinus = <PLUS> | <MINUS>;
-- A DTG (date/time group) is a combined date and time.
DTG :: date: Date
time: Time
ord mk_DTG(d1,t1) < mk_DTG(d2,t2) == d1 < d2 or d1 = d2 and t1 < t2;
-- A date and time with time zone offset.
DTGInZone :: date: Date
time: TimeInZone
inv mk_DTGInZone(date,time) ==
let changeDay = normaliseTime(time).#2
in -- Adjusted time must not be earlier than 0000-01-01T00:00:00Z.
not (date = FIRST_DATE and changeDay = <PLUS>) and
-- Adjusted time must not be later than 9999-12-31T23:59:59,999Z
not (date = LAST_DATE and changeDay = <MINUS>)
eq dtg1 = dtg2 == normalise(dtg1) = normalise(dtg2)
ord dtg1 < dtg2 == normalise(dtg1) < normalise(dtg2);
-- An interval is a pair of DTGs representing all time instants between the start (inclusive)
-- and end (exclusive) values.
Interval :: begins: DTG
ends : DTG
inv ival == -- The start of the interval must be earlier than the end.
ival.begins < ival.ends;
-- Duration: a period of time in milliseconds.
Duration :: dur: nat
ord d1 < d2 == d1.dur < d2.dur;
values
MILLIS_PER_SECOND:nat = 1000;
SECONDS_PER_MINUTE:nat = 60;
MINUTES_PER_HOUR:nat = 60;
HOURS_PER_DAY:nat = 24;
DAYS_PER_MONTH:map nat1 to nat1 = {1|->31, 2|->28, 3|->31, 4|->30, 5|->31, 6|->30,
7|->31, 8|->31, 9|->30, 10|->31, 11|->30, 12|->31};
DAYS_PER_MONTH_LEAP:map nat1 to nat1 = DAYS_PER_MONTH ++ {2|->29};
MAX_DAYS_PER_MONTH:nat1 = Set`max[nat1](rng DAYS_PER_MONTH);
MONTHS_PER_YEAR:nat1 = card dom DAYS_PER_MONTH;
DAYS_PER_YEAR:nat1 = daysInYear(1); -- 1 is an arbitrary non-leap year.
DAYS_PER_LEAP_YEAR:nat1 = daysInYear(4); -- 4 is an arbitrary leap year.
FIRST_YEAR:nat = 0;
LAST_YEAR:nat = 9999;
FIRST_DATE:Date = mk_Date(FIRST_YEAR,1,1);
LAST_DATE:Date = mk_Date(LAST_YEAR,12,31);
FIRST_TIME:Time = mk_Time(0,0,0,0);
LAST_TIME:Time = mk_Time(23,59,59,999);
FIRST_DTG:DTG = mk_DTG(FIRST_DATE, FIRST_TIME);
LAST_DTG:DTG = mk_DTG(LAST_DATE, LAST_TIME);
NO_DURATION:Duration = durFromMillis(0);
ONE_MILLISECOND:Duration = durFromMillis(1);
ONE_SECOND:Duration = durFromSeconds(1);
ONE_MINUTE:Duration = durFromMinutes(1);
ONE_HOUR:Duration = durFromHours(1);
ONE_DAY:Duration = durFromDays(1);
ONE_YEAR:Duration = durFromDays(DAYS_PER_YEAR);
ONE_LEAP_YEAR:Duration = durFromDays(DAYS_PER_LEAP_YEAR);
functions
-- Is a year a leap year?
isLeap: Year +> bool
isLeap(year) == year rem 4 = 0 and (year rem 100 = 0 => year rem 400 = 0);
-- The number of days in a month with respect to a year.
daysInMonth: Year * Month +> nat1
daysInMonth(year, month) ==
if isLeap(year) then DAYS_PER_MONTH_LEAP(month) else DAYS_PER_MONTH(month);
-- The number of days in a year.
daysInYear: Year +> nat1
daysInYear(year) == Seq`sum([daysInMonth(year,m) | m in set {1,...,MONTHS_PER_YEAR}]);
-- Does a DTG fall between two given DTGs?
-- Start is inclusive, end is exclusive.
dtgInRange: DTG * DTG * DTG +> bool
dtgInRange(dtg1, dtg2, dtg3) == dtg1 <= dtg2 and dtg2 < dtg3;
-- Is a DTG within a specified duration of another DTG?
dtgWithin: DTG * Duration * DTG +> bool
dtgWithin(dtg, dur, target) ==
inInterval(dtg, mk_Interval(subtract(target, dur), add(target, dur)));
-- Does a DTG fall within an interval?
inInterval: DTG * Interval +> bool
inInterval(dtg, ival) == dtgInRange(ival.begins, dtg, ival.ends);
-- Do two intervals overlap?
overlap: Interval * Interval +> bool
overlap(i1, i2) == i2.begins < i1.ends and i1.begins < i2.ends;
--post RESULT = exists d:DTG & inInterval(d, i1) and inInterval(d, i2);
-- Does one interval fall wholly within another interval?
within: Interval * Interval +> bool
within(i1, i2) == i2.begins <= i1.begins and i1.ends <= i2.ends;
--post RESULT = forall d:DTG & inInterval(d, i1) => inInterval(d, i2);
-- Increase a DTG by a duration.
add: DTG * Duration +> DTG
add(dtg, dur) == durToDTG(durAdd(durFromDTG(dtg), dur))
post subtract(RESULT, dur) = dtg;
-- Decrease a DTG by a duration.
subtract: DTG * Duration +> DTG
subtract(dtg, dur) == durToDTG(durDiff(durFromDTG(dtg), dur))
pre dur <= durFromDTG(dtg);
--post add(RESULT,dur) = dtg;
-- The duration between two DTGs.
diff: DTG * DTG +> Duration
diff(dtg1, dtg2) == durDiff(durFromDTG(dtg1), durFromDTG(dtg2))
post (dtg1 <= dtg2 => add(dtg1,RESULT) = dtg2) and
(dtg2 <= dtg1 => add(dtg2,RESULT) = dtg1);
-- Add two durations.
durAdd: Duration * Duration +> Duration
durAdd(d1, d2) == mk_Duration(d1.dur + d2.dur)
--post durDiff(RESULT, d1) = d2 and durDiff(RESULT,d2) = d1;
post durSubtract(RESULT, d1) = d2 and
durSubtract(RESULT, d2) = d1;
-- Subtract one duration from another.
durSubtract: Duration * Duration +> Duration
durSubtract(d1, d2) == mk_Duration(d1.dur - d2.dur)
pre d1 >= d2;
--post durAdd(RESULT, d2) = d1;
-- Multiply a duration by a fixed amount.
durMultiply: Duration * nat +> Duration
durMultiply(d, n) == mk_Duration(d.dur * n)
post durDivide(RESULT, n) = d;
-- Divide a duration by a fixed amount.
durDivide: Duration * nat +> Duration
durDivide(d, n) == mk_Duration(d.dur div n);
--post durMultiply(RESULT, n) <= d and d < durMultiply(RESULT, n+1);
-- The difference between two durations.
durDiff: Duration * Duration +> Duration
durDiff(d1, d2) == mk_Duration(abs(d1.dur - d2.dur))
post (d1 <= d2 => durAdd(d1,RESULT) = d2) and (d2 <= d1 => durAdd(d2,RESULT) = d1);
-- The whole number of milliseconds in a duration.
durToMillis: Duration +> nat
durToMillis(d) == d.dur
post durFromMillis(RESULT) = d;
-- The duration of a number of milliseconds.
durFromMillis: nat +> Duration
durFromMillis(sc) == mk_Duration(sc);
--post durToMillis(RESULT) = sc;
-- The whole number of seconds in a duration.
durToSeconds: Duration +> nat
durToSeconds(d) == durToMillis(d) div MILLIS_PER_SECOND
post durFromSeconds(RESULT) <= d and d < durFromSeconds(RESULT+1);
-- The duration of a number of seconds.
durFromSeconds: nat +> Duration
durFromSeconds(sc) == durFromMillis(sc*MILLIS_PER_SECOND);
--post durToSeconds(RESULT) = sc;
-- The whole number of minutes in a duration.
durToMinutes: Duration +> nat
durToMinutes(d) == durToSeconds(d) div SECONDS_PER_MINUTE
post durFromMinutes(RESULT) <= d and d < durFromMinutes(RESULT+1);
-- The duration of a number of minutes.
durFromMinutes: nat +> Duration
durFromMinutes(mn) == durFromSeconds(mn*SECONDS_PER_MINUTE);
--post durToMinutes(RESULT) = mn;
-- Remove all whole minutes from a duration.
durModMinutes : Duration +> Duration
durModMinutes(d) == mk_Duration(d.dur rem ONE_MINUTE.dur)
post RESULT < ONE_MINUTE;
--exists n:nat & durAdd(durFromMinutes(n),RESULT) = d
-- The whole number of hours in a duration.
durToHours: Duration +> nat
durToHours(d) == durToMinutes(d) div MINUTES_PER_HOUR
post durFromHours(RESULT) <= d and d < durFromHours(RESULT+1);
-- The duration of a number of hours.
durFromHours: nat +> Duration
durFromHours(hr) == durFromMinutes(hr*MINUTES_PER_HOUR);
--post durToHours(RESULT) = hr;
-- Remove all whole hours from a duration.
durModHours : Duration +> Duration
durModHours(d) == mk_Duration(d.dur rem ONE_HOUR.dur)
post RESULT < ONE_HOUR;
--exists n:nat & durAdd(durFromHours(n),RESULT) = d
-- The whole number of days in a duration.
durToDays: Duration +> nat
durToDays(d) == durToHours(d) div HOURS_PER_DAY
post durFromDays(RESULT) <= d and d < durFromDays(RESULT+1);
-- The duration of a number of days.
durFromDays: nat +> Duration
durFromDays(dy) == durFromHours(dy*HOURS_PER_DAY);
--post durToDays(RESULT) = dy;
-- Remove all whole days from a duration.
durModDays : Duration +> Duration
durModDays(d) == mk_Duration(d.dur rem ONE_DAY.dur)
post RESULT < ONE_DAY;
--exists n:nat & durAdd(durFromDays(n),RESULT) = d
-- The whole number of months in a duration (with respect to a year).
durToMonth: Duration * Year +> nat
durToMonth(dur, year) ==
Set`max[Month]({ m | m in set {1,...,MONTHS_PER_YEAR} & durUptoMonth(year,m) <= dur }) - 1
pre dur < durFromYear(year);
-- The duration of a month (with respect to a year).
durFromMonth: Year * Month +> Duration
durFromMonth(year, month) == durFromDays(daysInMonth(year,month));
-- The duration up to the start of a month (with respect to a year).
durUptoMonth: Year * Month +> Duration
durUptoMonth(year, month) == sumDuration([durFromMonth(year,m) | m in set {1,...,month-1}]);
-- The whole number of years in a duration (starting from a reference year).
durToYear : Duration * Year +> nat
durToYear(dur, year) ==
if dur < durFromYear(year)
then 0
else 1 + durToYear(durDiff(dur, durFromYear(year)), year+1)
--post RESULT = Set`max({ y | y : Year & durUptoYear(year+y) <= dur })
measure m_durToYear;
-- The measure function for durToYear
m_durToYear : Duration * Year +> nat
m_durToYear(d,-) == d.dur;
-- The duration of a year.
durFromYear: Year +> Duration
durFromYear(year) == durFromDays(daysInYear(year));
-- The duration up to the start of a year.
durUptoYear: Year +> Duration
durUptoYear(year) == sumDuration([durFromYear(y) | y in set {FIRST_YEAR,...,year-1}]);
-- The DTG corresponding to a duration.
durToDTG: Duration +> DTG
durToDTG(dur) == let dy = durFromDays(durToDays(dur))
in mk_DTG(durToDate(dy),durToTime(durDiff(dur,dy)))
post durFromDTG(RESULT) = dur;
-- The duration of a DTG (with respect to the start of time).
durFromDTG: DTG +> Duration
durFromDTG(dtg) == durAdd(durFromDate(dtg.date),durFromTime(dtg.time));
--post durToDTG(RESULT) = dtg;
-- The date corresponding to a duration.
durToDate: Duration +> Date
durToDate(dur) == let yr = durToYear(dur,FIRST_YEAR),
ydur = durDiff(dur, durUptoYear(yr)),
mn = durToMonth(ydur,yr)+1,
dy = durToDays(durDiff(ydur, durUptoMonth(yr,mn)))+1
in mk_Date(yr,mn,dy)
post durFromDate(RESULT) <= dur and dur < durAdd(durFromDate(RESULT),ONE_DAY);
-- The duration of a date (with respect to the start of time).
durFromDate: Date +> Duration
durFromDate(date) ==
durAdd(durUptoYear(date.year),
durAdd(durUptoMonth(date.year,date.month), durFromDays(date.day-1)));
--post durToDate(RESULT) = date;
-- The time corresponding to a duration.
durToTime: Duration +> Time
durToTime(dur) == let hr = durToHours(dur),
mn = durToMinutes(durDiff(dur,durFromHours(hr))),
hmd = durAdd(durFromHours(hr),durFromMinutes(mn)),
sc = durToSeconds(durDiff(dur,hmd)),
ml = durToMillis(durDiff(dur,durAdd(hmd,durFromSeconds(sc))))
in mk_Time(hr,mn,sc,ml)
pre dur < ONE_DAY
post durFromTime(RESULT) = dur;
-- The duration of a time.
durFromTime: Time +> Duration
durFromTime(time) ==
durAdd(durFromHours(time.hour),
durAdd(durFromMinutes(time.minute),
durAdd(durFromSeconds(time.second),durFromMillis(time.milli))));
--post durToTime(RESULT) = time;
-- The duration of a time with respect to a time zone.
durFromTimeInZone: TimeInZone +> Duration
durFromTimeInZone(time) ==
let ntime = normaliseTime(time).#1
in durFromTime(ntime);
--post durToTime(RESULT) = time;
-- The duration of a time interval.
durFromInterval: Interval +> Duration
durFromInterval(i) == diff(i.begins, i.ends)
post add(i.begins, RESULT) = i.ends;
-- Is a DTG expressed no finer than a specified granularity.
finestGranularity: DTG * Duration +> bool
finestGranularity(dtg, dur) == durFromDTG(dtg).dur mod dur.dur = 0
pre dur <> NO_DURATION;
--post RESULT = exists n:nat & durMultiply(dur, n) = durFromDTG(dtg);
-- Are the DTGs in an interval expressed no finer than a specified granularity.
finestGranularityI: Interval * Duration +> bool
finestGranularityI(i, dur) ==
finestGranularity(i.begins, dur) and finestGranularity(i.ends, dur);
-- The minimum DTG in a set.
minDTG: set1 of DTG +> DTG
minDTG(dtgs) == Set`min[DTG](dtgs)
post RESULT in set dtgs and forall d in set dtgs & RESULT <= d;
-- The maximum DTG in a set.
maxDTG: set1 of DTG +> DTG
maxDTG(dtgs) == Set`max[DTG](dtgs)
post RESULT in set dtgs and forall d in set dtgs & RESULT >= d;
-- The minimum Date in a set.
minDate: set1 of Date +> Date
minDate(dates) == Set`min[Date](dates)
post RESULT in set dates and forall d in set dates & RESULT <= d;
-- The maximum Date in a set.
maxDate: set1 of Date +> Date
maxDate(dates) == Set`max[Date](dates)
post RESULT in set dates and forall d in set dates & RESULT >= d;
-- The minimum Time in a set.
minTime: set1 of Time +> Time
minTime(times) == Set`min[Time](times)
post RESULT in set times and forall t in set times & RESULT <= t;
-- The maximum Time in a set.
maxTime: set1 of Time +> Time
maxTime(times) == Set`max[Time](times)
post RESULT in set times and forall t in set times & RESULT >= t;
-- The minimum Duration in a set.
minDuration: set1 of Duration +> Duration
minDuration(durs) == Set`min[Duration](durs)
post RESULT in set durs and forall d in set durs & RESULT <= d;
-- The maximum Duration in a set.
maxDuration: set1 of Duration +> Duration
maxDuration(durs) == Set`max[Duration](durs)
post RESULT in set durs and forall d in set durs & RESULT >= d;
-- The sum of a sequence of durations.
sumDuration: seq of Duration +> Duration
sumDuration(sd) == mk_Duration(Seq`sum([ d.dur | d in seq sd ]));
-- An interval that represents an instant in time.
instant: DTG +> Interval
instant(dtg) == mk_Interval(dtg, add(dtg, ONE_MILLISECOND))
post inInterval(dtg, RESULT);
--and forall d:DTG & d = dtg <=> inInterval(d,RESULT);
-- Given a date, find the next date on which the day of month is the same.
nextDateForYM: Date +> Date
nextDateForYM(date) == nextDateForDay(date, date.day);
--post RESULT = minDate({ dt | dt:Date & dt > date and dt.day = date.day});
-- Given a date and specific day, find the closest next date on which the day of month is the
-- same as the specified day.
nextDateForDay: Date * Day +> Date
nextDateForDay(date, day) == nextYMDForDay(date.year, date.month, date.day, day)
pre day <= MAX_DAYS_PER_MONTH;
--post RESULT = minDate({ dt | dt:Date & dt > date and dt.day = day });
-- Given a year/month/day, find the closest next date on which the day of month is the same.
nextYMDForDay: Year * Month * Day * Day +> Date
nextYMDForDay(yy, mm, dd, day) ==
let nextm = if mm = MONTHS_PER_YEAR then 1 else mm+1,
nexty = if mm = MONTHS_PER_YEAR then yy+1 else yy
in if dd < day and day <= daysInMonth(yy, mm)
then mk_Date(yy, mm, day)
elseif day = 1
then mk_Date(nexty, nextm, day)
else nextYMDForDay(nexty, nextm, 1, day)
pre dd <= daysInMonth(yy, mm)
--post RESULT = minDate({ date | date:Date & date > mk_Date(yy, mm, dd) and
-- date.day = day })
measure m_nextYMDForDay;
-- The measure function for nextYMDForDay
m_nextYMDForDay: Year * Month * Day * Day +> nat
m_nextYMDForDay(y,m,-,-) == ((LAST_YEAR+1)*MONTHS_PER_YEAR) - (y*MONTHS_PER_YEAR + m);
-- Given a date, find the previous date on which the day of month is the same.
previousDateForYM: Date +> Date
previousDateForYM(date) == previousDateForDay(date, date.day);
--post RESULT = maxDate({ dt | dt:Date & dt date and dt.day = date.day });
-- Given a date and specific day, find the closest previous date on which the day of month is
-- the same as the specified day.
previousDateForDay: Date * Day +> Date
previousDateForDay(date, day) == previousYMDForDay(date.year, date.month, date.day, day)
pre day <= MAX_DAYS_PER_MONTH;
--post RESULT = maxDate({ dt | dt:Date & dt < date and dt.day = day });
-- Given a date, find the closest later date on which the day of month is the same.
previousYMDForDay: Year * Month * Day * Day +> Date
previousYMDForDay(yy, mm, dd, day) ==
let prevm = if mm > 1 then mm-1 else MONTHS_PER_YEAR,
prevy = if mm > 1 then yy else yy-1
in if day < dd
then mk_Date(yy, mm, day)
elseif day <= daysInMonth(prevy, prevm)
then mk_Date(prevy, prevm, day)
else previousYMDForDay(prevy, prevm, 1, day)
pre dd <= daysInMonth(yy, mm)
--post RESULT = maxDate({ date | date:Date & date < mk_Date(yy, mm, dd) and
-- date.day = day })
measure m_previousYMDForDay;
-- The measure function for previousYMDForDay
m_previousYMDForDay: Year * Month * Day * Day +> nat
m_previousYMDForDay(y,m,-,-) == y*MONTHS_PER_YEAR + m;
-- Normalise a DTG value such that it is expressed without time zone offset.
-- Applying the offset may result in a change of date.
-- Example: 2001-01-01T01:00+02:00 becomes 2000-12-31T23:00Z.
normalise: DTGInZone +> DTG
normalise(dtg) == let mk_(ntime,pm) = normaliseTime(dtg.time),
baseDtg = mk_DTG(dtg.date, ntime)
in cases pm:
<PLUS> -> subtract(baseDtg, ONE_DAY),
<MINUS> -> add(baseDtg, ONE_DAY)
end;
-- Normalise a time value with a time zone offset to the UTC value, wrapping across the day
-- boundary. Return an indication if the normalisation pushes the time to a different day.
-- Example: 01:00+02:00 (01:00, two hours ahead of UTC) becomes (23:00Z,<PLUS>) indicating
-- the original time with offset is on the day after the UTC time.
-- Similarly, 23:30-01:15 becomes (00:45,<MINUS>).
normaliseTime: TimeInZone +> Time * [PlusOrMinus]
normaliseTime(time) ==
let utcTimeDur = durFromTime(time.time)
in cases time.offset:
mk_Offset(offset,<PLUS>)
-> -- Zone offset ahead of UTC
if offset <= utcTimeDur
then -- No day change
mk_(durToTime(durSubtract(utcTimeDur,offset)), nil)
else -- UTC time one day earlier
mk_(durToTime(durSubtract(durAdd(utcTimeDur,ONE_DAY),offset)),<PLUS>),
mk_Offset(offset,<MINUS>)
-> -- Zone offset behind UTC
let adjusted = durAdd(utcTimeDur,offset)
in if adjusted < ONE_DAY
then -- No day change
mk_(durToTime(adjusted),nil)
else -- UTC time one day later
mk_(durToTime(durSubtract(adjusted,ONE_DAY)),<MINUS>)
end;
-- Format a date and time as per ISO 8601.
formatDTG: DTG +> seq of char
formatDTG(dtg) == formatDate(dtg.date) ^ "T" ^ formatTime(dtg.time);
-- Format a date and time with a time zone offset as per ISO 8601.
formatDTGInZone: DTGInZone +> seq of char
formatDTGInZone(dtg) == formatDate(dtg.date) ^ "T" ^ formatTimeInZone(dtg.time);
-- Format a date as per ISO 8601.
formatDate: Date +> seq of char
formatDate(mk_Date(y,m,d)) ==
Numeric`zeroPad(y,4) ^ "-" ^ Numeric`zeroPad(m,2) ^ "-" ^ Numeric`zeroPad(d,2);
-- Format a time as per ISO 8601.
formatTime: Time +> seq of char
formatTime(mk_Time(h,m,s,l)) ==
let frac = if l = 0 then "" else "," ^ Numeric`zeroPad(l,3)
in Numeric`zeroPad(h,2) ^ ":" ^ Numeric`zeroPad(m,2) ^ ":" ^
Numeric`zeroPad(s,2) ^ frac;
-- Format a time with a time zone offset as per ISO 8601.
formatTimeInZone: TimeInZone +> seq of char
formatTimeInZone(mk_TimeInZone(time,o)) ==
formatTime(time) ^ (if o.delta = NO_DURATION then "Z" else formatOffset(o));
-- Format a time offset as per ISO 8601.
formatOffset: Offset +> seq of char
formatOffset(mk_Offset(dur,pm)) ==
let hm = durToTime(dur),
sign = if pm = <PLUS> then "+" else "-"
in sign ^ Numeric`zeroPad(hm.hour,2) ^ ":" ^ Numeric`zeroPad(hm.minute,2);
-- Format a DTG interval as per ISO 8601.
formatInterval: Interval +> seq of char
formatInterval(interval) == formatDTG(interval.begins) ^ "/" ^ formatDTG(interval.ends);
-- Format a duration as per ISO 8601.
formatDuration: Duration +> seq of char
formatDuration(d) ==
let numDays = durToDays(d),
mk_Time(h,m,s,l) = durToTime(durModDays(d)),
item: nat * char +> seq of char
item(n,c) == if n = 0 then "" else Numeric`formatNat(n)^[c],
itemSec: nat * nat +> seq of char
itemSec(x,y) == Numeric`formatNat(x) ^ "." ^ Numeric`zeroPad(y,3) ^ "S",
date = item(numDays,'D'),
time = item(h,'H') ^ item(m,'M') ^ if l=0 then item(s,'S') else itemSec(s,l)
in if date="" and time=""
then "PT0S"
else "P" ^ date ^ (if time="" then "" else "T" ^ time);
end ISO8601
¤ Dauer der Verarbeitung: 0.32 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
