Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ISO8601.vdmsl Sprache: VDM

Original von: VDM^©

/*
   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 Offset
              struct UTC
              struct DTG
              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;
               NO_DURATION, ONE_MILLISECOND, ONE_SECOND, ONE_MINUTE, ONE_HOUR, ONE_DAY, ONE_YEAR, ONE_LEAP_YEAR: Duration
        functions mkUTC: Hour * Minute * Second +> UTC
                  isUTC: Time +> bool
                  toUTC: Time +> UTC
                  isLeap: Year +> bool
                  daysInMonth: Year * Month +> nat1
                  daysInYear: Year +> nat1
                  dateLess: Date * Date +> bool
                  dateLeq: Date * Date +> bool
                  dateGrtr: Date * Date +> bool
                  dateGeq: Date * Date +> bool
                  timeEq: Time * Time +> bool
                  timeLess: Time * Time +> bool
                  utcLess: UTC * UTC +> bool
                  timeLeq: Time * Time +> bool
                  timeGrtr: Time * Time +> bool
                  timeGeq: Time * Time +> bool
                  dtgEq: DTG * DTG +> bool
                  dtgLess: DTG * DTG +> bool
                  dtgLeq: DTG * DTG +> bool
                  dtgGrtr: DTG * DTG +> bool
                  dtgGeq: DTG * DTG +> bool
                  durLess: Duration * Duration +> bool
                  durLeq: Duration * Duration +> bool
                  durGrtr: Duration * Duration +> bool
                  durGeq: Duration * Duration +> bool
                  dtgInRange: DTG * DTG * DTG +> bool
                  inInterval: DTG * Interval +> 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 +> UTC
                  durFromTime: Time +> Duration
                  durFromInterval: Interval +> Duration
                  minDTG: set of DTG +> DTG
                  maxDTG: set of DTG +> DTG
                  minDate: set of Date +> Date
                  maxDate: set of Date +> Date
                  minTime: set of Time +> Time
                  maxTime: set of Time +> Time
                  minDuration: set of Duration +> Duration
                  maxDuration: set of Duration +> Duration
                  sumDuration: seq of Duration +> Duration
                  instant: DTG +> Interval
                  format: DTG +> seq of char
                  formatDate: Date +> seq of char
                  formatTime: Time +> seq of char
                  formatInterval: Interval +> seq of char
                  formatDuration: Duration +> seq of char
                  normalise: DTG +> DTG

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);

  -- A time consists of four elements (hours/minutes/seconds/milliseconds),
  -- optionally with a time zone offset.
  Time :: hour  :Hour
          minute:Minute
          second:Second
          milli :Millisecond
          offset:[Offset];

  -- The timezone offset
  Offset :: delta:Duration
            pm   :[PlusOrMinus]
            -- Offset must be less than one day and an integral number of minutes.
  inv os == durLess(os.delta, ONE_DAY) and durModMinutes(os.delta) = NO_DURATION;

  PlusOrMinus = <PLUS> | <MINUS>;

  -- UTC time: a time with no offset.
  UTC = Time
  inv utc == utc.offset = nil;

  -- A DTG (date/time group) is a combined date and time.
  DTG :: date:Date
         time:Time
  inv mk_DTG(date,time) ==
        let utcTimeDur = durFromUTCTime(toUTC(time))
        in -- Adjusted time must not be earlier than 0000-01-01T00:00:00Z.
           (date = FIRST_DATE and time.offset <> nil and time.offset.pm = <PLUS> =>
                durGeq(utcTimeDur,time.offset.delta)) and
           -- Adjusted time must not be later than 9999-12-31T23:59:59,999Z
           (date = LAST_DATE and time.offset <> nil and time.offset.pm = <MINUS> =>
                durLess(durAdd(utcTimeDur,time.offset.delta),ONE_DAY));

  -- An interval is a pair of DTGs representing all time instants between those
  -- bounding values (inclusive).
  -- The end of the interval must not be earlier than the start.
  Interval :: begins:DTG
              ends  :DTG
  inv ival == dtgLeq(ival.begins, ival.ends);

  -- Duration: a period of time in milliseconds.
  Duration :: dur:nat;

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(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);
  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

  -- Create a UTC time (without milliseconds).
  mkUTC: Hour * Minute * Second +> UTC
  mkUTC(h,m,s) == mk_Time(h,m,s,0,nil);

  -- Is a time in UTC?
  isUTC: Time +> bool
  isUTC(time) == time.offset = nil;

  -- Drop the offset part of a time.
  toUTC: Time +> UTC
  toUTC(time) == mu(time, offset|->nil);

  -- 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}]);

  -- Order relation on dates.
  dateLess: Date * Date +> bool
  dateLess(mk_Date(y1,m1,d1), mk_Date(y2,m2,d2)) ==
    y1<y2 or (y1=y2 and m1<m2) or (y1=y2 and m1=m2 and d1<d2);

  -- Less than or equal relation on dates.
  dateLeq: Date * Date +> bool
  dateLeq(date1,date2) == dateLess(date1, date2) or date1 = date2;

  -- Greater than relation on dates.
  dateGrtr: Date * Date +> bool
  dateGrtr(d1, d2) == dateLess(d2, d1);

  -- Greater than or equal relation on dates.
  dateGeq: Date * Date +> bool
  dateGeq(d1, d2) == dateLeq(d2, d1);

  -- Equality relation on times.
  -- Primitive equality insufficient since offset must be considered.
  timeEq: Time * Time +> bool
  timeEq(time1, time2) == normaliseTime(time1) = normaliseTime(time2);

  -- Order relation on times.
  timeLess: Time * Time +> bool
  timeLess(time1, time2) ==
    utcLess(normaliseTime(time1).#1, normaliseTime(time2).#1);

  -- Order relation on UTC times.
  utcLess: UTC * UTC +> bool
  utcLess(mk_Time(h1,m1,s1,l1,-), mk_Time(h2,m2,s2,l2,-)) ==
    h1<h2 or (h1=h2 and m1<m2) or (h1=h2 and m1=m2 and s1<s2) or
    (h1=h2 and m1=m2 and s1=s2 and l1<l2);

  -- Less than or equal relation on times.
  timeLeq: Time * Time +> bool
  timeLeq(time1, time2) == timeLess(time1, time2) or timeEq(time1, time2);

  -- Greater than relation on times.
  timeGrtr: Time * Time +> bool
  timeGrtr(d1, d2) == timeLess(d2, d1);

  -- Greater than or equal relation on times.
  timeGeq: Time * Time +> bool
  timeGeq(d1, d2) == timeLeq(d2, d1);

  -- Equality relation on DTGs: are their normalised values identical?
  -- Primitive equality insufficient since primitive equality on times is insufficient.
  dtgEq: DTG * DTG +> bool
  dtgEq(dtg1, dtg2) == normalise(dtg1) = normalise(dtg2);

  -- Order relation on DTGs.
  dtgLess: DTG * DTG +> bool
  dtgLess(dtg1, dtg2) ==
    let n1 = normalise(dtg1),
        n2 = normalise(dtg2)
    in dateLess(n1.date,n2.date) or (n1.date=n2.date and utcLess(n1.time,n2.time));

  -- Less than or equal relation on DTGs.
  dtgLeq: DTG * DTG +> bool
  dtgLeq(dtg1, dtg2) == dtgLess(dtg1, dtg2) or dtgEq(dtg1, dtg2);

  -- Greater than relation on DTGs.
  dtgGrtr: DTG * DTG +> bool
  dtgGrtr(d1, d2) == dtgLess(d2, d1);

  -- Greater than or equal relation on DTGs.
  dtgGeq: DTG * DTG +> bool
  dtgGeq(d1, d2) == dtgLeq(d2, d1);

  -- Order relation on durations.
  durLess: Duration * Duration +> bool
  durLess(d1, d2) == d1.dur < d2.dur;

  -- Less than or equal relation on durations.
  durLeq: Duration * Duration +> bool
  durLeq(d1, d2) == durLess(d1,d2) or d1 = d2;

  -- Greater than relation on durations.
  durGrtr: Duration * Duration +> bool
  durGrtr(d1, d2) == durLess(d2, d1);

  -- Greater than or equal relation on durations.
  durGeq: Duration * Duration +> bool
  durGeq(d1, d2) == durLeq(d2, d1);

  -- Does a DTG fall between two given DTGs?
  dtgInRange: DTG * DTG * DTG +> bool
  dtgInRange(dtg1, dtg2, dtg3) == dtgLeq(dtg1, dtg2) and dtgLeq(dtg2, dtg3);

  -- 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) == dtgLeq(i2.begins,i1.ends) and dtgLeq(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) == dtgLeq(i2.begins,i1.begins) and dtgLeq(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 RESULT.time.offset = dtg.time.offset and subtract(RESULT,dur) = dtg;

  -- Decrease a DTG by a duration.
  subtract: DTG * Duration +> DTG
  subtract(dtg, dur) == durToDTG(durDiff(durFromDTG(dtg),dur))
  pre durLeq(dur, durFromDTG(dtg))
  post RESULT.time.offset = dtg.time.offset;
  --post add(RESULT,dur) = dtg;

  -- The duration between two DTGs.
  diff: DTG * DTG +> Duration
  diff(dtg1, dtg2) == durDiff(durFromDTG(dtg1), durFromDTG(dtg2))
  post (dtgLeq(dtg1,dtg2) => add(dtg1,RESULT) = dtg2) and
       (dtgLeq(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 on duration from another.
  durSubtract: Duration * Duration +> Duration
  durSubtract(d1, d2) == mk_Duration(d1.dur - d2.dur)
  pre durGeq(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 durLeq(durMultiply(RESULT, n), d) and durLess(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 (durLeq(d1,d2) => durAdd(d1,RESULT)=d2) and (durLeq(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 durLeq(durFromSeconds(RESULT), d) and durLess(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 durLeq(durFromMinutes(RESULT), d) and durLess(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 durLess(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 durLeq(durFromHours(RESULT), d) and durLess(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 durLess(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 durLeq(durFromDays(RESULT), d) and durLess(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 durLess(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({ m | m in set {1,...,MONTHS_PER_YEAR} & durLeq(durUptoMonth(year,m), dur) }) - 1
  pre durLess(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 durLess (dur, durFromYear(year))
    then 0
    else 1 + durToYear(durDiff(dur, durFromYear(year)), year+1)
  --post RESULT = Set`max({ y | y : Year & durLeq(durUptoYear(year+y), dur) })
  measure durToYear_measure;

  -- The measure function for durToYear
  durToYear_measure : Duration * Year +> nat
  durToYear_measure(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 isUTC(RESULT.time) and durFromDTG(RESULT) = dur;

  -- The duration of a DTG (with respect to the start of time).
  durFromDTG: DTG +> Duration
  durFromDTG(dtg) == let ndtg = normalise(dtg)
                     in durAdd(durFromDate(ndtg.date),durFromTime(ndtg.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 durLeq(durFromDate(RESULT), dur) and durLess(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 +> UTC
  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,nil)
  pre durLess(dur,ONE_DAY)
  post durFromTime(RESULT) = dur;

  -- The duration of a time.
  durFromTime: Time +> Duration
  durFromTime(time) ==
    let ntime = normaliseTime(time).#1
    in durFromUTCTime(ntime);
  --post timeEq(durToTime(RESULT), time);

  -- The duration of a UTC time; offset correction not necessary.
  durFromUTCTime: UTC +> Duration
  durFromUTCTime(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 interval.
  durFromInterval: Interval +> Duration
  durFromInterval(i) == diff(i.begins, i.ends)
  post add(i.begins, RESULT) = i.ends;

  -- The minimum DTG in a set.
  minDTG: set of DTG +> DTG
  minDTG(dtgs) == iota dtg in set dtgs & forall d in set dtgs & dtgLeq(dtg, d)
  pre dtgs <> {};

  -- The maximum DTG in a set.
  maxDTG: set of DTG +> DTG
  maxDTG(dtgs) == iota dtg in set dtgs & forall d in set dtgs & dtgLeq(d, dtg)
  pre dtgs <> {};

  -- The minimum Date in a set.
  minDate: set of Date +> Date
  minDate(dates) == iota date in set dates & forall d in set dates & dateLeq(date, d)
  pre dates <> {};

  -- The maximum Date in a set.
  maxDate: set of Date +> Date
  maxDate(dates) == iota date in set dates & forall d in set dates & dateLeq(d, date)
  pre dates <> {};

  -- The minimum Time in a set.
  minTime: set of Time +> Time
  minTime(times) == iota time in set times & forall t in set times & timeLeq(time, t)
  pre times <> {};

  -- The maximum Time in a set.
  maxTime: set of Time +> Time
  maxTime(times) == iota time in set times & forall t in set times & timeLeq(t, time)
  pre times <> {};

  -- The minimum Duration in a set.
  minDuration: set of Duration +> Duration
  minDuration(durs) == iota dur in set durs & forall d in set durs & durLeq(dur, d)
  pre durs <> {};

  -- The maximum Duration in a set.
  maxDuration: set of Duration +> Duration
  maxDuration(durs) == iota dur in set durs & forall d in set durs & durLeq(d, dur)
  pre durs <> {};

  -- The sum of a sequence of durations.
  sumDuration: seq of Duration +> Duration
  sumDuration(sd) == mk_Duration(Seq`sum([ sd(i).dur | i in set inds sd ]));

  -- An interval that represents an instant in time.
  instant: DTG +> Interval
  instant(dtg) == mk_Interval(dtg,dtg)
  post inInterval(dtg, RESULT);
       --and forall d:DTG & dtgEq(d,dtg) <=> inInterval(d,RESULT);

  -- Format a date and time as per ISO 8601.
  format: DTG +> seq of char
  format(dtg) == formatDate(dtg.date) ^ "T" ^ formatTime(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,o)) ==
    let frac = if l = 0 then "" else "," ^ Numeric`zeroPad(l,3),
        os = if o = nil then "Z" else formatOffset(o)
    in Numeric`zeroPad(h,2) ^ ":" ^ Numeric`zeroPad(m,2) ^ ":" ^
       Numeric`zeroPad(s,2) ^ frac ^ os;

  -- 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) == format(interval.begins) ^ "/" ^ format(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);

  -- Normalise a DTG value such that it is expressed as UTC; the offset is nil.
  -- Applying the offset may result in a change of date.
  -- Example: 2001-01-01T01:00+02:00 becomes 2000-12-31T23:00Z.
  normalise: DTG +> DTG
  normalise(dtg) == let mk_(ntime,pm) = normaliseTime(dtg.time),
                        baseDtg = mk_DTG(dtg.date,ntime)
                    in cases pm:
                         nil     -> baseDtg,
                         <PLUS>  -> subtract(baseDtg,ONE_DAY),
                         <MINUS> -> add(baseDtg,ONE_DAY)
                       end;

  -- Normalise a time value to UTC with respect to the offset, 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: Time +> UTC * [PlusOrMinus]
  normaliseTime(time) ==
    let utcTimeDur = durFromUTCTime(toUTC(time))
    in cases time.offset:
         nil
           -> -- Time already UTC
              mk_(time,nil),
         mk_Offset(offset,<PLUS>)
           -> -- Zone offset ahead of UTC
              if durLeq(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 durLess(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;

end ISO8601

¤ Dauer der Verarbeitung: 0.30 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.