Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/VDM/VDMSL/ISO8601SL/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 28 kB

Quelle ISO8601.vdmsl Sprache: 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 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

quality98%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.